$P \to Q \equiv \neg P \vee Q$

Question

La mayoría de los libros de texto que he revisado demuestran la equivalencia dada utilizando la tabla de verdad. Pero, ¿hay alguna forma de demostrar $P \to Q \equiv \neg P \vee Q$ ¿sin tabla de verdad?

Answer 1

$(1)\quad$ Pruébalo: $(P\rightarrow Q)\rightarrow(\neg P\vee Q)$ y $(\neg P\vee Q)\rightarrow (P\rightarrow Q)$

$(2)\quad$ Supongamos que $P\rightarrow Q$ y asumir $P$ entonces $Q$

$(3)\quad$ y por ello $\neg P\vee Q$

$(4)\quad$ si $\neg P$ entonces también $\neg P\vee Q$ .

$(5)\quad$ Invertir, asumir $\neg P\vee Q$ . Si $Q$ entonces $P\rightarrow Q$ .

$(6)\quad$ Y si $\,\neg P$ entonces también $P\rightarrow Q$ .

$\therefore$ $(P\rightarrow Q)\equiv(\neg P\vee Q)$

---

$(1)\quad ((f\rightarrow g) \wedge (g\rightarrow f))\equiv (f\equiv g)$

$(2)\quad ((f\rightarrow g)\wedge f)\rightarrow g$

$(3)\quad f\rightarrow (f\vee g)$

$(4)\quad f\rightarrow (f\vee g)$

$(5)\quad g\rightarrow (f\rightarrow g)$

$(6)\quad \neg f\rightarrow (f\rightarrow g)$

Answer 2

Utilizo la notación polaca/Lukasiewicz. Los axiomas del sistema son 1. CaCba. y 2. CCaCbcCCabCac.

La regla Co es {C $\alpha$$ \N-beta $, $ \N - Alfa $} $ \N - El vaciado de la puerta de entrada $ $ \N -beta$.

La regla Ail es $\alpha$ $\vdash$ A $\alpha$$ \N -beta$.

La regla Ci nos permite pasar de { $\gamma$ , $\alpha$ } $\vdash$ $\beta$ a $\gamma$ $\vdash$ C $\alpha$$ \N-beta $, where "$ |gamma $" indicates a set of hypotheses, axioms, or assumptions, and $ \N - alfa$ consiste en la última hipótesis realizada.

La regla del No es {CN $\alpha$$ \N-beta $, CN$ \N - Alfa $N$ \N-beta $} $ \N - El vaciado de la puerta de entrada $ $ \alpha$ (no hay ninguna regla Ni en la base del sistema).

La regla del aire es $\alpha$ $\vdash$ A $\beta$$ \N - Alpha$.

La regla Ao es {A $\alpha$$ \N-beta $, C$ \N - Alfa $$\gamma$ , C $\beta$$ |gamma $} $ \N - El vaciado de la puerta de entrada $ $ \N - La gamma$.

La regla Ei es {C $\alpha$$ \N-beta $, C$ \N-beta $$\alpha$ } $\vdash$ E $\alpha$$ \N -beta$.

hypothesis         1 | Cpq
hypothesis         2 || NANpq
hypothesis         3 ||| Np
3 Ail              4 ||| ANpq
3-4 Ci             5 || CNpANpq
axiom CaCba        6 || CNANpqCNpNANpq
6, 2 Co            7 || CNpNANpq
5, 7 No            8 || p
8, 1 Co            9 || q
9 Air              10 || ANpq
2-10 Ci            11 | CNANpqANpq
hypothesis         12 || NANpq
12-12 Ci           13 | CNANpqNANpq
11, 13 No          14 | ANpq
Ci 1-14            15 CCpqANpq
hypothesis         16 | ANpq
hypothesis         17 || p
hypothesis         18 ||| Np
axiom CaCba        20 ||| CpCNqp
axiom CaCba        21 ||| CNpCNqNp
20, 17 Co          22 ||| CNqp
21, 18 Co          23 ||| CNqNp
22, 23 No          24 ||| q
Ci 18-24           25 || CNpq
hypothesis         26 ||| q
Ci 26-26           27 || Cqq
16, 25, 27 Ao      28 || q
17-28 Ci           29 | Cpq
16-29 Ci           30 CANpqCpq
15, 30 Ei          31 ECpqANpq

Lehs parece haberme retado a demostrar esto de forma axiomática. La definición de una fórmula es:

1. Todas las letras minúsculas del alfabeto latino son fórmulas.
2. Si $\alpha$ es una fórmula, entonces N $\alpha$ es una fórmula.
3. Si $\alpha$ y $\beta$ son fórmulas, entonces C $\alpha$$ \N-beta $ and A$ \N - Alfa $$\beta$ son fórmulas.
4. Nada más para esta respuesta es una fórmula.

