Derivar por modus ponens$[A\rightarrow(B\rightarrow C)]\rightarrow[(A\rightarrow B)\rightarrow(A\rightarrow C)]$

Question

¿Cómo podría derivar por modus ponens la fórmula$$[A\rightarrow(B\rightarrow C)]\rightarrow[(A\rightarrow B)\rightarrow(A\rightarrow C)]$ $ de, y sólo de, los siguientes esquemas de axiomas?

1. $(A\lor A)\rightarrow A$.
2. $A\rightarrow(A\lor B)$.
3. $(A\lor B)\rightarrow(B\lor A)$.
4. $(A\rightarrow B)\rightarrow[(A\lor C)\rightarrow(B\lor C)]$.
5. Si$A\rightarrow B$ y$B\rightarrow C$, entonces$A\rightarrow C$.
6. $A\rightarrow A$.
7. $A\leftrightarrow \neg(\neg A)$.
8. $(A\rightarrow B)\leftrightarrow(\neg B\rightarrow \neg A)$.
9. $(A\land B)\rightarrow A$ y$(A\land B)\rightarrow B$.

Answer 1

En un sistema axiomático no puede derivar en absoluto (es necesario añadir un axioma) , pero si usted tiene un sistema de deducción natural se puede derivar de la nada (ex nihilo)

1) es fácilmente demostrado en un sistema de deducción natural:

1 | |______ P -> (Q -> R))                             Assumption
2 | | |____ P -> Q                                     Assumption
3 | | | |__ P                                          Assumption 
4 | | | |   Q                                          2,3 Modus ponens
5 | | | |   Q -> R                                     1,3 Modus ponens
6 | | | |   R                                          4,5 Modus ponens
. | | | <------------------------------------------------ end subproof 
7 | | |     P -> R                                     3-6 Conditional proof
. | | <-------------------------------------------------- end subproof 
8 | |      (P -> Q) -> (P  -> R)                       2-7 Conditional proof
. | | <-------------------------------------------------- end subproof 
9 | |      (P -> (Q -> R)) -> ((P -> Q) -> (P  -> R))  1-8 Conditional proof
================================
  QED

Pero todavía en una axiomática prueba de que no es demostrable.

Un poco metalogic:

Si un axiomsystem es consistente (la preservación de la verdad), entonces usted no prueba en modo alguno una falsa sentencia.

Si existe una interpretación de un sistema (cualquier interpretación en todos), donde en todos los modelos (valoraciones) todos los axiomas son siempre verdad, todos los teoremas son también siempre la verdad.

si en una interpretación donde en todos los modelos(valoraciones) los axiomas son verdaderos, pero hay un modelo (valoración) cuando una fórmula es falsa esa fórmula es no un teorema.

Ahora $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ falla en Lukasiewisc 3 valores de la lógica, mientras que todos los demás son los axiomas, teoremas de Lukasiewisc 3 valores de la lógica.

Así que los axiomas son verdaderos en todas las valoraciones , sino $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ no es cierto en algunos de valoración , por lo tanto, $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ no puede ser un teorema del sistema.

La prueba

Lukasiewicz 3 valores de lógica se compone de los siguientes truthtables:

       ||     ||  A ->  B || A & B || A v B || 
       || Des ||  1 2 3   || 1 2 3 || 1 2 3 || ~A  
 ----- ||-----||----------||-------||-------||--- 
 A = 1 ||  *  ||  1 2 3   || 1 2 3 || 1 1 1 || 3   
 A = 2 ||     ||  1 1 2   || 2 2 3 || 1 2 2 || 2 
 A = 3 ||     ||  1 1 1   || 3 3 3 || 1 2 3 || 1 

Una fórmula es una tautología o teorema en esta lógica si y sólo si en todo lo posible la valoración de la fórmula devuelve 1 (verdadero o valor determinado)

Todos los axiomas de hacer esto. (comprobar tu mismo)

Pero $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ donde $ P = Q = 2$ $ R = 3 $ produce un error, se devuelve 2

(P -> (Q -> R)) -> ((P -> Q) -> (P  -> R) )
(2 -> (2 -> 3)) -> ((2 -> 2) -> (2  -> 3) )
(2 -> (  2   )) -> ((  1   ) -> (   2   ) )
(  1          ) -> (         2            )
(               2                         )

por lo tanto, $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ no es un teorema de esta lógica , y por lo tanto también no puede ser un teorema de la syatem no puede ser un teorema del sistema.

QED

faltan pasos en esto una prueba de que usted va a pensar acerca de sí mismo

