WEITERE SCHLUSSREGELN IM AXIOMENSYSTEM SHOENFIELDS

 

Das Axiomensystem Shoenfields umfasst ein Axiom, vier Schlussregeln und zwei Definitionen.

 

Axiom:

  1. \( \neg a\vee a \) Satz vom ausgeschlossenen Dritten

Schlussregeln:

  1. \( \displaystyle\genfrac{}{}{1pt}{}{a\vee(b\vee c)}{(a\vee b)\vee c} \) Assoziativregel (ASS)
  2. \( \displaystyle\genfrac{}{}{1pt}{}{a\vee a}{a} \) Kompressionsregel (KOM)
  3. \( \displaystyle\genfrac{}{}{1pt}{}{a}{b\vee a} \) Expansionsregel (EXP)
  4. \( \displaystyle\genfrac{}{}{1pt}{}{a\vee b,\ \neg a\vee c}{b\vee c} \) Schnittregel (CUT)

Definitionen:

  1. \( a\to b \) bedeutet\( \quad\neg a\vee b \)
  2. \( a\wedge b \) bedeutet \( \quad\neg(\neg a\vee\neg b) \)

 

Wir leiten hieraus weitere Schlussregeln ab, die wir zum Teil R.E. Hodels Lehrbuch entnehmen oder selbst hinzufügen. Im ersteren Fall benutzen wir verschiedene Beweise aus diesem Lehrbuch, entwickeln neue Beweisvarianten oder geben eigene Beweise der von R.E. Hodel nicht bewiesenen Schlussregeln.

Erste abgeleitete Schlussregeln

Kommutativität bez. \( \vee \) (KMO)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee b}{b\vee a} \)
Beweis (siehe R.E. Hodel, S. 81)
1. \( \vdash\ a\vee b \) (VOR)
2. \( \vdash\ \neg a\vee a \) (AX)
3. \( \vdash\ b\vee a \) (CUT, 1, 2)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Kommutativität in Expansionsregel (KME)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a}{a\vee b} \)
Beweis (siehe R.E. Hodel, S. 81)
1. \( \vdash\ a \) (VOR)
2. \( \vdash\ b\vee a \) (EXP, 1)
3. \( \vdash\ a\vee b \) (KMO, 2)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Umkehrung der Assoziativregel (UASS)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{(a\vee b)\vee c}{a\vee(b\vee c)} \)
Beweis (siehe R.E. Hodel, S. 81)
1. \( \vdash\ (a\vee b)\vee c \) (VOR)
2. \( \vdash\ c\vee(a\vee b) \) (KMO, 1)
3. \( \vdash\ (c\vee a)\vee b \) (ASS, 2)
4. \( \vdash\ b\vee(c\vee a) \) (KMO, 3)
5. \( \vdash\ (b\vee c)\vee a \) (ASS, 4)
6. \( \vdash\ a\vee(b\vee c) \) (KMO, 5)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

Erste Erweiterungen der Schlussregeln

