Beweisen Sie DeMorgans Gesetze

21

Die zehn Schlussfolgerungen des Natural Deduction Systems beweisen die Gesetze von DeMorgan .

Die Regeln des natürlichen Abzugs

  • Verneinung Einführung: {(P → Q), (P → ¬Q)} ⊢ ¬P

  • Verneinung-Beseitigung: {(¬P → Q), (¬P → ¬Q)} ⊢ P

  • Und Einführung: {P, Q} ⊢ P ʌ Q

  • Und Beseitigung: P ʌ Q ⊢ {P, Q}

  • Oder Einführung: P ⊢ {(P ∨ Q),(Q ∨ P)}

  • Oder Beseitigung: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

  • Iff Einführung: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

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

  • Wenn Einführung: (P ⊢ Q) ⊢ (P → Q)

  • Wenn Beseitigung: {(P → Q), P} ⊢ Q

Beweisstruktur

Jede Aussage in Ihrem Beweis muss das Ergebnis einer der zehn Regeln sein, die auf einige zuvor abgeleitete Sätze (keine zirkuläre Logik) oder eine Annahme (nachfolgend beschrieben) angewendet wurden. Jede Regel wirkt auf einige Sätze auf der linken Seite des Operators (logische Konsequenz) und erzeugt eine beliebige Anzahl von Sätzen auf der rechten Seite. Die If-Einführung unterscheidet sich geringfügig von den übrigen Operatoren (im Folgenden ausführlich beschrieben). Es wirkt sich auf eine Anweisung aus, die die logische Konsequenz einer anderen ist.

Beispiel 1

Sie haben folgende Aussagen:

{(P → R), Q}

Sie können And Introduction verwenden, um Folgendes zu erstellen:

(P → R) ʌ Q

Beispiel 2

Sie haben folgende Aussagen:

{(P → R), P}

Sie können If Elimination verwenden, um Folgendes zu machen:

R

Beispiel 3

Sie haben folgende Aussagen:

(P ʌ Q)

Sie können And Elimination verwenden, um Folgendes zu machen:

P

oder machen:

Q

Mariä Himmelfahrt

Sie können jederzeit eine von Ihnen gewünschte Aussage treffen. Jede Aussage, die aus diesen Annahmen abgeleitet wird, ist "abhängig" von ihnen. Aussagen werden auch von den Annahmen abhängen, auf die sich ihre übergeordneten Aussagen stützen. Die einzige Möglichkeit, Annahmen zu beseitigen, ist die If-Einführung. Bei If-Einführung beginnen Sie mit einer Aussage Q, die auf einer Aussage beruht, Pund enden mit (P → Q). Die neue Anweisung ist darauf angewiesen , jede Annahme Qauf verlässt sich außer für Annahme P. Ihre endgültige Aussage sollte sich auf keine Annahmen stützen.

Besonderheiten und Wertung

Sie konstruieren einen Beweis für jedes der beiden Gesetze von DeMorgan, indem Sie nur die 10 Folgerungen des Natural Deduction Calculus verwenden.

Die zwei Regeln sind:

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

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

Ihre Punktzahl ergibt sich aus der Anzahl der verwendeten Schlussfolgerungen und der Anzahl der getroffenen Annahmen. Ihre endgültige Aussage sollte sich nicht auf irgendwelche Annahmen stützen (dh sollte ein Theorem sein).

Sie können Ihren Proof nach Belieben formatieren.

Sie können jedes Lemma kostenlos von einem Proof auf einen anderen übertragen.

Beispiel Beweis

Ich werde das beweisen (P and not(P)) implies Q

(Jeder Aufzählungspunkt ist +1 Punkt)

  • Annehmen not (Q)

  • Annehmen (P and not(P))

  • Verwenden und Elim (P and not(P))ableiten{P, not(P)}

  • Verwenden Sie und Einführung auf Pund not(Q)abzuleiten(P and not(Q))

  • Verwenden Sie And Elim für die gerade abgeleitete Aussage P