Los axiomas del sistema son:

Prefijación recursiva de variables: CpCqp

Distribución condicional: CCpCqrCCpqCpr

Negación fuera: CCNpNqCCNpqp

Alternancia en la izquierda: CpApq

Alternancia en la derecha: CpAqp

Alternancia fuera: CApqCCprCCqrr

Equivalencia en: CCpqCCqpEpq

Las únicas reglas primitivas de inferencia son la sustitución uniforme y la separación de C {C $\alpha$$ \N-beta $, $ \N - Alfa $} $ \N - El vaciado de la puerta de entrada $ $ \beta$. Esto convierte el desprendimiento condensado en una regla de inferencia derivable como J. A. Kalman demostrado .

Una prueba es una secuencia finita de fórmulas en la que cada paso de la prueba es un axioma, o se deriva de los pasos precedentes de la prueba por sustitución uniforme, desprendimiento C o desprendimiento condensado. D $\alpha$ . $\beta$ indica una aplicación de desprendimiento condensado con $\alpha$ como la premisa que tiene la forma C $\gamma$$ \N - delta $ (the "major premise"), and $ \N-beta $ having the form $ |gamma $ (the "minor premise") yielding the formula $ \N - delta$. He probado esto a mano. No sé cómo conseguir que un probador de teoremas automatizado demuestre algo así desde cero. Las notas de Robert Veroff sobre las pruebas en lógica intuicionista podría tener sugerencias útiles para automatizar una prueba de este tipo, y el método de esbozos de pruebas podría tener sugerencias útiles aquí (ver [8] en el enlace anterior). Este teorema no se puede demostrar en la lógica intuicionista . El artículo de Veroff sobre Proof Sketches podría ser útil aquí para encontrar una prueba automatizada, y hace referencia a OTTER .

axiom       1 CpCqp.
axiom       2 CCpCqrCCpqCpr.
axiom       3 CCNpqCCNpNqp.
axiom       4 CpApq.
axiom       5 CpAqp.
axiom       6 CApqCCprCCqrr.
axiom       7 CCpqCCqpEpq.
D2.1        8 CCpqCCpp.
D8.1        9 Cpp.  
D1.1        10 CpCqCrq.
D1.3        11 CpCCNqrCCNqNrq.
D2.10       12 CCpqCpCrq.
D12.11      13 CpCqCCNrsCCNrNsr.
D1.4        14 CpCqAqr.
D12.14      15 CpCqCrArs.
D1.2        16 CpCCqCrsCCqrCqs.
D2.16       17 CCpCqCrsCpCCqrCqs.
D17.13      18 CpCCqCNrsCqCCNrNsr.
D2.18       19 CCpCqCNrsCpCqCCNrNsr.
D19.15      20 CpCqCCNrNANrsr.
D17.20      21 CpCCqCNrNANrsCqr.
D2.21       22 CCpCqCNrNANrsCpCqr.
D22.10      23 CpCNANqrq.
D17.1       24 CCpqCCrpCrq.
D2.24       25 CCCpqCrpCCpqCrq.
D25.23      26 CCpqCNANprq.
D1.5        27 CpCqArq.
D1.27       28 CpCqCrAsr.
D17.28      29 CpCCqrCqAsr.
D2.29       30 CCpCqrCpCqAsr.

%

D30.26      31 CCpqCNANprAsq.
D2.11       32 CCpCNqrCpCCNqNrq.
D32.31      33 CCpqCCNANprNAsqANpr.
D2.33       34 CCCpqCNANprNAsqCCpqANpr.
D1.9        35 CpCqq.
D34.35      36 CCpqANpq.
D1.10       37 CpCqCrCsr.
D1.17       38 CpCCqCrCstCqCCrsCrt.
D2.38       39 CCpCqCrCstCpCqCCrsCrt.
D17.37      40 CpCCqrCqCsr.
D2.40       41 CCpCqrCpCqCsr.
D41.10      42 CpCqCrCsq.
D1.11       43 CpCqCCNrsCCNrNsr.
D1.43       44 CpCqCrCCNstCCNsNts.
D39.44      45 CpCqCCrCNstCrCCNsNts.
D17.45      46 CpCCqCrCNstCqCrCCNsNts.
D2.46       47 CCpCqCrCNstCpCqCrCCNsNts.
D47.42      48 CpCqCrCCNsNqs.
D39.48      49 CpCqCCrCNsNqCrs.
D17.49      50 CpCCqCrCNsNqCqCrs.
D2.50       51 CCpCqCrCNsNqCpCqCrs.
D51.37      52 CpCqCNqr.
D1.6        53 CpCAqrCCqsCCrss.
D1.53       54 CpCqCArsCCrtCCstt.
D17.54      55 CpCCqArsCqCCrtCCstt.
D2.55       56 CCpCqArsCpCqCCrtCCstt.
D56.1       57 CApqCrCCpsCCqss.
D17.57      58 CApqCCrCpsCrCCqss.
D2.58       59 CCApqCrCpsCApqCrCCqss.
D59.52      60 CANpqCpCCqrr.