Erste Erweiterung der Expansionsregel (EEXP1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee b}{a\vee(c\vee b)} \)
Beweis (siehe R.E. Hodel, S. 91)
1. \( \vdash\ a\vee b \) (VOR)
2. \( \vdash\ b\vee a \) (KMO, 1)
3. \( \vdash\ c\vee(b\vee a) \) (EXP, 2)
4. \( \vdash\ (c\vee b)\vee a \) (ASS, 3)
5. \( \vdash\ a\vee(c\vee b) \) (KMO, 4)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erste Erweiterung der Kompressionsregel (EKOM1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee(b\vee b)}{a\vee b} \)
Beweis
1. \( \vdash\ a\vee(b\vee b) \) (VOR)
2. \( \vdash\ (a\vee b)\vee b \) (ASS, 1)
3. \( \vdash\ b\vee(a\vee b) \) (KMO, 2)
4. \( \vdash\ \neg b\vee b \) (AX)
5. \( \vdash\ \neg b\vee(a\vee b) \) (EEXP1, 4)
6. \( \vdash\ (a\vee b)\vee(a\vee b) \) (CUT, 3, 5)
7. \( \vdash\ a\vee b \) (KOM, 6)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erste Erweiterung der Schnittregel (ECUT1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee(b\vee c),a\vee(\neg b\vee d)}{a\vee(c\vee d)} \)
Beweis (siehe R.E. Hodel, S. 92)
1. \( \vdash\ a\vee(b\vee c) \) (VOR)
2. \( \vdash\ (a\vee b)\vee c \) (ASS, 1)
3. \( \vdash\ [(a\vee b)\vee c]\vee d \) (KME, 2)
4. \( \vdash\ (a\vee b)\vee(c\vee d) \) (UASS, 3)
5. \( \vdash\ (c\vee d)\vee(a\vee b) \) (KMO, 4)
6. \( \vdash\ [(c\vee d)\vee a]\vee b \) (ASS, 5)
7. \( \vdash\ b\vee[(c\vee d)\vee a] \) (KMO, 6)
8. \( \vdash\ a\vee(\neg b\vee d) \) (Vor)
9. \( \vdash\ (a\vee\neg b)\vee d \) (ASS, 8)
10. \( \vdash\ d\vee(a\vee\neg b) \) (KMO, 9)
11. \( \vdash\ c\vee[d\vee(a\vee\neg b)] \) (EXP, 10)
12. \( \vdash\ (c\vee d)\vee(a\vee\neg b) \) (ASS, 11)
13. \( \vdash\ [(c\vee d)\vee a]\vee\neg b \) (ASS, 12)
14. \( \vdash\ \neg b\vee[(c\vee d)\vee a] \) (KMO, 13)
15. \( \vdash\ [(c\vee d)\vee a]\vee[(c\vee d)\vee a] \) (CUT, 7, 14)
16. \( \vdash\ (c\vee d)\vee a \) (KOM, 15)
17. \( \vdash\ a\vee(c\vee d) \) (KMO, 16)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erste Erweiterung der Assoziativregel (EASS1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee[b\vee(c\vee d)]}{a\vee[(b\vee c)\vee d]} \)
Beweis (siehe R.E. Hodel, S. 92)
1. \( a\vee[b\vee(c\vee d)] \) (VOR)
2. \( \vdash\ (a\vee b)\vee(c\vee d) \) (ASS, 1)
3. \( \vdash\ (c\vee d)\vee(a\vee b) \) (KMO, 2)
4. \( \vdash\ c\vee[d\vee(a\vee b)] \) (UASS, 3)
5. \( \vdash\ b\vee\{c\vee[d\vee(a\vee b)]\} \) (EXP, 4)
6. \( \vdash\ (b\vee c)\vee[d\vee(a\vee b)] \) (ASS, 5)
7. \( \vdash\ [(b\vee c)\vee d]\vee(a\vee b) \) (ASS, 6)
8. \( \vdash\ a\vee\{[(b\vee c)\vee d]\vee(a\vee b)\} \) (EXP, 7)
9. \( \vdash\ \{a\vee[(b\vee c)\vee d]\}\vee(a\vee b) \) (ASS, 8)
10. \( \vdash\ \{\{a\vee[(b\vee c)\vee d]\}\vee a\}\vee b \) (ASS, 9)
11. \( \vdash\ \{\{\{a\vee[(b\vee c)\vee d]\}\vee a\}\vee b\}\vee c \) (KME, 10)
12. \( \vdash\ \{\{a\vee[(b\vee c)\vee d]\}\vee a\}\vee(b\vee c) \) (UASS, 11)
13. \( \vdash\ \{\{\{a\vee[(b\vee c)\vee d]\}\vee a\}\vee(b\vee c)\}\vee d \) (KME, 12)
14. \( \vdash\ \{\{a\vee[(b\vee c)\vee d]\}\vee a\}\vee[(b\vee c)\vee d] \) (UASS, 13)
15. \( \vdash\ \{a\vee[(b\vee c)\vee d]\}\vee\{a\vee[(b\vee c)\vee d]\} \) (UASS, 14)
16. \( \vdash\ a\vee[(b\vee c)\vee d] \) (KOM, 15)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

Zentrale Beweismittel

Deduktionstheorem der Aussagenlogik (DT)

  1. Falls \( \Gamma\cup\{a\}\vdash b, \) so gilt \( \Gamma\vdash(a\to b). \)

 

Beweis (siehe R.E. Hodel, S. 89)

Unter Verwendung von KMO, EEXP1, EKOM1, ECUT1 und EASS1. \( \quad\Box \)

 

 

Erste Fallunterscheidung (FU1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\to c,\ b\to d,\ a\vee b}{c\vee d} \)
Beweis
1. \( \vdash\ a\to c \) (VOR)
2. \( \vdash\ b\to d \) (VOR)
3. \( \vdash\ a\vee b \) (VOR)
4. \( \vdash\ \neg a\vee c \) (DEF \(\to\), 1)
5. \( \vdash\ \neg b\vee d \) (DEF \(\to\), 2)
6. \( \vdash\ b\vee a \) (KMO, 3)
7. \( \vdash\ a\vee d\) (CUT, 5, 6)
8. \( \vdash\ c\vee d \) (CUT, 4, 8)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweite Fallunterscheidung (FU2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee b,\ a\vdash b,\ b\vdash c}{c} \)

Weiter ...