• son los axiomas siempre la verdad. sólo un montón de trabajo , en lugar de un 8 línea truthtable obtener un 27 truthtable

• es el sistema de truthpreserving? esta prueba se basa en un sistema que utiliza el modus ponens ( $ \vdash A, \vdash A \to B $ $ \vdash B $ ) como regla de inferencia, el sistema no tiene esta regla tiene el silogismo hipotético regla de inferencia ( $ \vdash A \to B , \vdash B \to C $ $ \vdash A \to C $ ) a mí me parece que el hypothectical silogismo regla de inferencia es equivalente o un poco más débil que el modus ponens regla de inferencia, pero este está en la necesidad de una prueba es $ A \to (( A \to B ) \to B) $ comprobable de un teorema en el sistema

• ¿cuál es la differece entre una interpretación y un modelo? (una interpretación, es una lógica o lógica del sistema en sí mismo, un modelo es una particular valoración)

• pero estas son cosas que la cooperativa puede pensar

dos carteles que están de acuerdo conmigo, mientras yo pueda prueba de que están equivocados.

Answer 2

En mi respuesta a continuación, podemos encontrar un "moderno" de la reconstrucción de PM's del sistema de lógica proposicional.

Aquí tenemos, con la ayuda de Wiki Principia Mathematica lógica proposicional , el original del comprobante de PM's

