Una pregunta sobre el cálculo proposicional implícito

Question

Mi pregunta está motivada por un post anterior sobre Cálculo implícito

Habiendo demostrado que los axiomas de Mendelson (A1) y (A2) más La ley de Peirce son un conjunto completo de axiomas para implicación fragmento del cálculo proposicional, donde :

(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$

(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$

y La ley de Peirce es :

$((\mathcal{A} \rightarrow \mathcal{B}) \rightarrow \mathcal{A}) \rightarrow \mathcal{A}$

No soy capaz de derivar (A3), donde :

(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$ .

Con el fin de ampliar cálculo implicacional al completo cálculo proposicional Supongo que tenemos que introducir $\bot$ con el fin de definir $\lnot \mathcal{A}$ como $\mathcal{A} \rightarrow \bot$ .

Pero sigo sin encontrar la solución.

Answer 1

Creo que he resuelto el esquema, todavía tengo que rellenar los huecos pero aquí algo para empezar: (f = $ \bot $ )

1  |- ( A -> (B->C)) -> ((A -> B)-> (A->C)))                 A2 
2  |- ( A -> (B->f)) -> ((A -> B)-> (A->f)))                 1 C := f
3  |- ( (A->f) -> (B->f) )-> (((A->f) -> B)-> ((A->f)->f)))  2 A := (A->f)
4  |- ((A -> B) -> A) -> A                                   A3 Peirce
5  |- ((A->f) -> A) -> A                                     4  B := f 
6  |- ((A->f) -> f) -> ((A->f) -> f)                         theorem (A -> A)
7  |- f -> A                                                 axiom 
8  |- ((A -> f) -> f) -> ((A -> f) -> A)                     hyp syll 6,7 
9  |- ((A -> f) -> f) -> A                                   hyp syll 8,5
10 |- ((A -> f) -> (B-> f)) -> (((A ->f) -> B)-> A )         hyp syll 3,9

Y 10 es $ ( \lnot A \to \lnot B) \to (( \lnot A \to B) \to A ) $

buen ejercicio

Answer 2

Combinando la estrategia de las subfórmulas, la ponderación de los axiomas y el objetivo, y una búsqueda (parcial) de saturación de niveles, he encontrado una prueba de 15 pasos (excluyendo los axiomas), de nivel 5, utilizando OTTER [1]. En realidad, en lugar de probar

CCCp0Cq0CCCp0qp. OTTER demostró que el más general

CCCpqCr0CCCpqrp. (podemos sustituir q/0, r/q en CCCpqCr0CCCpqrp para obtener CCCp0Cq0CCCp0qp, pero no podemos obtener CCCpqCr0CCCpqrp a partir de CCCp0Cq0CCp0qp sólo por sustitución).

Tenga en cuenta que esto no implica que

CCNpNqCCNpqp podría ser sustituido por

CCCpqNrCCCpqrp sin la definición Np := Cp0.

Aquí está la prueba:

axiom         3 CxCyx.                   Level of formula is 0.

axiom         4 CCxCyzCCxyCxz.           0

axiom         5 CCCxyxx.                 0

axiom         6 C0x.                     0

D3.3          7 CxCyCzy.                 1

D4.4          8 CCCxCyzCxyCCxCyzCxz.     1

D3.4          9 CxCCyCzuCCyzCyu.         1

D3.5         11 CxCCCyzyy.               1

D3.6         13 CxC0y.                   1

DD4.4.7      17 CCxCCyxzCxz.             2

D3.9         20 CxCyCCzCuvCCzuCzv.       2

D4.11        25 CCxCCyzyCxy.             2

D4.13        27 CCx0Cxy.                 2

D17.9        42 CCxyCCzxCzy.             3

DD4.4.20     51 CCxCCCyCzuCCyzCyuvCxv.   3

DD4.11.27    71 CCCxy0x.                 3

D51.42      224 CCCCxyCxzuCCxCyzu.       4

D42.71      300 CCxCCyz0Cxy.             4

D224.300   2474 CCCxyCz0CCCxyzx.         5

1]- W. McCune, "OTTER y Mace2", http://www.mcs.anl.gov/research/projects/AR/otter/ , 1988-2014.

Answer 3

La solución está motivada por Alonzo Church, Introducción a la lógica matemática (1956), Ex 12.7 [página 86].

Necesitamos $\bot$ y $\rightarrow$ como primitivos y la definición de $\lnot A$ como : $A \rightarrow \bot$ .

Necesitamos también como axioma adicional, Ex Falso Quodlibet [véase Church, párrafo 122, página 84] :

$\vdash \bot \rightarrow A$ .

Con EFQ y La ley de Peirce podemos tener Doble negación :

$\vdash \lnot \lnot A \rightarrow A$ .

Prueba

1) $\lnot \lnot A$ --- asumido

2) $\lnot A \rightarrow \bot$ --- por defecto de $\lnot$

3) $\lnot A$ --- asumido

4) $\bot$ --- de 2) y 3) por modus ponens

5) $\vdash \bot \rightarrow A$ --- EFQ

6) $A$ --- de 4) y 5) por mp

7) $\lnot A \rightarrow A$ --- de 3) y 6) por Teorema de la deducción

8) $\vdash (\lnot A \rightarrow A) \rightarrow A$ --- de La ley de Peirce

9) $A$ --- de 7) y 8) por mp

10) $\vdash \lnot \lnot A \rightarrow A$ --- de 1) y 9) por DT .

---

Nota

Véase Joel W. Robbin, Lógica matemática: un primer curso (1969 - reimpresión de Dover), página 22 : el esquema axiomático (A3) del sistema de Mendelson puede ser sustituido por : $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ o, de forma equivalente, por $\vdash (\lnot A \rightarrow B) \rightarrow (\lnot B \rightarrow A)$ .

O podemos sustituirlo por EFQ y La ley de Peirce .

---

Ahora la prueba de Mendelson (A3) :

1) $\lnot C \rightarrow \lnot B$ --- asumido

2) $\lnot C \rightarrow B$ --- asumido

3) $\lnot C$ --- asumido

4) $\lnot B$ --- de 1) y 3) por modus ponens

5) $B$ --- de 2) y 3) por modus ponens

6) $\bot$ --- de 4) y 5) y la definición de $\lnot$ , por mp

7) $\lnot \lnot C$ --- de 3) y 6) por DT

8) $C$ --- de 7) y Doble negación , por mp .

Por último, aplique Teorema de la deducción dos veces :

$\vdash (\lnot C \rightarrow \lnot B) \rightarrow ((\lnot C \rightarrow B) \rightarrow C)$ .

---

Hemos utilizado el Teorema de la deducción que es demostrable con (A1) y (A2) sólo.