Usando as dez inferências do Sistema de Dedução Natural, comprova as leis de DeMorgan .

As regras da dedução natural

• Introdução à Negação: {(P → Q), (P → ¬Q)} ⊢ ¬P

• Eliminação de Negação: {(¬P → Q), (¬P → ¬Q)} ⊢ P

• E Introdução: {P, Q} ⊢ P ʌ Q

• E eliminação: P ʌ Q ⊢ {P, Q}

• Ou Introdução: P ⊢ {(P ∨ Q),(Q ∨ P)}

• Ou eliminação: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

• Iff Introdução: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

• Eliminação Iff: (P ≡ Q) ⊢ {(P → Q), (Q → P)}

• Se Introdução: (P ⊢ Q) ⊢ (P → Q)

• Se Eliminação: {(P → Q), P} ⊢ Q

Estrutura de prova

Cada declaração em sua prova deve ser o resultado de uma das dez regras aplicadas a algumas proposições derivadas anteriormente (sem lógica circular) ou de uma suposição (descrita abaixo). Cada regra opera em algumas proposições no lado esquerdo do ⊢(operador de conseqüência lógica) e cria qualquer número de proposições no lado direito. A introdução ao If funciona de maneira um pouco diferente do restante dos operadores (descrito em detalhes abaixo). Opera através de uma declaração que é o consequente lógico de outra.

Exemplo 1

Você tem as seguintes instruções:

{(P → R), Q}

Você pode usar E Introdução para fazer:

(P → R) ʌ Q

Exemplo 2

Você tem as seguintes instruções:

{(P → R), P}

Você pode usar If Elimination para fazer:

R

Exemplo 3

Você tem as seguintes instruções:

(P ʌ Q)

Você pode usar And Elimination para fazer:

P

ou fazer:

Q

Propagação da Suposição

Você pode, a qualquer momento, assumir qualquer afirmação que desejar. Qualquer declaração derivada dessas suposições será "dependente" delas. As declarações também dependerão das suposições nas quais as declarações dos pais se baseiam. A única maneira de eliminar suposições é por If Introduction. Para Se introdução, você começa com uma Declaração Qque depende de uma declaração Pe termina com (P → Q). A nova declaração é dependente de cada suposição Qbaseia-se em , exceto para a assunção P. Sua declaração final não deve se basear em suposições.

Especificidades e pontuação

Você construirá uma prova para cada uma das duas leis de DeMorgan usando apenas as 10 inferências do Cálculo de dedução natural.

As duas regras são:

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

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

Sua pontuação é o número de inferências usadas mais o número de suposições feitas. Sua declaração final não deve se basear em nenhuma hipótese (ou seja, deve ser um teorema).

Você é livre para formatar sua prova como achar melhor.

Você pode transportar qualquer lema de uma prova para outra sem nenhum custo para pontuar.

Prova de exemplo

Vou provar isso (P and not(P)) implies Q

(Cada ponto de marcador é +1)

• Assumir not (Q)

• Assumir (P and not(P))

• Usando And Elim em (P and not(P))derivar{P, not(P)}

• Uso e introdução sobre Pe not(Q)derivar(P and not(Q))

• Use And Elim na declaração derivada para fazer P

A nova Pproposição é diferente da outra que derivamos anteriormente. Ou seja, é dependente das suposições not(Q)e (P and not(P)). Considerando que a declaração original era apenas dependente (P and not(P)). Isso nos permite fazer:

• Se Introdução à Pintrodução not(Q) implies P(ainda dependente da (P and not(P))suposição)

• Use And Introduction not(P)e not(Q)(da etapa 3) para derivar(not(P) and not(Q))

• Use And Elim na declaração que você derivou para fazer not(P) (agora dependente not(Q))

• Se Introdução sobre a nova not(P)introduçãonot(Q) implies not(P)

• Agora vamos usar a eliminação da negação not(Q) implies not(P)e not(Q) implies PderivarQ

Isso Qdepende apenas da suposição de (P and not(P))que podemos concluir a prova com

• Se a introdução Qderiva(P and not(P)) implies Q

Esta prova marca um total de 11.

Pontuação: 81

Cada linha deve valer 1 ponto. As leis de De Morgan são encontradas nas declarações (3) e (6). Os rótulos entre parênteses indicam a (s) declaração (ões) anterior (s) em que uma linha depende se eles não forem imediatamente 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]

Pontuação: 59

Explicação

Usarei uma árvore como estrutura para a prova, pois acho esse estilo bastante legível. Cada linha é anotada pela contagem de regras usadas, por exemplo, o "Exemplo 1" no desafio seria representado como esta árvore (crescendo de baixo para cima):

Observe que o desconhecido conta A, B e também a suposição Γ - então esse não é um teorema. Para demonstrar como provar um teorema, vamos assumir A e usar uma introdução Or da seguinte maneira:

Agora, isso ainda depende da suposição A, mas podemos derivar um teorema aplicando uma introdução ao If:

Então, conseguimos derivar o teorema ⊢ A → ( A ∨ B ) em um total de 3 etapas (1 suposição e 2 regras aplicadas).

Com isso, podemos provar algumas novas regras que nos ajudam a provar as leis de DeMorgan.

Regras adicionais

Vamos primeiro derivar o Princípio da Explosão e denotá-lo com PE em outras provas:

A partir disso, derivamos outra forma: A ¬ ¬ A → X - vamos chamá-lo de CPE :

Precisamos de outro em que o termo negado (¬) seja uma suposição e o refira como CPE ^- :

Das duas regras que acabamos de derivar ( CPE e CPE ^- ), podemos derivar uma importante regra Double Negation :

A próxima coisa a fazer é provar algo como Modus Tollens - daí o MT :

Lemas

Lema A

Lema A1

Precisamos da seguinte regra duas vezes:

Lema A

Ao instanciar o lema recentemente provado duas vezes, podemos mostrar uma direção de uma equivalência, precisaremos dele na prova final:

Lema B

Para mostrar outra direção, precisamos fazer duas vezes algumas coisas bastante repetitivas (para os argumentos A e B em ( A ∨ B )) - isso significa que aqui eu poderia testar a prova ainda mais.

Lema B1 '

Lema B1

Lema B2 '

Lema B2

Lema B

Finalmente, a conclusão de B1 e B2 :

Prova real

Uma vez que provamos essas duas afirmações:

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

Podemos provar a primeira equivalência (¬ ( A ∨ B ) ¬ ¬ A ʌ ¬ B )) da seguinte maneira:

E com a regra recém-comprovada, juntamente com a Iff-Elimination, também podemos provar a segunda equivalência:

Não tenho certeza sobre a pontuação - se eu fiz direito, informe-me se houver algo errado.

Explicação

Fonte

Se alguém quiser a fonte tex (precisa de mathpartir ):

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}:

Pontuação: 65

As leis de Morgan são as linhas 30 e 65.

(Não fiz nenhum esforço específico para jogar isso, por exemplo, para ver se há algumas provas repetidas que poderiam ser abstraídas no início.)

 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