*2.77 --- $(p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$.

---

Establecemos primero algunos teoremas útiles :

*(2.05) --- $\vdash (q \rightarrow r) \rightarrow [(p \rightarrow q) \rightarrow (p \rightarrow r)]$ --- a partir de la Suma con la sustitución : $\lnot p/p$.

*(2.06) --- $\vdash (p \rightarrow q) \rightarrow [(q \rightarrow r) \rightarrow (p \rightarrow r)]$ --- desde la Pers con la sustitución : $q \rightarrow p/p; p \rightarrow q/q; p \rightarrow r/r$ y (*2.05) por modus ponens

Llamamos a los anteriores teoremas : Syll

*(2.36) --- $\vdash (q \rightarrow r) \rightarrow [(p \lor q) \rightarrow (r \lor p)]$ - de Syll con el subst $p \lor q/p; p \lor r/q; r \lor p/r$ y Perm por mp, seguido por la Suma y Syll

*(2.37) --- $\vdash (q \rightarrow r) \rightarrow [(q \lor p) \rightarrow (p \lor r)]$ - de Suma, Perm y Syll

*(2.38) --- $\vdash (q \rightarrow r) \rightarrow [(q \lor r) \rightarrow (r \lor p)]$ - de Suma, Perm y Syll

---

Ahora podemos escribir la derivación de (*2.77) :

*2.53 --- $\vdash (p \lor q) \rightarrow (\lnot p \rightarrow q)$.

A partir de (*2.12) [es decir,$\vdash p \rightarrow \lnot \lnot p$] y Syll (*2.38), con la sustitución de $q/p; p/q; \lnot \lnot p/r$, y el mp y la definición de las $\rightarrow$.

*2.6 --- $\vdash (\lnot p \rightarrow q) \rightarrow ((p \rightarrow q) \rightarrow q)$.

Prueba

$\vdash (\lnot p \rightarrow q) \rightarrow ((\lnot p \lor q) \rightarrow (q \lor q))$ --- de Syll (*2.38) con el subst $q/p; \lnot p/q; q/r$

$\vdash [(\lnot p \lor q) \rightarrow (q \lor q)] \rightarrow [(\lnot p \lor q) \rightarrow q]$ --- de Taut, Suma y mp

$\vdash (\lnot p \rightarrow q) \rightarrow ((\lnot p \lor q) \rightarrow q)$ --- de las dos fórmulas anteriores por Syll (*2.06). El uso de la abreviatura de $\rightarrow$ llegamos a la última versión del teorema.

*2.62 --- $\vdash (p \lor q) \rightarrow ((p \rightarrow q) \rightarrow q)$ --- a partir de (*2.53) y (*2.6) por Syll.

*2.621 --- $\vdash (p \rightarrow q) \rightarrow ((p \lor q) \rightarrow q)$ --- a partir de (*2.62) con Comm y mp.

*2.73 --- $\vdash (p \rightarrow q) \rightarrow [((p \lor q) \lor r) \rightarrow (q \lor r)]$ --- a partir de (*2.621) y (*2.38), con la sustitución : $p \lor q/q; q/r; r/p$ y Syll.

*2.74 --- $\vdash (q \rightarrow p) \rightarrow [((q \lor p) \lor r) \rightarrow (p \lor r)]$ --- a partir de (*2.73) con la sustitución : $q/p; p/q$.

Nota. Necesitamos varios pasos de Perm y Assoc a obtener a partir de : $((q \lor p) \lor r)$ $(p \lor (q \lor r))$dentro de la fórmula. Escribimos la primera.

Desde : $(q \rightarrow p) \rightarrow [((q \lor p) \lor r) \rightarrow (p \lor r)]$ aplicamos Comm llegar : $((q \lor p) \lor r) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$; luego usamos Assoc y Syll a obtener : $(r \lor (q \lor p)) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$; y así sucesivamente, hasta que llegamos a : $(p \lor (q \lor r)) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$.

Al final de las transformaciones, aplicamos de nuevo Comm :

*2.74 --- $\vdash (q \rightarrow p) \rightarrow [(p \lor (q \lor r)) \rightarrow (p \lor r)]$.

A partir de (*2.74) con la sustitución de $\lnot q/q$ y (*2.53), con Syll, obtenemos :

$\vdash (q \lor p) \rightarrow [((p \lor (\lnot q \lor r)) \rightarrow (p \lor r)]$.

El uso de Perm y Syll y la definición de $\rightarrow$ llegamos a la versión final :

*2.75 --- $\vdash (p \lor q) \rightarrow [(p \lor (q \rightarrow r)) \rightarrow (p \lor r)]$.

De *2.75 por Comm que se derivan de :

*2.76 --- $\vdash (p \lor (q \rightarrow r)) \rightarrow ((p \lor q) \rightarrow (p \lor r))$.

De *2.76, con la sustitución : $\lnot p/p; q/q; r/r$ obtenemos :

*2.77 --- $\vdash (p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$.

---

El apéndice. Se demuestra la "falta" axioma : Assoc (*1.05) que ha demostrado ser derivable de los demás PM's axiomas por Bernays (además de los otros cuatro axiomas, vamos a utilizar sólo Syll) :

$\vdash (p \lor (q \lor r)) \rightarrow ((p \lor q) \lor r))$;

Prueba

$\vdash r \rightarrow (p \lor r)$ --- Agregar (*1.3)

$\vdash r \rightarrow (p \lor r) \rightarrow [q \lor r \rightarrow q \lor (p \lor r)]$ --- de Suma (*1.6) con subst $r/q;p \lor r/r; q/p$

$\vdash q \lor r \rightarrow q \lor (p \lor r)$ --- modus ponens

$\vdash p \lor (q \lor r) \rightarrow p \lor [q \lor (p \lor r)]$ --- a partir de la Suma con el subst $p/p; q \lor r/q; q \lor (p \lor r)/r$ y mp

(Un) --- $\vdash p \lor (q \lor r) \rightarrow [q \lor (p \lor r)] \lor p$ --- por Perm (*1.4) y Syll (*2.05)

$\vdash p \rightarrow (r \lor p)$ --- Agregar

$\vdash p \lor r \rightarrow q \lor (p \lor r)$ --- de arriba con la sustitución : $p \lor r/p; q/r$

$\vdash p \rightarrow (p \lor r)$ --- de Agregar (*1.3) y Perm (*1.4) por Syll (*2.05)

$\vdash p \rightarrow q \lor (p \lor r)$ --- de las dos últimas por Syll

$\vdash [q \lor (p \lor r)] \lor p \rightarrow ([q \lor (p \lor r)] \lor [q \lor (p \lor r)])$ --- a partir de la última por Syll

(B) --- $\vdash [q \lor (p \lor r)] \lor p \rightarrow [q \lor (p \lor r)]$ --- desde el último uso Tensa y Syll.

Finalmente, a partir de (A) y (B) por Syll :

$\vdash p \lor (q \lor r) \rightarrow (q \lor (p \lor r))$.

Después de haber utilizado sólo (*2.05) en la prueba de Assoc, podemos utilizar Assoc para demostrar Comm (*2.04) :

$\vdash (p \rightarrow (q \rightarrow r)) \rightarrow (q \rightarrow (p \rightarrow r))$ --- de Assoc con la sustitución : $\lnot p/p; \lnot q/q; r/r$.

Ahora, después de haber demostrado Comm, se puede ir a partir de (*2.06).

Answer 3

De acuerdo a Willemien la respuesta anterior, no es posible demostrar que a partir de la propuesta de sistema de axiomas.

Es comprobable en Principia Mathematica (sistema que utiliza los cuatro primeros axiomas y modus ponens) debido a la introducción de la abreviatura :

$p \supset q =_{def} \lnot p \lor q$.

Este es un "simplificado" prueba [ver (T9) más abajo], siguiendo a Peter Andrews, Una Introducción a la Lógica Matemática y la Teoría Tipo : A la Verdad a Través de la Prueba (1986).

Preliminares

Voy a llamar a los cuatro Axiomas como (Ax1)-(Ax4) [véase Russell-Bernays sistema de axiomas con la negación y la disyunción] y los cinco siguientes resultados (R5)-(R9).

Voy a presentar la definición :

$A \rightarrow B$ representa $\lnot A \lor B$. [*1.01]

Podemos tener también : $A \land B$ representa $\lnot (\lnot A \lor \lnot B)$ [*3.01], y $A \leftrightarrow B$ representa $(A \rightarrow B) \land (B \rightarrow A)$ [*4.01].

Los axiomas se hará constar en la forma primitiva como :

(Ax1'). $\lnot (A\lor A) \lor A$ --- (Tenso) [*1.2]

(Ax2'). $\lnot A \lor (A\lor B)$ --- (Agregar) [*1.3]

(Ax3'). $\lnot (A\lor B) \lor (B\lor A)$ --- (Perm) [*1.4]

(Ax4'). $\lnot (\lnot A \lor B) \lor [\lnot (A\lor C) \lor (B\lor C)]$ --- (Suma) [*1.5]

Las versiones originales se derivan de la utilización de la definición de $\rightarrow$.

Como reglas de inferencia, vamos a utilizar sólo modus ponens [*1.1], formulado utilizando la definición de $\rightarrow$ como :

de $A$ y $A \rightarrow B$, $B$ puede ser inferido;

y la sustitución de la regla :

para una variable proposicional cualquier fórmula puede ser sustituido.

Voy a llamar (R5) como Syll [*2.06].

Acerca de (R7 - Doble Negación) : $\vdash A\leftrightarrow \neg(\neg A)$, somos capaces de demostrar como (T2) y (T3), y que realmente sólo necesitan : $\vdash A\rightarrow \neg(\neg A)$.

Acerca de (R8) y (R9), no van a ser utilizados en las pruebas a continuación.

A partir de (Ax4) que se derivan de la regla :

(R10). Si $\vdash (A\rightarrow B)$$\vdash (A\lor C)$,$\vdash (B\lor C)$ .

A partir de (Ax3) que se derivan de la regla :

(R11). Si $\vdash (A\lor B)$,$\vdash (B\lor A)$.

---

Inicial teoremas

(T1). $\vdash A \lor \lnot A$. [*2.11]

Prueba

$\vdash ((A \lor A) \rightarrow A) \rightarrow [((A \lor A) \lor \lnot A) \rightarrow (A \lor \lnot A)]$ --- a partir de (Ax4) con el subst: $A \lor A/A; A/B; \lnot A/C$

$\vdash (A \lor A) \rightarrow A$ --- (Ax1)

$\vdash ((A \lor A) \lor \lnot A) \rightarrow (A \lor \lnot A)$ --- por MP

$\vdash (A \lor A) \lor \lnot A $ --- a partir de (Ax2') con el subst $A/A; A/B$ usando (Ax3) y Syll

$\vdash A \lor \lnot A$ --- por MP.

(T2). $\vdash A \rightarrow \lnot \lnot A$. [*2.12]

Prueba

A partir de (T1) con el subst : $\lnot A/A$ y la definición de $\rightarrow$.

(T3). $\vdash \lnot \lnot A \rightarrow A$. [*2.14]

Prueba

$\vdash (\lnot A \rightarrow \lnot \lnot \lnot A) \rightarrow ((\lnot A \lor A) \rightarrow (\lnot \lnot \lnot A \lor A))$ --- (Ax4)

$\vdash \lnot A \lor A \rightarrow (\lnot \lnot \lnot A \lor A)$ - - - (T2) con el subst $\lnot A/A$ por MP

$\vdash \lnot \lnot A \rightarrow A$ --- con (Ax3) y Syll por MP, y la definición de $\rightarrow$.

(T4). Si $\vdash A \rightarrow C$$\vdash B \rightarrow C$,$\vdash (A \lor B) \rightarrow C$.

Prueba

$\vdash B \rightarrow C$ --- supone

$\vdash B \lor A \rightarrow C \lor A$ --- (Ax4) y MP

$\vdash B \lor A \rightarrow A \lor C$ --- (Ax3) y Syll

$\vdash A \lor B \rightarrow A \lor C$ --- (Ax3) y Syll

$\vdash A \rightarrow C$ --- supone

$\vdash A \lor C \rightarrow C \lor C$ --- (Ax4) y MP

$\vdash A \lor B \rightarrow C \lor C$ --- Syll

$\vdash C \lor C \rightarrow C$ --- (Ax1)

$\vdash A \lor B \rightarrow C$ --- Syll

(T5). Si $\vdash A \rightarrow C$$\vdash \lnot A \rightarrow C$, luego $\vdash C$. [*2.61]

Prueba

Por (T4) con el subst : $\lnot A/B$ e (T1) y el MP.

(T6). Si $\vdash A \rightarrow C$,$\vdash A \rightarrow (C \lor B)$$\vdash A \rightarrow (B \lor C)$.

Prueba

$\vdash A \rightarrow B$ --- supone

$\vdash A \rightarrow (C \lor B)$ --- (Ax2) y Syll

$\vdash A \rightarrow (B \lor C)$ --- (Ax3) y Syll

(T7). $\vdash [(A \lor B) \lor C] \rightarrow [A \lor (B \lor C)]$. [*2.32]

Prueba

1) $\vdash A \rightarrow [A \lor (B \lor C)]$ --- (R6) y (T6)

2) $\vdash B \rightarrow (B \lor C)$ --- (R6) y (T6)

3) $\vdash B \rightarrow [A \lor (B \lor C)]$ --- de 2) por (T6)

4) $\vdash (A \lor B) \rightarrow [A \lor (B \lor C)]$ --- a partir de 1) y 3) por (T4)

