Probar las leyes de DeMorgan

21

El uso de las diez inferencias del Sistema de Deducción Natural prueba las leyes de DeMorgan .

Las reglas de la deducción natural

  • Introducción a la negación: {(P → Q), (P → ¬Q)} ⊢ ¬P

  • Eliminación de negación: {(¬P → Q), (¬P → ¬Q)} ⊢ P

  • E Introducción: {P, Q} ⊢ P ʌ Q

  • Y eliminación: P ʌ Q ⊢ {P, Q}

  • O Introducción: P ⊢ {(P ∨ Q),(Q ∨ P)}

  • O eliminación: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

  • Introducción de Iff: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

  • Eliminación de Iff: (P ≡ Q) ⊢ {(P → Q), (Q → P)}

  • Si Introducción: (P ⊢ Q) ⊢ (P → Q)

  • Si eliminación: {(P → Q), P} ⊢ Q

Estructura de prueba

Cada declaración en su prueba debe ser el resultado de una de las diez reglas aplicadas a algunas proposiciones derivadas previamente (sin lógica circular) o una suposición (descrita a continuación). Cada regla opera a través de algunas proposiciones en el lado izquierdo del (operador de consecuencia lógica) y crea cualquier número de proposiciones desde el lado derecho. La Introducción If funciona de manera ligeramente diferente al resto de los operadores (se describe en detalle a continuación). Opera a través de una declaración que es el consecuente lógico de otra.

Ejemplo 1

Tienes las siguientes declaraciones:

{(P → R), Q}

Puede usar And Introduction para hacer:

(P → R) ʌ Q

Ejemplo 2

Tienes las siguientes declaraciones:

{(P → R), P}

Puede usar If Elimination para hacer:

R

Ejemplo 3

Tienes las siguientes declaraciones:

(P ʌ Q)

Puede usar And Elimination para hacer:

P

o hacer:

Q

Propagación de suposiciones

En cualquier momento, puede asumir cualquier declaración que desee. Cualquier declaración derivada de estos supuestos será "dependiente" de ellos. Las declaraciones también dependerán de los supuestos en los que se basan sus declaraciones principales. La única forma de eliminar los supuestos es mediante la introducción If Para la introducción If, comienza con una Declaración Qque depende de una declaración Py termina con (P → Q). La nueva declaración depende de cada hipótesis Qse basa en excepto por supuesto P. Su declaración final no debe basarse en suposiciones.

Detalles y puntuación

Construirá una prueba para cada una de las dos leyes de DeMorgan utilizando solo las 10 inferencias del cálculo de deducción natural.

Las dos reglas son:

¬(P ∨ Q) ≡ ¬P ʌ ¬Q

¬(P ʌ Q) ≡ ¬P ∨ ¬Q

Su puntaje es el número de inferencias utilizadas más el número de suposiciones hechas. Su declaración final no debe basarse en ninguna suposición (es decir, debe ser un teorema).

Usted es libre de formatear su prueba como mejor le parezca.

Puede transferir cualquier Lemmas de una prueba a otra sin costo alguno para calificar.

Prueba de ejemplo

Demostraré que (P and not(P)) implies Q

(Cada punto de viñeta es +1 punto)

  • Asumir not (Q)

  • Asumir (P and not(P))

  • Usando y Elim en (P and not(P))deriva{P, not(P)}

  • Uso e introducción sobre Py not(Q)para derivar(P and not(Q))

  • Use y elimine en la declaración que acaba de derivar para hacer P

La nueva Ppropuesta es diferente de la otra que derivamos anteriormente. Es decir, depende de los supuestos not(Q)y (P and not(P)). Mientras que la declaración original solo dependía de (P and not(P)). Esto nos permite hacer:

  • Si Introducción al Pintroducir not(Q) implies P(todavía depende de la (P and not(P))suposición)

  • Uso e introducción en not(P)y not(Q)(desde el paso 3) para derivar(not(P) and not(Q))

  • Use And Elim en la declaración que se acaba de derivar not(P) (ahora depende de not(Q))

  • Si Introducción sobre la nueva not(P)introducciónnot(Q) implies not(P)

  • Ahora utilizaremos la eliminación de negaciones en not(Q) implies not(P)y not(Q) implies Ppara derivarQ

Esto Qdepende solo de la suposición (P and not(P))para que podamos terminar la prueba con

  • Si Introducción Qa derivar(P and not(P)) implies Q

Esta prueba tiene un total de 11.

