Korzystanie z dziesięciu wniosków Systemu Naturalnego Odliczenia dowodzi praw DeMorgan .

Zasady odliczenia naturalnego

• Wprowadzenie do negacji: {(P → Q), (P → ¬Q)} ⊢ ¬P

• Eliminacja negacji: {(¬P → Q), (¬P → ¬Q)} ⊢ P

• I wprowadzenie: {P, Q} ⊢ P ʌ Q

• I eliminacja: P ʌ Q ⊢ {P, Q}

• Lub Wprowadzenie: P ⊢ {(P ∨ Q),(Q ∨ P)}

• Lub eliminacja: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

• Iff Wprowadzenie: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

• Eliminacja Iff: (P ≡ Q) ⊢ {(P → Q), (Q → P)}

• Jeśli wprowadzenie: (P ⊢ Q) ⊢ (P → Q)

• Jeśli eliminacja: {(P → Q), P} ⊢ Q

Struktura dowodu

Każde stwierdzenie w twoim dowodzie musi być wynikiem jednej z dziesięciu reguł zastosowanych do niektórych wcześniej wyprowadzonych zdań (bez logiki kołowej) lub założenia (opisanego poniżej). Każda reguła działa na niektóre zdania po lewej stronie ⊢(operator konsekwencji logicznych) i tworzy dowolną liczbę zdań z prawej strony. If Wprowadzenie działa nieco inaczej niż reszta operatorów (szczegółowo opisane poniżej). Działa w ramach jednej instrukcji, która jest logiczną konsekwencją innej.

Przykład 1

Masz następujące stwierdzenia:

{(P → R), Q}

Możesz użyć And Introduction, aby:

(P → R) ʌ Q

Przykład 2

Masz następujące stwierdzenia:

{(P → R), P}

Możesz użyć If Elimination, aby:

R

Przykład 3

Masz następujące stwierdzenia:

(P ʌ Q)

Możesz użyć And Elimination, aby:

P

lub zrobić:

Q

Propagacja założenia

Możesz w dowolnym momencie przyjąć dowolne oświadczenie. Wszelkie stwierdzenia wynikające z tych założeń będą na nich „polegać”. Oświadczenia będą również zależeć od założeń, na których opierają się ich oświadczenia nadrzędne. Jedynym sposobem na wyeliminowanie założeń jest If Wprowadzenie. W przypadku wprowadzenia rozpoczyna się od instrukcji, Qktóra jest zależna od instrukcji Pi kończy się na (P → Q). Nowe stwierdzenie opiera się na każdym założeniu, Qz wyjątkiem założenia P. Twoje ostateczne oświadczenie nie powinno opierać się na żadnych założeniach.

Specyfika i punktacja

Zbudujesz jeden dowód dla każdego z dwóch praw DeMorgan, używając tylko 10 wniosków z naturalnego rachunku dedukcyjnego.

Dwie zasady to:

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

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

Twój wynik to liczba użytych wnioskowania plus liczba poczynionych założeń. Twoje ostateczne stwierdzenie nie powinno opierać się na żadnych założeniach (tj. Powinno być twierdzeniem).

Możesz dowolnie sformatować dowód, jeśli uznasz to za stosowne.

Możesz przenosić dowolne lematy z jednego dowodu na drugi bez ponoszenia kosztów.

Przykład dowodu

Udowodnię to (P and not(P)) implies Q

(Każdy punkt jest +1 punkt)

• Założyć not (Q)

• Założyć (P and not(P))

• Używanie And Elim przy (P and not(P))wyprowadzaniu{P, not(P)}

• Wykorzystanie i wprowadzenie na temat Pi not(Q)czerpać(P and not(Q))

• Użyj And Elim na wyciągu właśnie utworzonym do wykonania P

Nowa Ppropozycja różni się od drugiej, którą wyprowadzamy wcześniej. Mianowicie zależy od założeń not(Q)i (P and not(P)). Podczas gdy oryginalne stwierdzenie opierało się tylko na (P and not(P)). To pozwala nam na:

• Jeśli wprowadzenie po Pwprowadzeniu not(Q) implies P(nadal opiera się na (P and not(P))założeniu)