5) $\vdash C \rightarrow (B \lor C)$ --- (R6) y (T6)

6) $\vdash C \rightarrow [A \lor (B \lor C)]$ --- 5) por (T6)

7) $\vdash [(A \lor B) \lor C] \rightarrow [A \lor (B \lor C)]$ --- de 4) y 6) por (T4)

(T8). Si $\vdash (A \lor B) \lor C$,$\vdash A \lor (B \lor C)$.

Prueba

(T7).

---

Principales teorema de

(T9). Si $\vdash (A \rightarrow B)$$\vdash A \rightarrow (B \rightarrow C)$,$\vdash A \rightarrow C$.

Prueba

1) $\vdash A \rightarrow B$ --- supone

2) $\vdash A \rightarrow (B \rightarrow C)$ --- supone

3) $\vdash \lnot A \lor (\lnot B \lor C)$ --- por definición de $\rightarrow$

4) $\vdash (\lnot B \lor C) \lor \lnot A$ --- a partir de 3) (R11)

5) $\vdash \lnot B \lor (C \lor \lnot A)$ --- por (T8)

6) $\vdash B \rightarrow (C \lor \lnot A)$ --- por definición de $\rightarrow$

7) $\vdash A \rightarrow (C \lor \lnot A)$ --- desde el 1) y 6) por Syll