Asistente de trigo
fuente
77
Aunque el consenso sobre el meta es claro, no todos lo habrán visto aún, así que esto es solo para resaltar que el golf de prueba es el tema .
Trichoplax
2
Creo que deberías explicar la estructura de las pruebas y (el símbolo tampoco se muestra en el móvil).
xnor
3
Creo que las explicaciones definitivamente ayudan. Lo que me parece más útil sería un ejemplo trabajado y calificado de alguna prueba simple que incluya If-Introduction y supuestos, preferiblemente anidados. Tal vez de contrapositivo?
xnor
1
En su ejemplo, creo que los dos primeros supuestos tendrían que cambiarse; en ninguna parte indica que (P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))(en este caso, ¬Q ⊢ ((P ʌ ¬P) ⊢ P)to (P ʌ ¬P) ⊢ (¬Q ⊢ P)was used).
LegionMammal978
1
¿Se le permite probar varias cosas en un solo "contexto de suposición" y luego extraer múltiples enunciados de implicación para ahorrar en cuántas "líneas de suposición" se necesitan? por ejemplo, (assume (P/\~P); P,~P by and-elim; (assume ~Q; P by assumption; ~P by assumption); ~Q->P by impl-intro; ~Q->~P by impl-intro; Q by neg-elim); P/\~P->Q by impl-intropara obtener una puntuación de 9?
Daniel Schepler

Respuestas:

6

Puntuación: 81

Cada línea debe valer 1 punto. Las leyes de De Morgan se encuentran en las declaraciones (3) y (6). Las etiquetas entre paréntesis indican las declaraciones anteriores de las que depende una línea si no están inmediatamente anteriores.

(a) assume P {
    (aa) P ^ P
    (ab) P
    (ac) P v Q
} (a1) P -> P
  (a2) P -> P v Q
(1) assume ~P ^ ~Q {
    (1a) assume P v Q {
        (1aa) assume Q {
            (1aaa) assume ~P {
                (1aaaa) Q ^ Q [1aa]
                (1aaab) Q
                (1aaac) ~Q [1]
            } (1aaa1) ~P -> Q
              (1aaa2) ~P -> ~Q
            (1aab) P
        } (1aa1) Q -> P
        P [1a, a1, 1aa1]
        ~P [1]
    } (1a1) P v Q -> P
      (1a2) P v Q -> ~P
    (1b) ~(P v Q)
} (11) ~P ^ ~Q -> ~(P v Q)
(2) assume ~(P v Q) {
    (2a) ~(P v Q) ^ ~(P v Q)
    (2b) assume P {
        (2aa) ~(P v Q) [2a]
    } (2b1) P -> ~(P v Q)
    (2c) ~P [a2, 2b1]
    (2d) assume Q {
        (2da) ~(P v Q) [2a]
        (2db) P v Q
    } (2d1) Q -> ~(P v Q)
      (2d2) Q -> P v Q
    (2e) ~Q
    (2f) ~P ^ ~Q
} (21) ~(P v Q) -> ~P ^ ~Q
(3) ~(P v Q) == ~P ^ ~Q [11, 21]
(4) assume ~P v ~Q {
    (4a) assume ~P {
        (4aa) assume P ^ Q {
            (4aaa) P
            (4aab) ~P ^ ~P [4a]
            (4aac) ~P
        } (4aa1) P ^ Q -> P
          (4aa2) P ^ Q -> ~P
        (4ab) ~(P ^ Q)
    } (4a1) ~P -> ~(P ^ Q)
    (4b) assume ~Q {
        (4ba) assume P ^ Q {
            (4baa) Q
            (4bab) ~Q ^ ~Q [4b]
            (4bac) ~Q
        } (4ba1) P ^ Q -> Q
          (4ba2) P ^ Q -> ~Q
        (4bb) ~(P ^ Q)
    } (4b1) ~P -> ~(P ^ Q)
    (4c) ~(P ^ Q) [4, 4a1, 4b1]
} (41) ~P v ~Q -> ~(P ^ Q) 
(5) assume ~(P ^ Q) {
    (5a) assume ~(~P v ~Q) {
        (5aa) ~(~P v ~Q) ^ ~(P ^ Q) [5, 5a]
        (5ab) assume ~P {
            (5aba) ~P v ~Q
            (5abb) ~(~P v ~Q) [5aa]
        } (5ab1) ~P -> ~P v ~Q
          (5ab2) ~P -> ~(~P v ~Q)
        (5ac) P
        (5ad) assume ~Q {
            (5ada) ~P v ~Q
            (5adb) ~(~P v ~Q) [5aa]
        } (5ad1) ~Q -> ~P v ~Q
          (5ad2) ~Q -> ~(~P v ~Q)
        (5ae) Q
        (5af) P ^ Q [5ac, 5ae]
        (5ag) ~(P ^ Q) [5aa]
    } (5a1) ~(~P v ~Q) -> P ^ Q
      (5a2) ~(~P v ~Q) -> ~(P ^ Q)
    (5b) ~P v ~Q
} (51) ~(P ^ Q) -> ~P v ~Q
(6) ~(P ^ Q) == ~P v ~Q [41, 51]
Feersum
fuente
4