%

D1.9        61 CpCqq.
D1.61       62 CpCqCrr.
D17.60      63 CANpqCCpCqrCpr.
D2.63       64 CCANpqCpCqrCANpqCpr.
D64.62      65 CANpqCpq.
D7.36       66 CCANpqCpqECpqANpq.
D66.65      67 ECpqANpq.

Answer 3

En muchos sistemas formales no se tienen ambas cosas $\to$ y $\lor$ En lugar de ello, se define uno de ellos. Por ejemplo, en los sistemas de estilo Hilbert es popular tener $\to$ como una primitiva y definir $\lor$ utilizando esencialmente la equivalencia que usted señala, mientras que en el cálculo secuencial solemos tener $\lor$ y definir $\to$ utilizando su equivalencia. En estos sistemas no es necesario probar esta equivalencia, ya que es cierto por definición .

Otros sistemas, como el de la deducción natural, sí contienen ambos $\to$ y $\lor$ como nociones primitivas. Es entonces un ejercicio fácil demostrar su equivalencia dados los axiomas del sistema. Si tienes curiosidad, puedes buscar la deducción natural y probarla tú mismo.

Answer 4

Aquí hay otro enfoque adaptado de la Lógica Formal de Arthur Prior p. 65-66.

Primeras reglas de formación:

1. Todas las letras minúsculas del alfabeto latino son fórmulas.
2. Si x es una fórmula, entonces $\delta$ x es una fórmula.
3. Si x es una fórmula, entonces N x es una fórmula.
4. Si x y y son fórmulas, entonces C x y es una fórmula (los espacios pueden ser ignorados o insertados libremente).

Dejemos que "0" represente la falsedad y "1" la verdad. Tenemos la siguiente matriz para la implicación "C", la disyunción (o, de manera equivalente alternancia ) "A", y la negación "N".

C | 0  1|  A| 0  1|  N
----------------------
0 | 1  1|  0| 0  1|  1
1*| 0  1|  1| 1  1|  0

Esto nos da las ecuaciones C00 =1, C01=1, C10=0, C11=1, A00=0, A01=1, A10=1, A11=1, N0=1, N1=0.

$\delta$ representa una variable funcional. Parafraseando a Prior, donde x es una fórmula, $\delta$ x representa cualquier función de verdad en la que $\delta$ entra como argumento. $\delta$ a representa cualquier función de verdad de b, como Nb, Abb, Aab, CNba, CCbcCCabCac. $\delta$ b también puede significar la propia b. Sustitución por $\delta$ se produce al poner el argumento de $\delta$ en la posición donde aparece un símbolo " ' ". La notación x / y indica que x debe ser sustituido por y para todas las instancias de x en la fórmula en la que x aparece. Por ejemplo, la instrucción de sustitución $\delta$ /C ' ' en $\delta$ r da como resultado Crr. $\delta$ /C ' A ' p en C $\delta$ r $\delta$ p produce C CrArp CpApp. La sustitución $\delta$ /' en digamos C $\delta$ p $\delta$ La 1 sólo nos hace caer $\delta$ dando lugar a Cp1. $\delta$ /A ' C ' ' en C $\delta$ p A $\delta$ q $\delta$ Na produce C ApCpp A AqCqq CNaANaNa.

Nótese que la función de valoración "v", v(C x y )=C v( x ) v( y ). Además, para la función de valoración v( $\delta$ x )= $\delta$ v( x ).

Ahora resulta que lo siguiente es un metateorema.

Meta-teorema 1: Si v( x )=v( y ), entonces v(C $\delta$ x $\delta$ y )=1. En otras palabras, si x \= y , entonces C $\delta$ x $\delta$ y sigue.

Demostración: Supongamos que v( x )=v( y ). Como v(C00)=1, y v(C11)=1, se deduce que para todo p, v(Cpp)=1. Sustituyendo p/ $\delta$ x en Cpp obtenemos entonces que v(C $\delta$ x $\delta$ x )=1. Como v(C x y )=C v( x ) v( y ), se deduce entonces que C v( $\delta$ x ) v( $\delta$ x )=1. Dado que v( $\delta$ x )= $\delta$ v( x ), se deduce entonces que C $\delta$ v( x ) $\delta$ v( x )=1. Por la suposición inicial, obtenemos entonces que C $\delta$ v( x ) $\delta$ v( y )=1. Dado que v( $\delta$ x )= $\delta$ v( x ) obtenemos entonces que