8) $\vdash \lnot A \lor (C \lor \lnot A)$ --- por definición de $\rightarrow$

9) $\vdash (C \lor \lnot A) \lor \lnot A$ --- por (R11)

10) $\vdash C \lor (\lnot A \lor \lnot A)$ --- por (T8)

11) $\vdash (\lnot A \lor \lnot A) \lor C$ --- de 10) por (Ax3)

12) $\vdash \lnot A \lor C$ --- a partir de (Ax1) (es decir,$\vdash (\lnot A \lor \lnot A) \rightarrow \lnot A$) y (11) (R10)

13) $\vdash A \rightarrow C$ --- por definición de $\rightarrow$.

Para la versión original de (*2.77), ver la otra respuesta (para la mayoría de aplicaciones, la versión actual es suficiente).

---

Los resultados adicionales

(T10). $\vdash A \rightarrow (\lnot A \rightarrow B)$. [*2.24]

Prueba

(T2) y (T6) por MP.

(T11). $\vdash (A \lor B) \rightarrow (\lnot A \rightarrow B)$. [*2.53]

Prueba

$\vdash (A \rightarrow \lnot \lnot A) \rightarrow ((A \lor B) \rightarrow (\lnot \lnot A \lor B))$ --- (Ax4)

$\vdash (A \lor B) \rightarrow (\lnot \lnot A \lor B)$ \begin{cases} 1 & \text{if %#%#%} \\ 0 & \text{else} \\ \end(T2) con MP

$\vdash (A \lor B) \rightarrow (\lnot A \rightarrow B)$ --- por definición de $\rightarrow$.

(T12). $\vdash (\lnot A \rightarrow B) \rightarrow (A \lor B)$. [*2.54]

Prueba

Como (T11) de (T3).