Freges Satzrechnung - Frege's propositional calculus
In der mathematischen Logik war Freges Satzrechnung die erste Axiomatisierung der Satzrechnung . Es wurde 1879 von Gottlob Frege erfunden , der auch die Prädikatenrechnung erfand , als Teil seiner Prädikatenrechnung zweiter Ordnung (obwohl Charles Peirce als erster den Begriff "zweite Ordnung" verwendete und unabhängig seine eigene Version der Prädikatenrechnung entwickelte von Frege).
Es werden nur zwei logische Operatoren verwendet: Implikation und Negation, und es besteht aus sechs Axiomen und einer Inferenzregel : modus ponens .
| Axiome | Inferenzregel |
|---|---|
|
|
Freges Satzrechnung entspricht jeder anderen klassischen Satzrechnung, wie dem "Standard-PC" mit 11 Axiomen. Freges PC und Standard-PC haben zwei gemeinsame Axiome: THEN-1 und THEN-2. Beachten Sie, dass die Axiome THEN-1 bis THEN-3 nur den Implikationsoperator verwenden (und definieren), während die Axiome FRG-1 bis FRG-3 den Negationsoperator definieren.
Die folgenden Theoreme zielen darauf ab, die verbleibenden neun Axiome des Standard-PC im "Theoremraum" von Freges PC zu finden, was zeigt, dass die Theorie des Standard-PC in der Theorie von Freges PC enthalten ist.
(Eine Theorie, die hier auch zu bildlichen Zwecken als "Theoremraum" bezeichnet wird, ist eine Menge von Theoremen, die eine Teilmenge einer universellen Menge wohlgeformter Formeln sind . Die Theoreme sind durch eine gerichtete Weise miteinander verbunden Inferenzregeln , die eine Art dendritisches Netzwerk bilden. An den Wurzeln des Theoremraums befinden sich die Axiome, die den Theoremraum "erzeugen", ähnlich wie eine Erzeugungsmenge eine Gruppe erzeugt.)
Regeln
Regel ( DANN-1 ) - A ⊢ B → A.
| # | wff | Grund |
|---|---|---|
| 1. | EIN | Prämisse |
| 2. | A → (B → A) | DANN-1 |
| 3. | B → A. | MP 1,2. |
Regel ( DANN-2 ) - A → (B → C) ⊢ (A → B) → (A → C)
| # | wff | Grund |
|---|---|---|
| 1. | A → (B → C) | Prämisse |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | DANN-2 |
| 3. | (A → B) → (A → C) | MP 1,2. |
Regel ( DANN-3 ) - A → (B → C) ⊢ B → (A → C)
| # | wff | Grund |
|---|---|---|
| 1. | A → (B → C) | Prämisse |
| 2. | (A → (B → C)) → (B → (A → C)) | DANN-3 |
| 3. | B → (A → C) | MP 1,2. |
Regel ( BRD-1 ) - A → B B B → ¬A
| # | wff | Grund |
|---|---|---|
| 1. | (A → B) → (¬B → ¬A) | BRD-1 |
| 2. | A → B. | Prämisse |
| 3. | ¬B → ¬A | MP 2,1. |
Regel ( TH1 ) - A → B, B → C ⊢ A → C.
| # | wff | Grund |
|---|---|---|
| 1. | B → C. | Prämisse |
| 2. | (B → C) → (A → (B → C)) | DANN-1 |
| 3. | A → (B → C) | MP 1,2 |
| 4. | (A → (B → C)) → ((A → B) → (A → C)) | DANN-2 |
| 5. | (A → B) → (A → C) | MP 3,4 |
| 6. | A → B. | Prämisse |
| 7. | A → C. | MP 6,5. |
Theoreme
Satz ( TH1 ) - (A → B) → ((B → C) → (A → C))
| # | wff | Grund |
|---|---|---|
| 1. | (B → C) → (A → (B → C)) | DANN-1 |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | DANN-2 |
| 3. | (B → C) → ((A → B) → (A → C)) | TH1 * 1,2 |
| 4. | ((B → C) → ((A → B) → (A → C))) → ((A → B) → ((B → C) → (A → C))) | DANN-3 |
| 5. | (A → B) → ((B → C) → (A → C)) | MP 3,4. |
Satz ( TH2 ) - A → (¬A → ¬B)
| # | wff | Grund |
|---|---|---|
| 1. | A → (B → A) | DANN-1 |
| 2. | (B → A) → (¬A → ¬B) | BRD-1 |
| 3. | A → (¬A → ¬B) | TH1 * 1,2. |
Satz ( TH3 ) - ¬A → (A → ¬B)
| # | wff | Grund |
|---|---|---|
| 1. | A → (¬A → ¬B) | TH 2 |
| 2. | (A → (¬A → ¬B)) → (¬A → (A → ¬B)) | DANN-3 |
| 3. | ¬A → (A → ¬B) | MP 1,2. |
Satz ( TH4 ) - ¬ (A → ¬B) → A.
| # | wff | Grund |
|---|---|---|
| 1. | ¬A → (A → ¬B) | TH3 |
| 2. | (¬A → (A → ¬B)) → (¬ (A → ¬B) → ¬¬A) | BRD-1 |
| 3. | ¬ (A → ¬B) → ¬¬A | MP 1,2 |
| 4. | A → A. | BRD-2 |
| 5. | ¬ (A → ¬B) → A. | TH1 * 3,4. |
Satz ( TH5 ) - (A → ¬B) → (B → ¬A)
| # | wff | Grund |
|---|---|---|
| 1. | (A → ¬B) → (¬B → ¬A) | BRD-1 |
| 2. | ((A → B) → (B → A)) → (B → ((A → B) → A)) | DANN-3 |
| 3. | ¬¬B → ((A → ¬B) → ¬A) | MP 1,2 |
| 4. | B → ¬¬B | BRD-3 mit A: = B. |
| 5. | B → ((A → ¬B) → ¬A) | TH1 * 4,3 |
| 6. | (B → ((A → B) → A)) → ((A → B) → (B → A)) | DANN-3 |
| 7. | (A → ¬B) → (B → ¬A) | MP 5,6. |
Satz ( TH6 ) - ¬ (A → ¬B) → B.
| # | wff | Grund |
|---|---|---|
| 1. | ¬ (B → ¬A) → B. | TH4 mit A: = B, B: = A. |
| 2. | (B → ¬A) → (A → ¬B) | TH5 mit A: = B, B: = A. |
| 3. | ((B → ¬A) → (A → ¬B)) → (¬ (A → ¬B) → ¬ (B → ¬A)) | BRD-1 |
| 4. | ¬ (A → ¬B) → ¬ (B → ¬A) | MP 2,3 |
| 5. | ¬ (A → ¬B) → B. | TH1 * 4,1. |
Satz ( TH7 ) - A → A.
| # | wff | Grund |
|---|---|---|
| 1. | A → ¬¬A | BRD-3 |
| 2. | A → A. | BRD-2 |
| 3. | A → A. | TH1 * 1,2. |
Satz ( TH8 ) - A → ((A → B) → B)
| # | wff | Grund |
|---|---|---|
| 1. | (A → B) → (A → B) | TH7 mit A: = A → B. |
| 2. | ((A → B) → (A → B)) → (A → ((A → B) → B)) | DANN-3 |
| 3. | A → ((A → B) → B) | MP 1,2. |
Satz ( TH9 ) - B → ((A → B) → B)
| # | wff | Grund |
|---|---|---|
| 1. | B → ((A → B) → B) | DANN-1 mit A: = B, B: = A → B. |
Satz ( TH10 ) - A → (B → ¬ (A → ¬B))
| # | wff | Grund |
|---|---|---|
| 1. | (A → ¬B) → (A → ¬B) | TH7 |
| 2. | ((A → ¬B) → (A → ¬B)) → (A → ((A → ¬B) → ¬B) | DANN-3 |
| 3. | A → ((A → ¬B) → ¬B) | MP 1,2 |
| 4. | ((A → ¬B) → ¬B) → (B → ¬ (A → ¬B)) | TH5 |
| 5. | A → (B → ¬ (A → ¬B)) | TH1 * 3,4. |
Anmerkung: ¬ (A → ¬B) → A (TH4), ¬ (A → ¬B) → B (TH6) und A → (B → ¬ (A → ¬B)) (TH10), also ¬ (A. → ¬B) verhält sich wie A∧B (vergleiche mit den Axiomen AND-1, AND-2 und AND-3).
Satz ( TH11 ) - (A → B) → ((A → ¬B) → ¬A)
| # | wff | Grund |
|---|---|---|
| 1. | A → (B → ¬ (A → ¬B)) | TH10 |
| 2. | (A → (B → ¬ (A → ¬B))) → ((A → B) → (A → ¬ (A → ¬B))) | DANN-2 |
| 3. | (A → B) → (A → ¬ (A → ¬B)) | MP 1,2 |
| 4. | (A → ¬ (A → ¬B)) → ((A → ¬B) → ¬A) | TH5 |
| 5. | (A → B) → ((A → ¬B) → ¬A) | TH1 * 3,4. |
TH11 ist das Axiom NOT-1 des Standard-PCs, das als " reductio ad absurdum " bezeichnet wird.
Satz ( TH12 ) - ((A → B) → C) → (A → (B → C))
| # | wff | Grund |
|---|---|---|
| 1. | B → (A → B) | DANN-1 |
| 2. | (B → (A → B)) → (((A → B) → C) → (B → C)) | TH1 |
| 3. | ((A → B) → C) → (B → C) | MP 1,2 |
| 4. | (B → C) → (A → (B → C)) | DANN-1 |
| 5. | ((A → B) → C) → (A → (B → C)) | TH1 * 3,4. |
Satz ( TH13 ) - (B → (B → C)) → (B → C)
| # | wff | Grund |
|---|---|---|
| 1. | (B → (B → C)) → ((B → B) → (B → C)) | DANN-2 |
| 2. | (B → B) → ((B → (B → C)) → (B → C)) | DANN-3 * 1 |
| 3. | B → B. | TH7 |
| 4. | (B → (B → C)) → (B → C) | MP 3,2. |
Regel ( TH14 ) - A → (B → P), P → Q ⊢ A → (B → Q)
| # | wff | Grund |
|---|---|---|
| 1. | P → Q. | Prämisse |
| 2. | (P → Q) → (B → (P → Q)) | DANN-1 |
| 3. | B → (P → Q) | MP 1,2 |
| 4. | (B → (P → Q)) → ((B → P) → (B → Q)) | DANN-2 |
| 5. | (B → P) → (B → Q) | MP 3,4 |
| 6. | ((B → P) → (B → Q)) → (A → ((B → P) → (B → Q))) | DANN-1 |
| 7. | A → ((B → P) → (B → Q)) | MP 5,6 |
| 8. | (A → (B → P)) → (A → (B → Q)) | DANN-2 * 7 |
| 9. | A → (B → P) | Prämisse |
| 10. | A → (B → Q) | MP 9,8. |
Satz ( TH15 ) - ((A → B) → (A → C)) → (A → (B → C))
| # | wff | Grund |
|---|---|---|
| 1. | ((A → B) → (A → C)) → (((A → B) → A) → ((A → B) → C)) | DANN-2 |
| 2. | ((A → B) → C) → (A → (B → C)) | TH12 |
| 3. | ((A → B) → (A → C)) → (((A → B) → A) → (A → (B → C))) | TH14 * 1,2 |
| 4. | ((A → B) → A) → (((A → B) → (A → C)) → (A → (B → C))) | DANN-3 * 3 |
| 5. | A → ((A → B) → A) | DANN-1 |
| 6. | A → (((A → B) → (A → C)) → (A → (B → C))) | TH1 * 5,4 |
| 7. | ((A → B) → (A → C)) → (A → (A → (B → C))) | DANN-3 * 6 |
| 8. | (A → (A → (B → C))) → (A → (B → C)) | TH13 |
| 9. | ((A → B) → (A → C)) → (A → (B → C)) | TH1 * 7,8. |
Satz TH15 ist die Umkehrung des Axioms THEN-2.
Satz ( TH16 ) - (¬A → ¬B) → (B → A)
| # | wff | Grund |
|---|---|---|
| 1. | (¬A → ¬B) → (¬¬B → ¬¬A) | BRD-1 |
| 2. | ¬¬B → ((¬A → ¬B) → ¬¬A) | DANN-3 * 1 |
| 3. | B → ¬¬B | BRD-3 |
| 4. | B → ((¬A → ¬B) → ¬¬A) | TH1 * 3,2 |
| 5. | (¬A → ¬B) → (B → ¬¬A) | DANN-3 * 4 |
| 6. | A → A. | BRD-2 |
| 7. | (¬ A → A) → (B → (¬ A → A)) | DANN-1 |
| 8. | B → (¬¬A → A) | MP 6,7 |
| 9. | (B → (A → A)) → ((B → A) → (B → A)) | DANN-2 |
| 10. | (B → ¬¬A) → (B → A) | MP 8,9 |
| 11. | (¬A → ¬B) → (B → A) | TH1 * 5,10. |
Satz ( TH17 ) - (¬A → B) → (¬B → A)
| # | wff | Grund |
|---|---|---|
| 1. | (¬A → ¬¬B) → (¬B → A) | TH16 mit B: = ¬B |
| 2. | B → ¬¬B | BRD-3 |
| 3. | (B → ¬¬B) → (¬A → (B → ¬¬B)) | DANN-1 |
| 4. | ¬A → (B → ¬¬B) | MP 2,3 |
| 5. | (¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B)) | DANN-2 |
| 6. | (¬A → B) → (¬A → ¬¬B) | MP 4,5 |
| 7. | (¬A → B) → (¬B → A) | TH1 * 6,1. |
Vergleiche TH17 mit Satz TH5.
Satz ( TH18 ) - ((A → B) → B) → (¬A → B)
| # | wff | Grund |
|---|---|---|
| 1. | (A → B) → (¬B → (A → B)) | DANN-1 |
| 2. | (¬B → ¬A) → (A → B) | TH16 |
| 3. | (¬B → ¬A) → (¬B → (A → B)) | TH1 * 2,1 |
| 4. | ((¬B → ¬A) → (¬B → (A → B))) → (¬B → (¬A → (A → B))) | TH15 |
| 5. | ¬B → (¬A → (A → B)) | MP 3,4 |
| 6. | (¬A → (A → B)) → (¬ (A → B) → A) | TH17 |
| 7. | ¬B → (¬ (A → B) → A) | TH1 * 5,6 |
| 8. | (¬B → (¬ (A → B) → A)) → ((¬B → ¬ (A → B)) → (¬B → A)) | DANN-2 |
| 9. | (¬B → ¬ (A → B)) → (¬B → A) | MP 7,8 |
| 10. | ((A → B) → B) → (¬B → ¬ (A → B)) | BRD-1 |
| 11. | ((A → B) → B) → (¬B → A) | TH1 * 10,9 |
| 12. | (¬B → A) → (¬A → B) | TH17 |
| 13. | ((A → B) → B) → (¬A → B) | TH1 * 11,12. |
Satz ( TH19 ) - (A → C) → ((B → C) → (((A → B) → B) → C))
| # | wff | Grund |
|---|---|---|
| 1. | ¬A → (¬B → ¬ (¬A → ¬¬B)) | TH10 |
| 2. | B → ¬¬B | BRD-3 |
| 3. | (B → ¬¬B) → (¬A → (B → ¬¬B)) | DANN-1 |
| 4. | ¬A → (B → ¬¬B) | MP 2,3 |
| 5. | (¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B)) | DANN-2 |
| 6. | (¬A → B) → (¬A → ¬¬B) | MP 4,5 |
| 7. | ¬ (¬A → ¬¬B) → ¬ (¬A → B) | BRD-1 * 6 |
| 8. | ¬A → (¬B → ¬ (¬A → B)) | TH14 * 1,7 |
| 9. | ((A → B) → B) → (¬A → B) | TH18 |
| 10. | ¬ (¬A → B) → ¬ ((A → B) → B) | BRD-1 * 9 |
| 11. | ¬A → (¬B → ¬ ((A → B) → B)) | TH14 * 8,10 |
| 12. | ¬C → (¬A → (¬B → ¬ ((A → B) → B))) | DANN-1 * 11 |
| 13. | (¬C → ¬A) → (¬C → (¬B → ¬ ((A → B) → B))) | DANN-2 * 12 |
| 14. | (¬C → (¬B → ¬ ((A → B) → B))) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B))) | DANN-2 |
| fünfzehn. | (¬C → ¬A) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B))) | TH1 * 13,14 |
| 16. | (A → C) → (¬C → ¬A) | BRD-1 |
| 17. | (A → C) → ((→ C → ¬B) → (¬C → ¬ ((A → B) → B))) | TH1 * 16,15 |
| 18. | (¬C → ¬ ((A → B) → B)) → (((A → B) → B) → C) | TH16 |
| 19. | (A → C) → ((¬C → ¬B) → (((A → B) → B) → C)) | TH14 * 17,18 |
| 20. | (B → C) → (¬C → ¬B) | BRD-1 |
| 21. | ((B → C) → (¬C → ¬B)) → (((¬C → ¬B) → (((A → B) → B) → C)) → ((B → C) → (((A → B) → B) → C))) |
TH1 |
| 22. | ((¬C → ¬B) → (((A → B) → B) → C)) → ((B → C) → (((A → B) → B) → C)) | MP 20,21 |
| 23. | (A → C) → ((B → C) → (((A → B) → B) → C)) | TH1 * 19,22. |
Hinweis: A → ((A → B) → B) (TH8), B → ((A → B) → B) (TH9) und (A → C) → ((B → C) → (((A. → B) → B) → C)) (TH19), also verhält sich ((A → B) → B) genau wie A∨B. (Vergleiche mit den Axiomen OR-1, OR-2 und OR-3.)
Satz ( TH20 ) - (A → ¬A) → ¬A
| # | wff | Grund |
|---|---|---|
| 1. | (A → A) → ((A → ¬A) → ¬A) | TH11 |
| 2. | A → A. | TH7 |
| 3. | (A → ¬A) → ¬A | MP 2,1. |
TH20 entspricht dem Axiom NOT-3 des Standard-PC, das als " tertium non datur " bezeichnet wird.
Satz ( TH21 ) - A → (¬A → B)
| # | wff | Grund |
|---|---|---|
| 1. | A → (¬A → ¬¬B) | TH2 mit B: = ~ B. |
| 2. | ¬¬B → B. | BRD-2 |
| 3. | A → (¬A → B) | TH14 * 1,2. |
TH21 entspricht dem Axiom NOT-2 des Standard-PCs, das als " ex contraictione quodlibet " bezeichnet wird.
Alle Axiome des Standard-PCs wurden nach der Vermietung von Freges PC abgeleitet
Regel ( $ 1 ) - $ 2
A∧B: = ¬ (A → ¬B) und A∨B: = (A → B) → B. Diese Ausdrücke sind nicht eindeutig, z. B. könnte A∨B auch als (B → A) → A, ¬A → B oder ¬B → A definiert worden sein. Beachten Sie jedoch, dass die Definition A∨B: = (A → B) → B keine Negationen enthält. Andererseits kann A∧B nicht allein als Implikation definiert werden, ohne Negation zu verwenden.
In gewissem Sinne können die Ausdrücke A∧B und A∨B als "Black Boxes" betrachtet werden. Im Inneren enthalten diese Blackboxen Formeln, die nur aus Implikation und Negation bestehen. Die Blackboxen können alles enthalten, solange sie in die Axiome AND-1 bis AND-3 und OR-1 bis OR-3 des Standard-PCs eingesteckt werden. Diese Axiome liefern vollständige syntaktische Definitionen der Konjunktions- und Disjunktionsoperatoren .
Der nächste Satz von Theoremen zielt darauf ab, die verbleibenden vier Axiome von Freges PC im "Theoremraum" von Standard-PC zu finden, was zeigt, dass die Theorie von Freges PC in der Theorie von Standard-PC enthalten ist.
Satz ( ST1 ) - A → A.
| # | wff | Grund |
|---|---|---|
| 1. | (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) | DANN-2 |
| 2. | A → ((A → A) → A) | DANN-1 |
| 3. | (A → (A → A)) → (A → A) | MP 2,1 |
| 4. | A → (A → A) | DANN-1 |
| 5. | A → A. | MP 4,3. |
Satz ( ST2 ) - A → ¬¬A
| # | wff | Grund |
|---|---|---|
| 1. | EIN | Hypothese |
| 2. | A → (¬A → A) | DANN-1 |
| 3. | ¬A → A. | MP 1,2 |
| 4. | ¬A → ¬A | ST1 |
| 5. | (¬A → A) → ((¬A → ¬A) → ¬¬A) | NICHT-1 |
| 6. | (¬A → ¬A) → ¬¬A | MP 3,5 |
| 7. | ¬¬A | MP 4,6 |
| 8. | A ⊢ ¬A | Zusammenfassung 1-7 |
| 9. | A → ¬¬A | DT 8. |
ST2 ist das Axiom FRG-3 von Freges PC.
Satz ( ST3 ) - B∨C → (¬C → B)
| # | wff | Grund |
|---|---|---|
| 1. | C → (¬C → B) | NICHT-2 |
| 2. | B → (¬C → B) | DANN-1 |
| 3. | (B → (¬C → B)) → ((C → (¬C → B)) → ((B ∨ C) → (¬C → B))) | OR-3 |
| 4. | (C → (¬C → B)) → ((B ∨ C) → (¬C → B)) | MP 2,3 |
| 5. | B∨C → (¬C → B) | MP 1,4. |
Satz ( ST4 ) - ¬¬A → A.
| # | wff | Grund |
|---|---|---|
| 1. | A∨¬A | NICHT-3 |
| 2. | (A∨¬A) → (¬¬A → A) | ST3 |
| 3. | A → A. | MP 1,2. |
ST4 ist das Axiom FRG-2 von Freges PC.
Beweisen Sie ST5: (A → (B → C)) → (B → (A → C))
| # | wff | Grund |
|---|---|---|
| 1. | A → (B → C) | Hypothese |
| 2. | B. | Hypothese |
| 3. | EIN | Hypothese |
| 4. | B → C. | MP 3,1 |
| 5. | C. | MP 2,4 |
| 6. | A → (B → C), B, A ⊢ C. | Zusammenfassung 1-5 |
| 7. | A → (B → C), B ⊢ A → C. | DT 6 |
| 8. | A → (B → C) ⊢ B → (A → C) | DT 7 |
| 9. | (A → (B → C)) → (B → (A → C)) | DT 8. |
ST5 ist Axiom THEN-3 von Freges PC.
Satz ( ST6 ) - (A → B) → (¬B → ¬A)
| # | wff | Grund |
|---|---|---|
| 1. | A → B. | Hypothese |
| 2. | ¬B | Hypothese |
| 3. | ¬B → (A → ¬B) | DANN-1 |
| 4. | A → ¬B | MP 2,3 |
| 5. | (A → B) → ((A → ¬B) → ¬A) | NICHT-1 |
| 6. | (A → ¬B) → ¬A | MP 1,5 |
| 7. | ¬A | MP 4,6 |
| 8. | A → B, ¬B ⊢ ¬A | Zusammenfassung 1-7 |
| 9. | A → B B ¬B → ¬A | DT 8 |
| 10. | (A → B) → (¬B → ¬A) | DT 9. |
ST6 ist das Axiom FRG-1 von Freges PC.
Jedes der Axiome von Frege kann von den Standardaxiomen abgeleitet werden, und jedes der Standardaxiome kann von den Axiomen von Frege abgeleitet werden. Dies bedeutet, dass die beiden Sätze von Axiomen voneinander abhängig sind und es in einem Satz kein Axiom gibt, das von dem anderen Satz unabhängig ist. Daher erzeugen die beiden Sätze von Axiomen dieselbe Theorie: Freges PC entspricht dem Standard-PC.
(Wenn die Theorien unterschiedlich sein sollten, sollte einer von ihnen Theoreme enthalten, die nicht in der anderen Theorie enthalten sind. Diese Theoreme können aus der Axiommenge ihrer eigenen Theorie abgeleitet werden. Wie jedoch gezeigt wurde, kann diese gesamte Axiommenge von der anderen abgeleitet werden Axiomensatz der Theorie, was bedeutet, dass die gegebenen Theoreme tatsächlich nur aus dem Axiomensatz der anderen Theorie abgeleitet werden können, so dass die gegebenen Theoreme auch zur anderen Theorie gehören. Widerspruch: Somit überspannen die beiden Axiomensätze denselben Theoremraum. Durch Konstruktion : Jeder Satz, der aus den Standardaxiomen abgeleitet ist, kann aus Freges Axiomen abgeleitet werden und umgekehrt, indem zuerst die Axiome der anderen Theorie wie oben gezeigt als Sätze bewiesen werden und diese Sätze dann als Deckspelzen verwendet werden, um den gewünschten Satz abzuleiten.)
Siehe auch
Verweise
- Buss, Samuel (1998). "Eine Einführung in die Beweistheorie" (PDF) . Handbuch der Beweistheorie . Elsevier. S. 1–78. ISBN 0-444-89840-9 . CS1-Wartung: entmutigter Parameter ( Link )
- Detlovs, Vilnis; Podnieks, Karlis (24. Mai 2017). "Axiome der Logik: Minimales System, Konstruktives System und Klassisches System". Einführung in die mathematische Logik (PDF) . Universität von Lettland . S. 29–30.