Puntuación: 59

Explicación

Usaré una estructura similar a un árbol para la prueba, ya que este estilo me parece bastante legible. Cada línea se anota mediante el recuento de reglas utilizadas, por ejemplo, el "Ejemplo 1" en el desafío se representaría como este árbol (creciendo de abajo hacia arriba):

AIntro

Tenga en cuenta los recuentos desconocidos A, B y también la suposición Γ, por lo que este no es un teorema. Para demostrar cómo demostrar un teorema, asumamos A y usemos una introducción Or de la siguiente manera:

OIntro

Ahora esto todavía depende de la suposición A, pero podemos derivar un teorema aplicando una introducción If:

Intro

Entonces pudimos derivar el teorema ⊢ A → ( AB ) en un total de 3 pasos (1 supuesto y 2 reglas aplicadas).

Con esto podemos pasar a probar algunas reglas nuevas que nos ayudan a probar las Leyes de DeMorgan.

Reglas Adicionales

Primero derivemos el Principio de Explosión y denotémoslo con PE en pruebas adicionales:

EDUCACIÓN FÍSICA

De esto derivamos otra forma de ello: A ⊢ ¬ AX - lo llamaremos CPE :

EDUCACIÓN FÍSICA

Necesitaremos otro donde el término negado (¬) sea una suposición y nos referiremos a él como CPE - :

NCPE

De las dos reglas que acabamos de derivar ( CPE y CPE - ), podemos derivar una regla importante Doble Negación :

DN

Lo siguiente que debe hacer es probar algo como Modus Tollens , por lo tanto, MT :

MONTE

Lemas

Lema A

Lema A1

Necesitaremos la siguiente regla dos veces:

LA1

Lema A

Al crear instancias del lema recién probado dos veces, podemos mostrar una dirección de equivalencia, la necesitaremos en la prueba final:

LA

Lema B

Para mostrar otra dirección, tendremos que hacer dos veces algunas cosas bastante repetitivas (tanto para los argumentos A como para B en ( AB )), esto significa que aquí podría jugar golf la prueba aún más.

Lema B1 '

LB1_

Lemma B1

LB1

Lema B2 '

LB2_

Lema B2

LB2

Lema B

Finalmente la conclusión de B1 y B2 :

LB

Prueba real

Una vez que probamos estas dos declaraciones:

  • Lema A : ⊢ ( AB ) → ¬ (¬ A ʌ ¬ B )
  • Lema B : ⊢ ¬ ( AB ) → (¬ A ʌ ¬ B )

Podemos probar la primera equivalencia (¬ ( AB ) ≡ ¬ A ʌ ¬ B )) de la siguiente manera:

P1

Y con la regla probada junto con Iff-Elimination también podemos probar la segunda equivalencia:

P2

No estoy seguro sobre el puntaje: si lo hice bien, avíseme si hay algo mal.

Explicación

Fuente

Si alguien quiere la fuente de texto (necesita matemática ):