Beweis (siehe R.E. Hodel, S. 81)
1. \( \vdash\ a \) (VOR)
2. \( \vdash\ b\vee a \) (EXP, 1)
3. \( \vdash\ a\vee b \) (KMO, 2)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweite Erweiterung der Kompressionsregel (EKOM2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee[b\vee(c\vee c)]}{a\vee(b\vee c)} \)
Beweis
1. \( \vdash\ a\vee[b\vee(c\vee c)] \) (VOR)
2. \( \vdash\ (a\vee b)\vee(c\vee c) \) (ASS, 1)
3. \( \vdash\ (a\vee b)\vee c \) (EKOM1, 2)
4. \(\vdash\ a\vee(b\vee c) \) (ASS, 3)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweite Erweiterung der Assoziativregel (EASS2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee[(b\vee c)\vee d]}{a\vee[b\vee(c\vee d)]} \)

 

 

Erweiterung der Kommutativregel (EKMO)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee(b\vee c)}{a\vee(c\vee b)} \)

 

 

Erstes Gesetz der doppelten Negation (DN1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a}{\neg\neg a} \)
Beweis (siehe R.E. Hodel, S. 81)
1. \( \vdash\ a \) (VOR)
2. \( \vdash\ \neg\neg a\vee\neg a \) (AX)
3. \( \vdash \neg a\vee\neg\neg a\) (KMO, 2)
4. \( \vdash\ \neg\neg a\vee a \) (EXP, 1)
5. \( \vdash\ a\vee\neg\neg a \) (KMO, 4)
6. \( \vdash\ \neg\neg a\vee\neg\neg a \) (CUT, 3, 5)
7. \( \vdash\ \neg\neg a \) (KOM, 6)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erweiterung des ersten Gesetzes der doppelten Negation (EDN1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee b}{\neg\neg a\vee b} \)
Beweis
1. \( \vdash\ a\vee b \) (VOR)
2. \( \vdash\ a\vee(\neg\neg a\vee b) \) (EEXP 8, 1)
3. \( \vdash\ \neg\neg a\vee\neg a \) (AX)
4. \( \vdash\ \neg\neg a\vee(b\vee\neg a) \) (EEXP, 3)
5. \( \vdash\ (\neg\neg a\vee b)\vee\neg a \) (ASS, 4)
6. \( \vdash\ \neg a\vee(\neg\neg a\vee b) \) (KMO, 5)
7. \( \vdash\ (\neg\neg a\vee b)\vee(\neg\neg a\vee b) \) (CUT, 2, 6)
8. \( \neg\neg a\vee b \) (KOM, 7)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweites Gesetz der doppelten Negation (DN2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg\neg a}{a} \)
Beweis
1. \( \vdash\ \neg\neg a \) (VOR)
2. \( \vdash\ a\vee\neg\neg a \) (EXP, 1)
3. \( \vdash \neg\neg a\vee a \) (KMO, 2)
4. \( \vdash\ \neg a\vee a \) (AX)
5. \( \vdash\ a\vee a \) (CUT, 3, 4)
6. \( \vdash\ a \) (KOM, 5)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erweiterung des zweiten Gesetzes der doppelten Negation (EDN2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg\neg a\vee b}{a\vee b} \)
Beweis
1. \( \vdash\ \neg\neg a\vee b \) (VOR)
2. \( \vdash\ a\vee(\neg\neg a\vee b) \) (EXP, 1)
3. \( \vdash\ (\neg\neg a\vee b)\vee a \) (KMO, 2)
4. \(\vdash\ \neg\neg a\vee(b\vee a) \) (UASS, 3)
5. \(\vdash\ \neg a\vee a \) (AX)
6. \(\vdash\ a\vee(b\vee a) \) (CUT, 4, 5)
7. \(\vdash\ (b\vee a)\vee a \) (KMO, 6)
8. \(\vdash\ b\vee(a\vee a) \) (UASS, 7)
9. \(\vdash\ b\vee a \) (EKOM1, 8)
10. \(\vdash\ a\vee b \) (KMO, 9)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Vereinigungsregel (VR)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a,\ b}{a\vee b} \)
Beweis
1. \( \vdash\ b \) (VOR)
2. \( \vdash\ a\vee b \) (EXP, 1)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erste Abtrennungsregel (AR1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\wedge b}{a} \)
Beweis
1. \( \vdash\ a\wedge b \) (VOR)
2. \( \vdash\ \neg(\neg a\vee\neg b) \) (DEF \(\wedge, 1\))
3. \( \vdash\ a\vee\neg(\neg a\vee\neg b) \) (EXP, 2)
4. \( \vdash\ \neg(\neg a\vee\neg b)\vee a \) (KMO, 3)
5. \( \vdash\ \neg a\vee a \) (AX)
6. \( \vdash\ a\vee\neg a \) (KMO, 5)
7. \( \vdash\ b\vee(a\vee\neg a) \) (EXP, 6)
8. \( \vdash\ (a\vee\neg a)\vee b \) (KMO, 7)
9. \( \vdash\ a\vee(\neg a\vee b) \) (UASS, 8)
10. \( \vdash\ (\neg a\vee b)\vee a \) (KMO, 9)
11. \( \vdash\ a\vee a \) (CUT, 4, 10)
10. \( \vdash\ a \) (KOM, 11)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweite Abtrennungsregel (AR2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\wedge b}{b} \)
Beweis
1. \( \vdash\ a\wedge b \) (VOR)
2. \( \vdash\ \neg(\neg a\vee\neg b) \) (DEF \(\wedge, 1\))
3. \( \vdash\ b\vee\neg(\neg a\vee\neg b) \) (EXP, 2)
4. \( \vdash\ \neg(\neg a\vee\neg b)\vee b \) (KMO, 3)
5. \( \vdash\ \neg b\vee b \) (AX)
6. \( \vdash\ \neg a\vee(\neg b\vee b) \) (EXP, 5)
7. \( \vdash\ (\neg a\vee\neg b)\vee b \) (ASS, 6)
8. \( \vdash\ b\vee b \) (CUT, 4, 7)
9. \( \vdash\ b \) (KOM, 8)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Konjunktionseinführung (KE)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a,\ b}{a\wedge b} \)
Beweis (siehe R.E. Hodel, S. 82)
Der Beweis benutzt den Modus Tollendo Ponens MTP (disjunktiver Syllogismus).
1. \( \vdash\ a \) (VOR)
2. \( \vdash\ b \) (VOR)
3. \( \vdash\ \neg(\neg a\vee\neg b)\vee(\neg a\vee\neg b) \) (AX)
4. \( \vdash\ [\neg(\neg a\vee\neg b)\vee\neg a]\vee\neg b \) (ASS, 3)
5. \( \vdash\ \neg b\vee[\neg(\neg a\vee\neg b)\vee\neg a] \) (KMO, 4)
6. \( \vdash\ \neg\neg b \) (DN1, 2)
7. \(\vdash\ \neg(\neg a\vee\neg b)\vee\neg a \) (MTP, 5, 6)
8. \(\vdash\ \neg a\vee[\neg(\neg a\vee\neg b)] \) (KMO, 7)
9. \(\vdash\ \neg\neg a \) (DN1, 1)
10. \(\vdash\ \neg(\neg a\vee\neg b) \) (MTP, 8, 9)
11. \(\vdash\ a\wedge b \) (DEF \(\wedge\))
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Kommutativität bez. \( \wedge \) (KMU)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\wedge b}{b\wedge a} \)

 

 

