Frege's propositional calculus
Encyclopedia
In mathematical logic
Frege's propositional calculus was the first axiomatization of propositional calculus
. It was invented by Gottlob Frege
, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus (although Charles Peirce was the first to use the term "second-order" and developed his own version of the predicate calculus independently of Frege).
It makes use of just two logical operators: implication and negation, and it is constituted by six axiom
s and one inference rule: modus ponens
.
Axioms
THEN-1: A → (B → A)
THEN-2: (A → (B → C)) → ((A → B) → (A → C))
THEN-3: (A → (B → C)) → (B → (A → C))
FRG-1: (A → B) → (¬B → ¬A)
FRG-2: ¬¬A → A
FRG-3: A → ¬¬A
Inference Rule
MP: P, P→Q ⊢ Q
Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN-1 and THEN-2. Notice that axioms THEN-1 through THEN-3 only make use of (and define) the implication operator, whereas axioms FRG-1 through FRG-3 define the negation operator.
The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem-space" of Frege's PC, showing that the theory of standard PC is contained within the theory of Frege's PC.
(A theory, also called here, for figurative purposes, a "theorem-space", is a set of theorems which are a subset of a universal set of well-formed formula
s. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem-space are found the axioms, which "generate" the theorem-space much like a generating set
generates a group.)
Rule THEN-1*: A ⊢ B→A
Rule THEN-2*: A→(B→C) ⊢ (A→B)→(A→C)
Rule THEN-3*: A→(B→C) ⊢ B→(A→C)
Rule FRG-1*: A→B ⊢ ¬B→¬A
Rule TH1*: A→B, B→C ⊢ A→C
Theorem TH1: (A→B)→((B→C)→(A→C))
Theorem TH2: A→(¬A→¬B)
Theorem TH3: ¬A→(A→¬B)
Theorem TH4: ¬(A→¬B)→A
Theorem TH5: (A→¬B)→(B→¬A)
Theorem TH6: ¬(A→¬B)→B
Theorem TH7: A→A
Theorem TH8: A→((A→B)→B)
Theorem TH9: B→((A→B)→B)
Theorem TH10: A→(B→¬(A→¬B))
Note: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), and A→(B→¬(A→¬B)) (TH10), so ¬(A→¬B) behaves just like A∧B (compare with axioms AND-1, AND-2, and AND-3).
Theorem TH11: (A→B)→((A→¬B)→¬A)
TH11 is axiom NOT-1 of standard PC, called "reductio ad absurdum
".
Theorem TH12: ((A→B)→C)→(A→(B→C))
Theorem TH13: (B→(B→C))→(B→C)
Rule TH14*: A→(B→P), P→Q ⊢ A→(B→Q)
Theorem TH15: ((A→B)→(A→C))→(A→(B→C))
Theorem TH15 is the converse
of axiom THEN-2.
Theorem TH16: (¬A→¬B)→(B→A)
Theorem TH17: (¬A→B)→(¬B→A)
Compare TH17 with theorem TH5.
Theorem TH18: ((A→B)→B)→(¬A→B)
Theorem TH19: (A→C)→ ((B→C)→(((A→B)→B)→C))
Note: A→((A→B)→B) (TH8), B→((A→B)→B) (TH9), and
(A→C)→((B→C)→(((A→B)→B)→C)) (TH19), so ((A→B)→B) behaves just like A∨B. (Compare with axioms OR-1, OR-2, and OR-3.)
Theorem TH20: (A→¬A)→¬A
TH20 corresponds to axiom NOT-3 of standard PC, called "tertium non datur".
Theorem TH21: A→(¬A→B)
TH21 corresponds to axiom NOT-2 of standard PC, called "ex contradictione quodlibet".
All the axioms of standard PC have be derived from Frege's PC, after having let
A∧B := ¬(A→¬B) and A∨B := (A→B)→B. These expressions are not unique, e.g. A∨B could also have been defined as (B→A)→A, ¬A→B, or ¬B→A. Notice, though, that the definition A∨B := (A→B)→B contains no negations. On the other hand, A∧B cannot be defined in terms of implication alone, without using negation.
In a sense, the expressions A∧B and A∨B can be thought of as "black boxes". Inside, these black boxes contain formulas made up only of implication and negation. The black boxes can contain anything, as long as when plugged into the AND-1 through AND-3 and OR-1 through OR-3 axioms of standard PC the axioms remain true. These axioms provide complete syntactic definitions of the conjunction
and disjunction
operators.
The next set of theorems will aim to find the remaining four axioms of Frege's PC within the "theorem-space" of standard PC, showing that the theory of Frege's PC is contained within the theory of standard PC.
Theorem ST1: A→A
Theorem ST2: A→¬¬A
ST2 is axiom FRG-3 of Frege's PC.
Theorem ST3: B∨C→(¬C→B)
Theorem ST4: ¬¬A→A
ST4 is axiom FRG-2 of Frege's PC.
Prove ST5: (A→(B→C))→(B→(A→C))
ST5 is axiom THEN-3 of Frege's PC.
Theorem ST6: (A→B)→(¬B→¬A)
ST6 is axiom FRG-1 of Frege's PC.
Each of Frege's axioms can be derived from the standard axioms, and each of the standard axioms can be derived from Frege's axioms. This means that the two sets of axioms are interdependent and there is no axiom in one set which is independent from the other set. Therefore the two sets of axioms generate the same theory: Frege's PC is equivalent to standard PC.
(For if the theories should be different, then one of them should contain theorems not contained by the other theory. These theorems can be derived from their own theory's axiom set: but as has been shown this entire axiom set can be derived from the other theory's axiom set, which means that the given theorems can actually be derived solely from the other theory's axiom set, so that the given theorems also belong to the other theory. Contradiction: thus the two axiom sets span the same theorem-space. By construction: Any theorem derived from the standard axioms can be derived from Frege's axioms, and vice versa, by first proving as theorems the axioms of the other theory as shown above and then using those theorems as lemmas to derive the desired theorem.)
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
Frege's propositional calculus was the first axiomatization of propositional calculus
Propositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
. It was invented by Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus (although Charles Peirce was the first to use the term "second-order" and developed his own version of the predicate calculus independently of Frege).
It makes use of just two logical operators: implication and negation, and it is constituted by six axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s and one inference rule: modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
.
Axioms
THEN-1: A → (B → A)
THEN-2: (A → (B → C)) → ((A → B) → (A → C))
THEN-3: (A → (B → C)) → (B → (A → C))
FRG-1: (A → B) → (¬B → ¬A)
FRG-2: ¬¬A → A
FRG-3: A → ¬¬A
Inference Rule
MP: P, P→Q ⊢ Q
Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN-1 and THEN-2. Notice that axioms THEN-1 through THEN-3 only make use of (and define) the implication operator, whereas axioms FRG-1 through FRG-3 define the negation operator.
The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem-space" of Frege's PC, showing that the theory of standard PC is contained within the theory of Frege's PC.
(A theory, also called here, for figurative purposes, a "theorem-space", is a set of theorems which are a subset of a universal set of well-formed formula
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
s. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem-space are found the axioms, which "generate" the theorem-space much like a generating set
Generating set
In mathematics, the expressions generator, generate, generated by and generating set can have several closely related technical meanings:...
generates a group.)
Rule THEN-1*: A ⊢ B→A
| # | wff | reason |
|---|---|---|
| 1. | A | premise |
| 2. | A→(B→A) | THEN-1 |
| 3. | B→A | MP 1,2. |
Rule THEN-2*: A→(B→C) ⊢ (A→B)→(A→C)
| # | wff | reason |
|---|---|---|
| 1. | A→(B→C) | premise |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | THEN-2 |
| 3. | (A→B)→(A→C) | MP 1,2. |
Rule THEN-3*: A→(B→C) ⊢ B→(A→C)
| # | wff | reason |
|---|---|---|
| 1. | A→(B→C) | premise |
| 2. | (A → (B → C)) → (B → (A → C)) | THEN-3 |
| 3. | B→(A→C) | MP 1,2. |
Rule FRG-1*: A→B ⊢ ¬B→¬A
| # | wff | reason |
|---|---|---|
| 1. | (A→B)→(¬B→¬A) | FRG-1 |
| 2. | A→B | premise |
| 3. | ¬B→¬A | MP 2,1. |
Rule TH1*: A→B, B→C ⊢ A→C
| # | wff | reason |
|---|---|---|
| 1. | B→C | premise |
| 2. | (B→C)→(A→(B→C)) | THEN-1 |
| 3. | A→(B→C) | MP 1,2 |
| 4. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 5. | (A→B)→(A→C) | MP 3,4 |
| 6. | A→B | premise |
| 7. | A→C | MP 6,5. |
Theorem TH1: (A→B)→((B→C)→(A→C))
| # | wff | reason |
|---|---|---|
| 1. | (B→C)→(A→(B→C)) | THEN-1 |
| 2. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 3. | (B→C)→((A→B)→(A→C)) | TH1* 1,2 |
| 4. | ((B→C)→((A→B)→(A→C)))→((A→B)→((B→C)→(A→C))) | THEN-3 |
| 5. | (A→B)→((B→C)→(A→C)) | MP 3,4. |
Theorem TH2: A→(¬A→¬B)
| # | wff | reason |
|---|---|---|
| 1. | A→(B→A) | THEN-1 |
| 2. | (B→A)→(¬A→¬B) | FRG-1 |
| 3. | A→(¬A→¬B) | TH1* 1,2. |
Theorem TH3: ¬A→(A→¬B)
| # | wff | reason |
|---|---|---|
| 1. | A→(¬A→¬B) | TH 2 |
| 2. | (A→(¬A→¬B))→(¬A→(A→¬B)) | THEN-3 |
| 3. | ¬A→(A→¬B) | MP 1,2. |
Theorem TH4: ¬(A→¬B)→A
| # | wff | reason |
|---|---|---|
| 1. | ¬A→(A→¬B) | TH3 |
| 2. | (¬A→(A→¬B))→(¬(A→¬B)→¬¬A) | FRG-1 |
| 3. | ¬(A→¬B)→¬¬A | MP 1,2 |
| 4. | ¬¬A→A | FRG-2 |
| 5. | ¬(A→¬B)→A | TH1* 3,4. |
Theorem TH5: (A→¬B)→(B→¬A)
| # | wff | reason |
|---|---|---|
| 1. | (A→¬B)→(¬¬B→¬A) | FRG-1 |
| 2. | ((A→¬B)→(¬¬B→¬A))→(¬¬B→((A→¬B)→¬A)) | THEN-3 |
| 3. | ¬¬B→((A→¬B)→¬A) | MP 1,2 |
| 4. | B→¬¬B | FRG-3, with A := B |
| 5. | B→((A→¬B)→¬A) | TH1* 4,3 |
| 6. | (B→((A→¬B)→¬A))→((A→¬B)→(B→¬A)) | FRG-1 |
| 7. | (A→¬B)→(B→¬A) | MP 5,6. |
Theorem TH6: ¬(A→¬B)→B
| # | wff | reason |
|---|---|---|
| 1. | ¬(B→¬A)→B | TH4, with A := B, B := A |
| 2. | (B→¬A)→(A→¬B) | TH5, with A := B, B := A |
| 3. | ((B→¬A)→(A→¬B))→(¬(A→¬B)→¬(B→¬A)) | FRG-1 |
| 4. | ¬(A→¬B)→¬(B→¬A) | MP 2,3 |
| 5. | ¬(A→¬B)→B | TH1* 4,1. |
Theorem TH7: A→A
| # | wff | reason |
|---|---|---|
| 1. | A→¬¬A | FRG-3 |
| 2. | ¬¬A→A | FRG-2 |
| 3. | A→A | TH1* 1,2. |
Theorem TH8: A→((A→B)→B)
| # | wff | reason |
|---|---|---|
| 1. | (A→B)→(A→B) | TH7, with A := A→B |
| 2. | ((A→B)→(A→B))→(A→((A→B)→B)) | THEN-3 |
| 3. | A→((A→B)→B) | MP 1,2. |
Theorem TH9: B→((A→B)→B)
| # | wff | reason |
|---|---|---|
| 1. | B→((A→B)→B) | THEN-1, with A := B, B := A→B. |
Theorem TH10: A→(B→¬(A→¬B))
| # | wff | reason |
|---|---|---|
| 1. | (A→¬B)→(A→¬B) | TH7 |
| 2. | ((A→¬B)→(A→¬B))→(A→((A→¬B)→¬B) | THEN-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. |
Note: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), and A→(B→¬(A→¬B)) (TH10), so ¬(A→¬B) behaves just like A∧B (compare with axioms AND-1, AND-2, and AND-3).
Theorem TH11: (A→B)→((A→¬B)→¬A)
| # | wff | reason |
|---|---|---|
| 1. | A→(B→¬(A→¬B)) | TH10 |
| 2. | (A→(B→¬(A→¬B)))→((A→B)→(A→¬(A→¬B))) | THEN-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 is axiom NOT-1 of standard PC, called "reductio ad absurdum
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
".
Theorem TH12: ((A→B)→C)→(A→(B→C))
| # | wff | reason |
|---|---|---|
| 1. | B→(A→B) | THEN-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)) | THEN-1 |
| 5. | ((A→B)→C)→(A→(B→C)) | TH1* 3,4. |
Theorem TH13: (B→(B→C))→(B→C)
| # | wff | reason |
|---|---|---|
| 1. | (B→(B→C)) → ((B→B)→(B→C)) | THEN-2 |
| 2. | (B→B)→ ( (B→(B→C)) → (B→C)) | THEN-3* 1 |
| 3. | B→B | TH7 |
| 4. | (B→(B→C)) → (B→C) | MP 3,2. |
Rule TH14*: A→(B→P), P→Q ⊢ A→(B→Q)
| # | wff | reason |
|---|---|---|
| 1. | P→Q | premise |
| 2. | (P→Q)→(B→(P→Q)) | THEN-1 |
| 3. | B→(P→Q) | MP 1,2 |
| 4. | (B→(P→Q))→((B→P)→(B→Q)) | THEN-2 |
| 5. | (B→P)→(B→Q) | MP 3,4 |
| 6. | ((B→P)→(B→Q))→ (A→((B→P)→(B→Q))) | THEN-1 |
| 7. | A→((B→P)→(B→Q)) | MP 5,6 |
| 8. | (A→(B→P))→(A→(B→Q)) | THEN-2* 7 |
| 9. | A→(B→P) | premise |
| 10. | A→(B→Q) | MP 9,8. |
Theorem TH15: ((A→B)→(A→C))→(A→(B→C))
| # | wff | reason |
|---|---|---|
| 1. | ((A→B)→(A→C))→(((A→B)→A)→((A→B)→C)) | THEN-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))) | THEN-3* 3 |
| 5. | A→((A→B)→A) | THEN-1 |
| 6. | A→ ( ((A→B) →(A→C))→(A→(B→C)) ) | TH1* 5,4 |
| 7. | ((A→B)→(A→C))→(A→(A→(B→C))) | THEN-3* 6 |
| 8. | (A→(A→(B→C)))→(A→(B→C)) | TH13 |
| 9. | ((A→B)→(A→C))→(A→(B→C)) | TH1* 7,8. |
Theorem TH15 is the converse
Converse
Converse is an American shoe company that has been making shoes, lifestyle fashion and athletic apparel since the early 20th century. Converse is one of the earliest pioneers in the sneaker and sporting good industry founded in 1908.- 1908–1941: Early days :...
of axiom THEN-2.
Theorem TH16: (¬A→¬B)→(B→A)
| # | wff | reason |
|---|---|---|
| 1. | (¬A→¬B)→(¬¬B→¬¬A) | FRG-1 |
| 2. | ¬¬B→((¬A→¬B)→¬¬A) | THEN-3* 1 |
| 3. | B→¬¬B | FRG-3 |
| 4. | B→((¬A→¬B)→¬¬A) | TH1* 3,2 |
| 5. | (¬A→¬B)→(B→¬¬A) | THEN-3* 4 |
| 6. | ¬¬A→A | FRG-2 |
| 7. | (¬¬A→A)→(B→(¬¬A→A)) | THEN-1 |
| 8. | B→(¬¬A→A) | MP 6,7 |
| 9. | (B→(¬¬A→A))→((B→¬¬A)→(B→A)) | THEN-2 |
| 10. | (B→¬¬A)→(B→A) | MP 8,9 |
| 11. | (¬A→¬B)→(B→A) | TH1* 5,10. |
Theorem TH17: (¬A→B)→(¬B→A)
| # | wff | reason |
|---|---|---|
| 1. | (¬A→¬¬B)→(¬B→A) | TH16, with B := ¬B |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | (¬A→B)→(¬B→A) | TH1* 6,1. |
Compare TH17 with theorem TH5.
Theorem TH18: ((A→B)→B)→(¬A→B)
| # | wff | reason |
|---|---|---|
| 1. | (A→B)→(¬B→(A→B)) | THEN-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)) | THEN-2 |
| 9. | (¬B→¬(A→B))→(¬B→A) | MP 7,8 |
| 10. | ((A→B)→B) → (¬B→¬(A→B)) | FRG-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. |
Theorem TH19: (A→C)→ ((B→C)→(((A→B)→B)→C))
| # | wff | reason |
|---|---|---|
| 1. | ¬A→(¬B→¬(¬A→¬¬B)) | TH10 |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | ¬(¬A→¬¬B)→¬(¬A→B) | FRG-1* 6 |
| 8. | ¬A→(¬B→¬(¬A→B)) | TH14* 1,7 |
| 9. | ((A→B)→B)→(¬A→B) | TH18 |
| 10. | ¬(¬A→B)→¬((A→B)→B) | FRG-1* 9 |
| 11. | ¬A→(¬B→¬((A→B)→B)) | TH14* 8,10 |
| 12. | ¬C→(¬A→(¬B→¬((A→B)→B))) | THEN-1* 11 |
| 13. | (¬C→¬A)→(¬C→(¬B→¬((A→B)→B))) | THEN-2* 12 |
| 14. | (¬C→(¬B→¬((A→B)→B))) → ((¬C→¬B)→(¬C→¬((A→B)→B))) | THEN-2 |
| 15. | (¬C→¬A)→ ((¬C→¬B)→(¬C→¬((A→B)→B))) | TH1* 13,14 |
| 16. | (A→C)→(¬C→¬A) | FRG-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) | FRG-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. |
Note: A→((A→B)→B) (TH8), B→((A→B)→B) (TH9), and
(A→C)→((B→C)→(((A→B)→B)→C)) (TH19), so ((A→B)→B) behaves just like A∨B. (Compare with axioms OR-1, OR-2, and OR-3.)
Theorem TH20: (A→¬A)→¬A
| # | wff | reason |
|---|---|---|
| 1. | (A→A)→((A→¬A)→¬A) | TH11 |
| 2. | A→A | TH7 |
| 3. | (A→¬A)→¬A | MP 2,1. |
TH20 corresponds to axiom NOT-3 of standard PC, called "tertium non datur".
Theorem TH21: A→(¬A→B)
| # | wff | reason |
|---|---|---|
| 1. | A→(¬A→¬¬B) | TH2, with B := ~B |
| 2. | ¬¬B→B | FRG-2 |
| 3. | A→(¬A→B) | TH14* 1,2. |
TH21 corresponds to axiom NOT-2 of standard PC, called "ex contradictione quodlibet".
All the axioms of standard PC have be derived from Frege's PC, after having let
A∧B := ¬(A→¬B) and A∨B := (A→B)→B. These expressions are not unique, e.g. A∨B could also have been defined as (B→A)→A, ¬A→B, or ¬B→A. Notice, though, that the definition A∨B := (A→B)→B contains no negations. On the other hand, A∧B cannot be defined in terms of implication alone, without using negation.
In a sense, the expressions A∧B and A∨B can be thought of as "black boxes". Inside, these black boxes contain formulas made up only of implication and negation. The black boxes can contain anything, as long as when plugged into the AND-1 through AND-3 and OR-1 through OR-3 axioms of standard PC the axioms remain true. These axioms provide complete syntactic definitions of the conjunction
Logical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
and disjunction
Logical disjunction
In logic and mathematics, a two-place logical connective or, is a logical disjunction, also known as inclusive disjunction or alternation, that results in true whenever one or more of its operands are true. E.g. in this context, "A or B" is true if A is true, or if B is true, or if both A and B are...
operators.
The next set of theorems will aim to find the remaining four axioms of Frege's PC within the "theorem-space" of standard PC, showing that the theory of Frege's PC is contained within the theory of standard PC.
Theorem ST1: A→A
| # | wff | reason |
|---|---|---|
| 1. | (A→((A→A)→A))→((A→(A→A))→(A→A)) | THEN-2 |
| 2. | A→((A→A)→A) | THEN-1 |
| 3. | (A→(A→A))→(A→A) | MP 2,1 |
| 4. | A→(A→A) | THEN-1 |
| 5. | A→A | MP 4,3. |
Theorem ST2: A→¬¬A
| # | wff | reason |
|---|---|---|
| 1. | A | hypothesis |
| 3. | A→(¬A→A) | THEN-1 |
| 4. | ¬A→A | MP 1,3 |
| 6. | ¬A→¬A | ST1 |
| 7. | (¬A→A)→((¬A→¬A)→¬¬A) | NOT-1 |
| 8. | (¬A→¬A)→¬¬A | MP 4,7 |
| 9. | ¬¬A | MP 6,8 |
| 10. | A ⊢ ¬¬A | summary 1-9 |
| 11. | A→¬¬A | DT 10. |
ST2 is axiom FRG-3 of Frege's PC.
Theorem ST3: B∨C→(¬C→B)
| # | wff | reason |
|---|---|---|
| 1. | C→(¬C→B) | NOT-2 |
| 2. | B→(¬C→B) | THEN-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. |
Theorem ST4: ¬¬A→A
| # | wff | reason |
|---|---|---|
| 1. | A∨¬A | NOT-3 |
| 2. | (A∨¬A)→(¬¬A→A) | ST3 |
| 3. | ¬¬A→A | MP 1,2. |
ST4 is axiom FRG-2 of Frege's PC.
Prove ST5: (A→(B→C))→(B→(A→C))
| # | wff | reason |
|---|---|---|
| 1. | A→(B→C) | hypothesis |
| 2. | B | hypothesis |
| 3. | A | hypothesis |
| 4. | B→C | MP 3,1 |
| 5. | C | MP 2,4 |
| 6. | A→(B→C), B, A ⊢ C | summary 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 is axiom THEN-3 of Frege's PC.
Theorem ST6: (A→B)→(¬B→¬A)
| # | wff | reason |
|---|---|---|
| 1. | A→B | hypothesis |
| 2. | ¬B | hypothesis |
| 3. | ¬B→(A→¬B) | THEN-1 |
| 4. | A→¬B | MP 2,3 |
| 5. | (A→B)→((A→¬B)→¬A) | NOT-1 |
| 6. | (A→¬B)→¬A | MP 1,5 |
| 7. | ¬A | MP 4,6 |
| 8. | A→B, ¬B ⊢ ¬A | summary 1-7 |
| 9. | A→B ⊢ ¬B→¬A | DT 8 |
| 10. | (A→B)→(¬B→¬A) | DT 9. |
ST6 is axiom FRG-1 of Frege's PC.
Each of Frege's axioms can be derived from the standard axioms, and each of the standard axioms can be derived from Frege's axioms. This means that the two sets of axioms are interdependent and there is no axiom in one set which is independent from the other set. Therefore the two sets of axioms generate the same theory: Frege's PC is equivalent to standard PC.
(For if the theories should be different, then one of them should contain theorems not contained by the other theory. These theorems can be derived from their own theory's axiom set: but as has been shown this entire axiom set can be derived from the other theory's axiom set, which means that the given theorems can actually be derived solely from the other theory's axiom set, so that the given theorems also belong to the other theory. Contradiction: thus the two axiom sets span the same theorem-space. By construction: Any theorem derived from the standard axioms can be derived from Frege's axioms, and vice versa, by first proving as theorems the axioms of the other theory as shown above and then using those theorems as lemmas to derive the desired theorem.)