In the following a rule \textbf{XYZ'} will denote the rule XYZ's second last
step, for example \textbf{PE'} will be $ A \land \lnot A \vdash X $.

\section*{Principle of Explosion [PE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=10]
    {\inferrule*[Left=$\lnot$-Elim,Right=9]
      {\inferrule*[Left=$\to$-Intro,Right=4]
        {\inferrule*[Left=$\land$-Elim,Right=3]
          {\inferrule*[Left=Axiom,Right=2]
            { }
            { A \land \lnot A, \lnot X \vdash A \land \lnot A }
          }
          { A \land \lnot A, \lnot X \vdash A }
        }
        { A \land \lnot A \vdash \lnot X \to A } \\
       \inferrule*[Right=$\to$-Intro,Left=4]
          {\inferrule*[Right=$\land$-Elim,Left=3]
            {\inferrule*[Right=Axiom,Left=2]
              { }
              { A \land \lnot A, \lnot X \vdash A \land \lnot A }
            }
            { A \land \lnot A, \lnot X \vdash \lnot A }
          }
        { A \land \lnot A \vdash \lnot X \to \lnot A }
      }
      { A \land \lnot A \vdash X }
    }
    { \vdash (A \land \lnot A) \to X }
\end{mathpar}

\section*{Conditioned PE [CPE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=5]
  {\inferrule*[Left=$\to$-Elim,Right=4]
    {\inferrule*[Left=$\land$-Intro,Right=3]
      {\inferrule*[Left=Axiom,Right=1]
        { } { A \vdash A } \\
       \inferrule*[Right=Axiom,Left=1]
        { } { \lnot A \vdash \lnot A }
      }
      { A, \lnot A \vdash A \land \lnot A } \\
     \inferrule*[Right=PE,Left=0]
      { } { \vdash (A \land \lnot A) \to X }
    }
    { A, \lnot A \vdash X }
  }
  { A \vdash \lnot A \to X }
\end{mathpar}

to get \textbf{CPE$^-$}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=1]
    {\inferrule*[Left=CPE',Right=0]
      { }
      { A, \lnot A \vdash X }
    }
    { \lnot A \vdash A \to X }
\end{mathpar}

\section*{Double Negation [DN]}

\begin{mathpar}
  \inferrule*[Left=$\equiv$-Intro,Right=5]
    {\inferrule*[Left=$\to$-Intro,Right=2]
      {\inferrule*[Left=$\lnot$-Elim,Right=1]
        {\inferrule*[Left=CPE$^-$,Right=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to X } \\
          \inferrule*[Right=CPE$^-$,Left=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to \lnot X }
        }
        { \lnot\lnot A \vdash A }
      }
      { \vdash \lnot\lnot A \to A } \\ \\ \\
      \inferrule*[Left=$\to$-Intro,Right=2]
        {\inferrule*[Left=$\lnot$-Intro,Right=1]
          {\inferrule*[Left=CPE,Right=0]
            { }
            {  A \vdash \lnot A \to X } \\
            \inferrule*[Right=CPE,Left=0]
            { }
            { A \vdash \lnot A \to \lnot X }
          }
          { A \vdash \lnot\lnot A }
        }
        { \vdash A \to \lnot\lnot A }
    }
    { \vdash \lnot\lnot A \equiv A  }
\end{mathpar}

\section*{Modus Tollens [MT]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=6]
    {\inferrule*[Left=$\lnot$-Intro,Right=5]
      {\inferrule*[Left=Axiom,Right=1]
       { }
       { A \to \lnot B \vdash A \to \lnot B } \\
       \inferrule*[Right=$\to$-Intro,Left=3]
         {\inferrule*[Right=Axiom,Left=2]
           { }
           { A, B \vdash B }
         }
         { B \vdash A \to B }
       }
      { A \to \lnot B, B \vdash \lnot A }
    }
    { A \to \lnot B \vdash B \to \lnot A }
\end{mathpar}

\section*{Lemma A}

\textbf{Lemma A1}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=9]
    {\inferrule*[Left=$\lor$-Elim,Right=8]
       { \inferrule*[Left=CPE,Right=3]
          {\inferrule*[Left=$\land$-Elim,Right=2]
            {\inferrule*[Left=Axiom,Right=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash B}
          }
          { A \land B \vdash \lnot B \to X } \\
         \inferrule*[Right=CPE,Left=3]
          {\inferrule*[Right=$\land$-Elim,Left=2]
            {\inferrule*[Right=Axiom,Left=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash A }
          }
          { A \land B \vdash \lnot A \to X } \\ \\ \\
         \inferrule*[Right=Axiom,Left=1]
          { }
          { \lnot A \lor \lnot B \vdash \lnot A \lor \lnot B }
       }
       { A \land B, \lnot A \lor \lnot B \vdash X }
    }
    { \lnot A \lor \lnot B \vdash (A \land B) \to X }
\end{mathpar}

\textbf{Lemma A}:
ბიმო
fuente
1
Por lo que puedo decir, el sistema de prueba de deducción natural aquí no permite probar una declaración una vez con variables de proposición genéricas y luego instanciarla. Por lo tanto, cada vez que tenga una instanciación diferente de uno de sus lemas en términos de variables Py Q, tendría que contar sus pasos por separado en el total final. (En otras palabras, el sistema de prueba no permite directamente probar lemas de "segundo orden" como "para todas las proposiciones A y B A/\B -> B/\A" , y luego usarlo para probar ambas P/\(Q/\R) -> (Q/\R)/\Py (P/\Q)/\R -> R/\(P/\Q).)
Daniel Schepler
@DanielSchepler: Sí, pero no hay dependencias circulares y, en la regla que establece , puede transferir cualquier Lemmas de una prueba a otra sin costo alguno para calificar. , así que eso estará bien. Editar : De hecho, si eso no estuviera permitido, estoy seguro de que esta pregunta solo tendría una respuesta elegible.
ბიმო
Estaba interpretando que eso significa simplemente que podría tener algunas pruebas comunes de un conjunto de fórmulas concretas compartidas entre las pruebas de las dos declaraciones finales.
Daniel Schepler
1

Puntuación: 65

Las leyes de Morgan son la línea 30 y la línea 65.

(No he hecho ningún esfuerzo particular para jugar golf, por ejemplo, para ver si hay algunas pruebas repetidas que podrían resumirse al principio).

 1. assume ~(P\/Q)
 2.   assume P
 3.     P\/Q  by or-introl, 2
 4.   P -> P\/Q  by impl-intro, 2, 3
 5.   P -> ~(P\/Q)  by impl-intro, 2, 1
 6.   ~P  by neg-intro, 4, 5
 7.   assume Q
 8.     P\/Q  by or-intror, 7
 9.   Q -> P\/Q  by impl-intro, 7, 8
10.   Q -> ~(P\/Q) by impl-intro, 7, 1
11.   ~Q  by neg-intro, 9, 10
12.   ~P /\ ~Q  by and-intro, 6, 11
13. ~(P\/Q) -> ~P/\~Q  by impl-intro, 1, 12
14. assume ~P /\ ~Q
15.   ~P, ~Q  by and-elim, 14
16.   assume P \/ Q
17.     assume P
18.     P -> P  by impl-intro, 17, 17
19.     assume Q
20.       assume ~P
21.       ~P -> Q  by impl-intro, 20, 19
22.       ~P -> ~Q  by impl-intro, 20, 15
23.       P  by neg-elim, 21, 22
24.     Q -> P  by impl-intro, 19, 23
25.     P  by or-elim, 16, 18, 24
26.   P\/Q -> P  by impl-elim, 16, 25
27.   P\/Q -> ~P  by impl-elim, 16, 15
28.   ~(P\/Q)  by neg-intro, 26, 27
29. ~P/\~Q -> ~(P\/Q)  by impl-intro, 14, 28
30. ~(P\/Q) <-> ~P/\~Q  by iff-intro, 13, 29
31. assume ~(P/\Q)
32.   assume ~(~P\/~Q)
33.     assume ~P
34.       ~P\/~Q  by or-introl, 33
35.     ~P -> ~P\/~Q  by impl-intro, 33, 34
36.     ~P -> ~(~P\/~Q)  by impl-intro, 33, 32
37.     P  by neg-elim, 35, 36
38.     assume ~Q
39.       ~P\/~Q  by or-intror, 38
40.     ~Q -> ~P\/~Q  by impl-intro, 38, 39
41.     ~Q -> ~(~P\/~Q)  by impl-intro, 38, 32
42.     Q  by neg-elim, 40, 41
43.     P /\ Q  by and-intro, 37, 42
44.   ~(~P\/~Q) -> P /\ Q  by impl-intro, 32, 43
45.   ~(~P\/~Q) -> ~(P /\ Q)  by impl-intro, 32, 31
46.   ~P \/ ~Q  by neg-elim, 44, 45
47. ~(P/\Q) -> ~P\/~Q  by impl-intro, 31, 46
48. assume ~P\/~Q
49.   assume ~P
50.     assume P/\Q
51.       P, Q  by and-elim, 50
52.     P/\Q -> P  by impl-intro, 50, 51
53.     P/\Q -> ~P  by impl-intro, 50, 49
54.     ~(P/\Q)  by neg-intro, 52, 53
55.   ~P -> ~(P/\Q)  by impl-intro, 49, 54
56.   assume ~Q
57.     assume P/\Q
58.       P, Q  by and-elim, 57
59.     P/\Q -> Q  by impl-intro, 57, 58
60.     P/\Q -> ~Q  by impl-intro, 57, 56
61.     ~(P/\Q)  by neg-intro, 59, 60
62.   ~Q -> ~(P/\Q)  by impl-intro, 56, 61
63.   ~(P/\Q)  by or-elim, 48, 55, 62
64. ~P\/~Q -> ~(P/\Q)  by impl-intro, 48, 63
65. ~(P/\Q) <-> ~P\/~Q  by iff-intro, 47, 64
Daniel Schepler
fuente