Deducción natural tautología

Question

Estoy tratando de probar la siguiente tautologías:

\begin{align} & ⊢ (A \to (B \to A)) \\ & ⊢ ((A \to B) \to A) \to A \end{align}

Para la primera, lo que hice fue:

1. $A$ asunción
   1. $B$ asunción
   2. $A$ reexpresado
2. $B \to A$ flecha-introducción de 2 y 3
   1. $A \to (B \to A)$ flecha-introducción de 1-4

Pero esto no se ve bien para mí.

Para la segunda, aquí está lo que tengo hasta ahora:

1. ((A - > B) --> A) asunción
   1. A --> B asunción
   2. Una flecha de eliminación de 1 y 2

Answer 1

Usted va a comenzar asumiendo $(A\to B)\to A$.

Lo ideal sería probar $A\to B$ y, a continuación, $A$ seguir, sino de curso $A\to B$ no es una tautología, por lo que no puede ser probada. Pero $\neg (A\to B)\lor (A\to B)$ es una tautología y por lo tanto puede ser probada.

Así que voy a probar la mencionada tautología, entonces usted va a realizar $\lor\text{-Elim}$ en esta tautología.

Uno de los casos se sigue de la hipótesis inicial.

Queda demostrado que se puede demostrar $A$$\neg(A\to B)$.

Esto es algo como esto:

• $\neg (A\to B)$
• $\,\,\,\,\neg A$ (Hipótesis)
• $\,\,\,\,\,\,\,\,\,\,\,\, A$ (Hipótesis)
• $\,\,\,\,\,\,\,\,\,\,\,\,\bot$
• $\,\,\,\,\,\,\,\, \,\,\,\,B$
• $\,\,\,\,A\to B$
• $\,\,\,\, \bot$
• $\neg \neg A$
• $A.$

Answer 2

Has resuelto el primero, así que aquí hay dos maneras de probar la segunda. 'Tensa Con' es el modus tollens.

Me he tomado la libertad de escribir Git Gud's de pruebas alternativas más explícitamente aquí (por favor vote por su respuesta si usted también resulta intuitivo). Se pone de relieve la relación a la ley de medio excluido y es económico en su uso de reglas especiales (por ejemplo, no apela a modus tollens). Aquí está:

Otra manera sería probar el contrapositivo, utilizando sólo $\rightarrow$-intro & Reit:

Answer 3

Yo uso la notación polaca. La segunda se convierte en la fórmula CCCabaa. La regla que se va a utilizar (flecha introducción, en la que voy a llamar "Ci", y el desprendimiento/eliminación condicional, que voy a llamar "Co") es {CN$\alpha$$\beta$, CN$\alpha$N$\beta$} $\vdash$ $\alpha$, que voy a llamar a "No".

hypothesis 1  |     CCaba
hypothesis 2  ||    Na
hypothesis 3  |||   a
hypothesis 4  ||||  Nb
hypothesis 5  ||||| a
Ci 5-5     6  ||||  Caa
Co 6, 3    7  ||||  a
Ci 4-7     8  |||   CNba
hypothesis 9  ||||  Nb
hypothesis 10 ||||| Na
Ci 10-10   11 ||||  CNaNa
Co 11, 2   12 ||||  Na
Ci 9-12    13 |||   CNbNa
No 13, 8   14 |||   b
Ci 3-14    15 ||    Cab
Co 1, 15   16 ||    a
Ci 2-16    17 |     CNaa
hypothesis 18 ||    Na
Ci 18-18   19 |     CNaNa
No 17, 19  20 |     a
Ci 1-20    21       CCCabaa

Para la primera se podría también escribir:

hypothesis 1 |   a
hypothesis 2 ||  b
hypothesis 3 ||| a
Ci 3-3     4 ||  Caa
Co 4, 1    5 ||  a
Ci 2-5     6 |   Cba
Ci 1-6     7     CaCba

Me pregunto por qué no también te pide demostrar CCpCqrCCpqCpr. Puesto que usted puede probar CCpCqrCCpqCpr utilizando sólo la introducción condicional y el desapego, una consecuencia de aquí vienen como que todas las implicaciones (bien formado fórmulas con sólo "C"'s y variables) que califican como tautologías puede obtener probado de introducción condicional, el desprendimiento y la regla

{CN$\alpha$$\beta$, CN$\alpha$N$\beta$} $\vdash$ $\alpha$, desde {CpCqp, CCpCqrCCpqCpr, CCCpqpp} bajo desprendimiento y uniforme de sustitución viene como suficiente para la implicational cálculo proposicional.