C v( $\delta$ x ) v( $\delta$ y )=1. A partir de v(C x y )=C v( x ) v( y ) obtenemos así que v(C $\delta$ x $\delta$ y )=1. Por lo tanto, si v( x )=v( y ), entonces v(C $\delta$ x $\delta$ y )=1.

El resultado es que una ecuación como Cxy=z nos da C $\delta$ z $\delta$ Cxy. Las fórmulas sugeridas a partir de las ecuaciones anteriores inmediatamente después de la tabla junto con los axiomas "C $\delta$ 0 C $\delta$ 1 $\delta$ p" y "1", y "C Cpq Cqp Epq" nos dan aquí un conjunto de axiomas.

Sea la notación 1 x / y * C 2-3 indican que en la fórmula 1 x se sustituye por y . Esto coincide con la fórmula que comienza con C tiene 2 como su siguiente parte, y 3 como su última parte. A continuación, separamos la fórmula 3. La notación 4 x / y C 5-C 6-7 indica que 4 coincide con la fórmula C5-C6-7. Como ya tenemos las fórmulas 5 y 6, separamos la fórmula 7.

Para ver cómo procede el plan de escribir la deducción, escribiré el siguiente cálculo:

                         |-C C00 AN00=C 1 AN00=C 1 A10=C 1 1=1
            |-C C0q AN0q-|
            |            |-C C01 AN01=C 1 AN01=C 1 A11=C 1 1=1
 C Cpq ANpq-|
            |            |-C C10 AN10=C 0 AN10=C 0 A00=C 0 0=1
            |-C C1q AN1q-|
                         |-C C11 AN11=C 1 AN11=C 1 A01=C 1 1=1.

Ahora, para escribir una deducción, básicamente podemos movernos de izquierda a derecha aquí. Desde 1, deduciremos C11. Luego de C11 deduciremos C 1 A10. Luego C 1 AN00. Luego C C00 AN00. Una vez que obtenemos C C01 AN01, entonces como tenemos C C00 AN00, podemos obtener C C0q AN0q. Pero, voy a saltar algunos pasos aquí que nos da una prueba más simple. Aquí va:

1 1.

2 C δ1 δC00.

3 C δ1 δC01.

4 C δ0 δC10.

5 C δ1 δC11.

6 C δ0 δA00.

7 C δ1 δA01.

8 C δ1 δA10.

9 C δ1 δA11.

10 C δ1 δN0.

11 C δ0 δN1.

12 C Cpq C Cqp Epq.

13 C δ0 C δ1 δp. (esto no es un axioma o teorema en la lógica intuicionista).

2 δ/' * C1-14

14 C00.

3 δ/' * C1-15

15 C01.

13 δ/C0' * C14-C15-16

16 C0p.

5 δ/' * C1-17

17 C11.

13 δ/C'1 * C15-C17-18

18 Cp1.

18 p/C00 * 19

19 C C00 1.

8 δ/C C00 ' * C19-20

20 C C00 A10.

10 δ/C C00 A'0 * 20-21

21 C C00 AN00.

18 p/C01 * 22

22 C C01 1.

9 δ/CC01' * C22-23

23 C C01 A11.

10 δ/C C01 A'1 * C23-24

24 C C01 AN01.

13 δ/ C C0' AN0', p/q * C21-C24-25 

25 C C0q AN0q.

16 p/AN10 * 26

26 C 0 AN10.

4 δ/C ' AN10 * C26-27

27 C C10 AN10.

18 p/C11 * 28

28 C C11 1.

7 δ/C C11 ' * C28-29

29 C C11 A01.

11 δ/C C11 A'1 * C29-30

30 C C11 AN11.

13 δ/C C1' AN1', p/q *C27-C30-31

31 C C1q AN1q.

14 δ/C C'q AN'q * C25-C31-32

32 C Cpq ANpq.

18 p/AN00 * 33

33 C AN00 1.

2 δ/C AN00 ' * C33-34

34 C AN00 C00.

18 p/AN01 * 35

35 C AN01 1.

3 δ/C AN01 ' * C35-36

36 C AN01 C01.

13 δ /C AN0' C0', p/q * C34-C36-37

37 C AN0q C0q.

6 δ/C'0 * C14-38

38 C A00 0.

11 δ/C A'0 0 * C38-39

39 C AN10 0.

4 δ/C AN10 ' * C39-40

40 C AN10 C10.

18 p/AN11 * 41

41 C AN11 1.

5 δ/C AN11 ' * C41-42

42 C AN11 C11.

13 δ/C AN1' C1', p/q * C40-C42-43

43 C AN1q C1q.

37 δ/C AN'q C'q * C37-C43-44

44 C ANpq Cpq.

 12 p/Cpq, q/ANpq * C32-C44-45

45 E Cpq ANpq.