• Użyj i wprowadzenie na ( not(P)i not(Q)od kroku 3), aby uzyskać(not(P) and not(Q))

• Użyj And Elim na wyciągu właśnie uzyskanym not(P) (teraz zależnym not(Q))

• Jeśli wprowadzenie nowego not(P)wprowadzenianot(Q) implies not(P)

• Teraz będziemy używać eliminacji negacji not(Q) implies not(P)i not(Q) implies PczerpaćQ

Jest Qto zależne tylko od założenia, (P and not(P))więc możemy dokończyć dowód

• Jeśli wprowadzenie, Qaby wyprowadzić(P and not(P)) implies Q

Wynik ten wynosi 11.

Wynik: 81

Każda linia powinna być warta 1 punkt. Prawa De Morgana znajdują się w stwierdzeniach (3) i (6). Etykiety w nawiasach oznaczają poprzednie oświadczenie, od którego zależy wiersz, jeśli nie są one bezpośrednio poprzedzające.

(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]

Wynik: 59

Wyjaśnienie

Jako dowód użyję struktury przypominającej drzewo, ponieważ uważam, że ten styl jest dość czytelny. Każda linia jest opatrzona adnotacjami o liczbie użytych reguł, na przykład „Przykład 1” w wyzwaniu byłby reprezentowany jako drzewo (rosnące od dołu do góry):

Zwróć uwagę, że nieznane liczby A, B, a także założenie Γ - więc to nie jest twierdzenie. Aby zademonstrować, jak udowodnić twierdzenie, załóżmy A i zastosujmy wprowadzenie w następujący sposób:

Teraz nadal zależy to od założenia A, ale możemy wyprowadzić twierdzenie, stosując wprowadzenie If:

Byliśmy więc w stanie wyprowadzić twierdzenie ⊢ A → ( A ∨ B ) w sumie 3 etapach (1 założenie i 2 zastosowane reguły).

Dzięki temu możemy dalej udowodnić kilka nowych zasad, które pomogą nam udowodnić prawa DeMorgan.

Dodatkowe zasady

Najpierw zacznijmy od zasady eksplozji i oznaczmy ją PE w dalszych dowodach:

Z tego czerpiemy inną formę: A ⊢ ¬ A → X - nazwiemy CPE :

Będziemy potrzebować innego, w którym zanegowany termin (¬) jest założeniem i będziemy go nazywać CPE ^- :

Z dwóch reguł, które właśnie wyprowadziliśmy ( CPE i CPE ^- ), możemy wyprowadzić ważną zasadę Podwójna negacja :

Następną rzeczą jest udowodnienie czegoś takiego jak Modus Tollens - stąd MT :

Lemmy

Lemma A

Lemma A1

Będziemy potrzebować następującej zasady dwa razy:

Lemma A

Poprzez dwukrotne utworzenie właśnie udowodnionego lematu możemy wskazać jeden kierunek równoważności, będziemy go potrzebować w ostatecznym dowodzie:

Lemat B.

Aby wskazać inny kierunek, musimy zrobić dwa razy kilka dość powtarzających się czynności (dla obu argumentów A i B w ( A ∨ B )) - oznacza to, że mógłbym tutaj jeszcze udoskonalić dowód.

Lemma B1 '

Lemma B1

Lemma B2 '

Lemma B2

Lemat B.

Wreszcie konkluzja B1 i B2 :

Rzeczywisty dowód

Raz udowodniliśmy te dwa stwierdzenia:

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

Pierwszą równoważność możemy udowodnić (¬ ( A ∨ B ) ≡ ¬ A ʌ ¬ B )) w następujący sposób:

A dzięki właśnie udowodnionej zasadzie wraz z eliminacją Iffa możemy udowodnić także drugą równoważność:

Nie jestem pewien co do wyniku - jeśli zrobiłem to dobrze, daj mi znać, czy coś jest nie tak.

Wyjaśnienie

Źródło

Jeśli ktoś chce źródła tex (potrzebuje 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}:

Wynik: 65

Prawa de Morgana to linia 30 i linia 65.

(Nie poczyniłem żadnego szczególnego wysiłku, aby to pograć w golfa, na przykład sprawdzić, czy istnieją powtarzające się dowody, które można by wyodrębnić na początku.)

 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