Der neue PSatz unterscheidet sich von dem anderen, den wir früher herleiten. Es ist nämlich auf die Annahmen angewiesen not(Q)und (P and not(P)). Während die ursprüngliche Aussage war nur auf (P and not(P)). Dies ermöglicht uns Folgendes:

  • Wenn Einführung auf PEinführung not(Q) implies P(immer noch abhängig von der (P and not(P))Annahme)

  • Verwenden Sie und Einführung auf not(P)und not(Q)(ab Schritt 3), um abzuleiten(not(P) and not(Q))

  • Verwenden Sie und Elim auf die soeben abgeleitete Aussage zu machen not(P) (jetzt abhängig von not(Q))

  • Wenn Einführung auf die neue not(P)Einführungnot(Q) implies not(P)

  • Wir werden nun die Negation Beseitigung auf verwenden not(Q) implies not(P)und not(Q) implies PherzuleitenQ

Dies Qhängt nur von der Annahme ab (P and not(P)), mit der wir den Beweis beenden können

  • Wenn Einführung auf Qabzuleiten(P and not(P)) implies Q

Dieser Beweis ergibt insgesamt 11 Punkte.

Weizen-Assistent
quelle
7
Obwohl der Konsens über Meta klar ist, wird ihn noch nicht jeder gesehen haben, um nur hervorzuheben, dass Beweise für das Golfen ein Thema sind .
Trichoplax
2
Ich denke, Sie sollten die Struktur der Beweise erklären und (das Symbol wird für mich auch nicht auf Mobilgeräten gerendert).
16.
3
Ich denke die Erklärungen helfen definitiv. Was ich am nützlichsten finden würde, wäre ein ausgearbeitetes und bewertetes Beispiel für einen einfachen Beweis, der If-Introduction und Annahmen enthält, vorzugsweise verschachtelt. Vielleicht kontrapositiv?
16.
1
In Ihrem Beispiel glaube ich, dass die ersten beiden Annahmen umgedreht werden müssten; Nichts macht es diesen Staat (P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))(in diesem Fall ¬Q ⊢ ((P ʌ ¬P) ⊢ P)zu (P ʌ ¬P) ⊢ (¬Q ⊢ P)verwendet wurde).
LegionMammal978
1
Dürfen Sie mehrere Dinge in einem einzigen "Annahmekontext" beweisen und dann mehrere Implikationsanweisungen extrahieren, um zu sparen, wie viele "Annahmelinien" benötigt werden? zB (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-introum eine Punktzahl von 9 zu bekommen?
Daniel Schepler

Antworten:

6

Prüfungsergebnis: 81

Jede Linie sollte 1 Punkt wert sein. Die Gesetze von De Morgan finden sich in den Aussagen (3) und (6). Beschriftungen in Klammern kennzeichnen die vorherigen Aussagen, von denen eine Zeile abhängt, wenn sie nicht unmittelbar vorangehen.

(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
quelle
4

Prüfungsergebnis: 59

Erläuterung

Ich werde eine baumähnliche Struktur für den Beweis verwenden, da ich diesen Stil gut lesbar finde. Jede Zeile wird mit der Anzahl der verwendeten Regeln beschriftet. Beispiel: Das "Beispiel 1" in der Challenge würde als dieser Baum dargestellt (von unten nach oben):

AIntro

Man beachte die unbekannten Zählungen A, B und auch die Annahme Γ - das ist also kein Theorem. Um zu demonstrieren, wie ein Theorem zu beweisen ist, nehmen wir A an und verwenden eine Or-Einführung wie folgt:

OIntro

Dies hängt immer noch von der Annahme A ab, aber wir können einen Satz ableiten, indem wir eine If-Einführung anwenden:

IIntro

So konnten wir den Satz ⊢ A → ( AB ) in insgesamt 3 Schritten ableiten (1 Annahme & 2 angewandte Regeln).

Damit können wir ein paar neue Regeln beweisen, die uns helfen, DeMorgans Gesetze zu beweisen.

Zusätzliche Regeln

Leiten wir zunächst das Explosionsprinzip ab und bezeichnen es in weiteren Beweisen mit PE :

PE

Daraus leiten wir eine andere Form ab: A ⊢ ¬ AX - wir nennen es CPE :

PE

Wir werden einen weiteren benötigen, bei dem der negierte Term (¬) eine Annahme ist, und ihn als CPE bezeichnen - :

NCPE

Aus den beiden soeben abgeleiteten Regeln ( CPE und CPE - ) können wir eine wichtige Regel Double Negation ableiten :

DN

Das nächste was zu tun ist, ist etwas wie Modus Tollens zu beweisen - daher MT :

MT

Lemmas

Lemma A

Lemma A1

Wir brauchen zwei Mal die folgende Regel:

LA1

Lemma A

Indem wir das gerade bewiesene Lemma zweimal instanziieren, können wir eine Richtung einer Äquivalenz zeigen, die wir für den endgültigen Beweis benötigen:

LA

Lemma B

Um eine andere Richtung aufzuzeigen, müssen wir zwei Mal ziemlich repetitive Sachen machen (für beide Argumente A und B in ( AB )) - das bedeutet, dass ich hier möglicherweise den Beweis weiter spielen könnte.

Lemma B1 '

LB1_

Lemma B1

LB1

Lemma B2 '

LB2_

Lemma B2

LB2

Lemma B

Schließlich die Schlussfolgerung von B1 und B2 :

PFUND

Tatsächlicher Beweis

Sobald wir diese beiden Aussagen bewiesen haben:

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

Wir können die erste Äquivalenz (¬ ( AB ) ≡ ¬ A ʌ ¬ B ) wie folgt beweisen :

P1

Und mit der gerade bewiesenen Regel zusammen mit Iff-Elimination können wir auch die zweite Äquivalenz beweisen:

P2

Ich bin mir nicht sicher, ob das stimmt. Wenn ich es richtig gemacht habe, lass es mich wissen, wenn etwas nicht stimmt.

Erläuterung

Quelle

Wenn jemand die Tex-Quelle haben möchte (braucht 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}:
ბიმო
quelle
1
Soweit ich das beurteilen kann, erlaubt das natürliche Deduktionsbeweissystem hier nicht, eine Aussage einmal mit generischen Satzvariablen zu beweisen und sie dann zu instanziieren. Also, jedes Mal haben Sie eine andere Instanziierung eines Ihrer Lemmata in Bezug auf die Variablen Pund Qwürden Sie seine Schritte separat in der Endsumme zählen müssen. (Mit anderen Worten, das Beweissystem erlaubt es nicht direkt, "Lemmata zweiter Ordnung" wie "für alle Sätze A und B A/\B -> B/\A" zu beweisen und dann beide P/\(Q/\R) -> (Q/\R)/\Pund zu beweisen (P/\Q)/\R -> R/\(P/\Q).)
Daniel Schepler
@DanielSchepler: Ja, aber es gibt keine zirkulären Abhängigkeiten und in der Regel heißt es, dass Sie jedes Lemma von einem Beweis zum anderen übertragen können, ohne dafür Punkte zu verlangen. Das wird schon gut. Bearbeiten : In der Tat, wenn das nicht erlaubt wäre, bin ich sicher, dass diese Frage nur eine berechtigte Antwort haben würde.
3.
Ich habe das so interpretiert, dass es einfach bedeutet, dass man einige gemeinsame Beweise für eine Reihe konkreter Formeln haben kann, die zwischen den Beweisen der beiden endgültigen Aussagen geteilt werden.
Daniel Schepler
1

Prüfungsergebnis: 65

Die Gesetze von de Morgan lauten Linie 30 und Linie 65.

(Ich habe keine besonderen Anstrengungen unternommen, um Golf zu spielen, zum Beispiel um zu sehen, ob es einige wiederholte Beweise gibt, die zu Beginn abstrahiert werden könnten.)

 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
quelle