¿Dar una prueba de que "p y ~ p" implica "q"?

Question

Contexto: Este no es un libro de texto o los deberes problema. Tenía la esperanza de que las personas más jóvenes podría ayudar a mi viejo y cansado cerebro. "Todo el mundo sabe que" una contradicción implica nada. Lo que estoy buscando es una prueba de la conclusión "q" a partir de la premisa de "p & ~p", en algunos ampliamente utilizados prueba de la teoría de lógica proposicional.

El uso de las tablas de verdad no está permitido, ya que me llame que el modelo de la teoría. Y no hay trucos como tomar lo que se ha demostrado como uno de sus axiomas, sobre la base de que es válido. Una prueba en un sistema axiomático, sería preferible, pero una deducción natural prueba está bien también. Por favor, dar una referencia a un texto o sitio web en el que se establece la prueba de la teoría en su totalidad.

Yo realmente lo necesitas para algo que estoy trabajando. Gracias por tu ayuda.

Answer 1

Se puede ver en Elliott Mendelson, Introducción a la Lógica Matemática (4ª ed - 1997), página 38, el Lema 1.11.c [consulte la página 39 para la derivación] :

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

Es el "bloque de construcción básico" para probar en una de Hilbert de estilo a prueba de sistema de axiomas + modus ponens) el Ex Falso Quodlibet.

En Deducción Natural, puede utilizar el llamado $\lnot$-eliminación de la regla (de$A$$\lnot A$, inferir $\bot$, es decir, el falsum), seguido por la Abs-regla (de $\bot$, inferir $B$ lo que sea) que se derivan de una contradicción, una fórmula wathever [puedes ver el debate acerca de la DN reglas que implican $\lnot$ y $\bot$ en este post].

Nota.

Este es Mendelson sistema de axiomas :

(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}))$

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

Con (A1) y (A2) demuestra Lema 1.8 [página 36] :

$\vdash \mathcal{B} \rightarrow \mathcal{B}$.

Con la ayuda de Lema 1.8 y el uso de sólo (A1) y (A2) es posible demostrar el Teorema de la Deducción [la Proposición 1.9, página 37]:

si $\Gamma, \mathcal{B} \vdash \mathcal{C}$,$\Gamma \vdash \mathcal{B} \rightarrow \mathcal{C}$.

Finalmente, Mendelson demuestra Lema 1.11.c :

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

Sin DT aún podemos tener ex falso quodlibet como un "derivado de la regla" :

(1) $\quad \lnot \mathcal B$ --- supone

(2) $\quad \mathcal B$ --- supone

(3) $\quad \vdash \mathcal B \rightarrow ( \lnot \mathcal C \rightarrow \mathcal B )$ --- (A1)

(4) $\quad \vdash \mathcal{\lnot B} \rightarrow ( \mathcal{\lnot C} \rightarrow \mathcal{\lnot B})$ --- (A1)

(5) $\quad \mathcal{\lnot C} \rightarrow \mathcal B$ --- a partir de (2) y (3) por modus ponens

(6) $\quad \mathcal{\lnot C} \rightarrow \mathcal{\lnot B}$ --- a partir de (1) y (4) por modus ponens

(7) $\quad \vdash (\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$ --- (A3)

(8) $\quad \mathcal{C}$ --- a partir de (5), (6) y (7) por modus ponens dos veces.

Por lo tanto :

$\quad \lnot \mathcal B, \mathcal B \vdash \mathcal C$.

En Mendelson del sistema, $\land$ $\lor$ son no primitivo; se definen como :

$p \land q =_{def} \lnot (p \rightarrow \lnot q)$

$p \lor q =_{def} \lnot p \rightarrow q$

Tener el Teorema de la Deducción, Mendelson, prueba un par de otros resultados de utilidad [ver Corolario 1.10, página 38] y, a continuación, Lema 1.11 incluyendo :

$\vdash \lnot \lnot \mathcal B \rightarrow \mathcal B$ --- Lema 1.11.un

y

$\vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lema 1.11.b.

Ahora tenemos :

(a)$\quad \vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lema 1.11.b

(b)$\quad \vdash \lnot \lnot (\mathcal B \rightarrow \lnot \lnot \mathcal B)$ --- de Lema 1.11.b ", que se aplica a sí mismo" modus ponens

(c)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B)$ --- con la definición de $\land$