Kontraposition (KP)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\to b}{\neg b\to\neg a} \)
Beweis
1. \( \vdash\ a\to b \) (VOR)
2. \( \vdash\ \neg a\vee b \) (DEF \(\to\), 1)
3. \( \vdash\ b\vee\neg a \) (KMO, 2)
4. \( \vdash\ \neg\neg b\vee\neg a \) (EDN1, 3)
5. \( \vdash\ \neg b\to\neg a \) (DEF \(\to\), 4)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Erste de Morgansche Regel (MR1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg(a\wedge b)}{\neg a\vee\neg b} \)
Beweis
1. \( \vdash\ \neg(a\wedge b) \) (VOR)
2. \( \vdash\ \neg\neg(\neg a\vee\neg b) \) (DEF \(\wedge\), 1)
3. \( \vdash\ \neg a\vee\neg b \) (DN2, 2)
Damit ist die Behauptung bewiesen. \( \quad\Box \)

 

 

Zweite de Morgansche Regel (MR2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg(a\vee b)}{\neg a\wedge\neg b} \)

 

 

Umkehrung der ersten de Morganschen Regel (UMR1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg a\vee\neg b}{\neg(a\wedge b)} \)

 

 

Umkehrung der zweiten de Morganschen Regel (UMR2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{\neg a\wedge\neg b}{\neg(a\vee b)} \)

 

 

Reductio ad absurdum, Negationseinführung (NE)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{b,\ a\wedge b\to\neg a}{\neg a} \)

 

 

Erstes Distributivgesetz (DG1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\wedge(b\vee c)}{(a\wedge b)\vee(a\wedge c)} \)

 

 

Zweites Distributivgesetz (DG2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{a\vee(b\wedge c)}{(a\vee b)\wedge(a\vee c)} \)

 

 

Umkehrung des ersten Distributivgesetzes (UDG1)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{(a\wedge b)\vee(a\wedge c)}{a\wedge(b\vee c)} \)

 

 

Umkehrung des zweiten Distributivgesetzes (UDG2)

  1. \( \displaystyle\vdash\ \genfrac{}{}{1pt}{}{(a\vee b)\wedge(a\vee c)}{a\vee(b\wedge c)} \)