Prueba $\vdash (p\to q)\lor (q\to r)$ utilizando la deducción natural

Question

Estoy tratando de probar lo siguiente:

$\vdash (p\to q)\lor(q\to r)$

utilizando sólo reglas intuitivamente válidas. He probado algunas formas diferentes, y creo que mi problema es que no estoy seguro de qué suposiciones hacer. ¿Puede alguien ayudarme? Gracias.

Answer 1

Esta afirmación no puede demostrarse mediante reglas intuitivamente válidas, ya que equivale a la ley del medio excluido, que no se sostiene intuitivamente.

Para ser más precisos tenemos:

$~\vdash X \lor \neg X$ por cada $X$ equivale a tener $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ por cada $A, B, C.$

Prueba:

• Supongamos que tenemos que demostrar $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ entonces por $\mathsf{LEM}$ sabemos $\vdash B \lor \neg B$ . En el caso de que $B$ se mantiene, ciertamente podemos mostrar $A \rightarrow B$ y en el otro caso podemos mostrar $\neg B \vdash B \rightarrow C$ desde $\neg B, B \vdash \bot$ .
• Supongamos que tenemos $~\vdash (A \rightarrow B) \lor (B \rightarrow C)$ por cada $A,B,C$ y tratar de mostrar $~\vdash X \lor \neg X$ para muy $X$ . Para ello, simplemente elegimos $A := (X \rightarrow X)$ , $B := X$ , $C := \bot$ .

---

Para ver una lista de más declaraciones equivalentes a $\mathsf{LEM}$ en la lógica intuicionista, eche un vistazo a este documento: Clasificación de las implicaciones materiales sobre la lógica mínima .

Answer 2

Puede probarlo en clásico lógica.

1) $q$ --- asumido [a]

2) $p \to q$ --- $\to$ -intro

3) $(p \to q) \lor (q \to r)$ --- $\lor$ -intro

4) $\lnot q$ --- asumido [b]

5) $\bot$ --- de 1) y 4)

6) $r$ --- de 5)

7) $q \to r$ --- $\to$ -intro

8) $(p \to q) \lor (q \to r)$ --- $\lor$ -intro

9) $\vdash q \lor \lnot q$ --- LEM

10) $(p \to q) \lor (q \to r)$ --- de 1)-3) y 4)-8) con 9) por $\lor$ -eliminación, descargando los supuestos [a] y [b].

Supongo que no podemos probarlo intuitivamente...

Answer 3

@Lereau da la respuesta técnica de por qué tu wff no es intuitivamente demostrable.

Pero ante una pregunta como ésta, siempre vale la pena dar un paso atrás y preguntarse si un determinado wff debe para que sea demostrable intuitivamente. ¿Parece el tipo de cosa que es constructivamente demostrable?

Bueno, obviamente no es así en este caso, ya que una disyunción sólo es demostrable constructivamente si uno de los disyuntos es demostrable constructivamente. Y evidentemente en este caso $(p \to q)$ no es demostrable constructivamente (sin suposiciones de fondo para jugar). Y lo mismo para la otra disyuntiva. Así que incluso antes de la respuesta técnica ya deberías saber que el wff es no constructivamente demostrable. (Aunque es clásicamente demostrable como señala @Mauro, o como se desprende inmediatamente de la respuesta de @Lereau).