(d)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B) \rightarrow ((\mathcal B \land \lnot \mathcal B) \rightarrow \mathcal C)$ --- Lema 1.11 c con la sustitución de $(\mathcal B \land \lnot \mathcal B)$ en lugar de $\mathcal B$.

Por lo tanto :

$\vdash \mathcal B \land \lnot \mathcal B \rightarrow \mathcal C$ --- de (c) y (d) por modus ponens.

Leer más.

Puede ser útil ver la nota por Peter Smith en los Tipos de prueba del sistema en su Lógica de Asuntos blog.

Answer 2

Yo uso la notación polaca.

Ya quieres algo ampliamente utilizado (existe sistemas que reciben menos usado que usted podría encontrar más interesante para ciertos fines), voy a utilizar el sistema de axiomas que hace referencia la Wikipedia. Que son los axiomas de

3 CCpCqrCCpqCpr.

4 CpCqp.

5 CCNpNqCqp.

El sistema también tiene definiciones para otras conectivas. Usted no encontrará todas las definiciones de todos los otros binarios y unario conectivas en la mayoría de los textos de lógica, y que no son necesarios aquí. La definición pertinente que necesitamos para este problema es:

1. C $\delta$ NCpNq $\delta$ Kpq,

donde $\delta$ es una variable functor de un argumento.

Usted ha pedido una prueba de KpNp $\vdash$ q. Debido a la deducción metatheorem y su opuesto, si KpNp $\vdash$ q, entonces CKpNpq. También, si CKpNpq, entonces KpNp $\vdash$ q. Ahora, la definición nos dice que si podemos probar CNCpNNpq, que CKpNpq puede seguir. Yo uso la notación Dx.y * z para condensada desprendimiento con x como la premisa mayor, y como la premisa menor, y "z" como el resultado de la fórmula. Yo también voy a escribir la anotación de la prueba antes de la prueba. Así que, he aquí una prueba:

D3.3 * 7

7 CCCpCqrCpqCCpCqrCpr

D4.4 * 8

8 CpCqCrq

D3.4 * 9

9 CCpqCpp

D4.3 * 10

10 CpCCqCrsCCqrCqs

D4.5 * 11

11 CpCCNqNrCrq

D7.8 * 12

12 CCpCCqprCpr

D4.8 * 13

13 CpCqCrCsr

D9.5 * 14

14 Cpp

D3.14 * 15

15 CCCpqpCCpqq

D7.13 * 16

16 CCpCCqCrqsCps

D3.11 * 17

17 CCpCNqNrCpCrq

D12.11 * 18

18 CNpCpq

D12.10 * 19

19 CCpqCCrpCrq

D4.18 * 20

20 CpCNqCqr

D3.18 * 21

21 CCNppCNpq

D15.20 * 22

22 CCCNpCpqrr

D16.19 * 23

23 CCCpqrCqr

D23.21 * 24

24 CpCNpq

D22.17 * 25

25 CNNpCqp

D16.25 * 26

26 CNNpp

D5.26 * 27

27 CpNNp

D24.27 * 28

28 CNCpNNpq

Ahora en 1. sustituimos $\delta$ C r, donde el apóstrofe [ ' ] indica la wff que sigue inmediatamente a $\delta$ 1 (NCpNq, y Kpq, respectivamente) obtención de 29.

29 CCNCpNqrCKpqr

Finalmente D29.28 de rendimientos

30 CKpNpq.

Supongamos ahora KpNp como una premisa. Por lo tanto, por el desapego y 30 obtenemos q como una conclusión. Por lo tanto, hemos KpNp $\vdash$ p como una meta-teorema.

Answer 3

Leí esto en Wikipedia tal vez, pero ahora no encuentro una fuente.

Da: $p$ y $\overline p$ son verdaderas.

Para probar: $q$

$$p\lor q =True\tag{vacuosly since $p$ is true}$$

Pero es verdad $\overline{p}$, $\implies p$ es false. $$false \lor q = True \implies q=True$$