Theorem (TH1) — (A→B)→((B→C)→(A→C))
More information #, wff ...
# |
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. |
Close
Theorem (TH2) — A→(¬A→¬B)
More information #, wff ...
# |
wff |
reason |
1. | A→(B→A) | THEN-1 |
2. | (B→A)→(¬A→¬B) | FRG-1 |
3. | A→(¬A→¬B) | TH1* 1,2. |
Close
Theorem (TH3) — ¬A→(A→¬B)
More information #, wff ...
# |
wff |
reason |
1. | A→(¬A→¬B) | TH 2 |
2. | (A→(¬A→¬B))→(¬A→(A→¬B)) | THEN-3 |
3. | ¬A→(A→¬B) | MP 1,2. |
Close
Theorem (TH4) — ¬(A→¬B)→A
More information #, wff ...
# |
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. |
Close
Theorem (TH5) — (A→¬B)→(B→¬A)
More information #, wff ...
# |
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)) |
THEN-3 |
7. | (A→¬B)→(B→¬A) | MP 5,6. |
Close
Theorem (TH6) — ¬(A→¬B)→B
More information #, wff ...
# |
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. |
Close
More information #, wff ...
# |
wff |
reason |
1. | A→¬¬A | FRG-3 |
2. | ¬¬A→A | FRG-2 |
3. | A→A | TH1* 1,2. |
Close
Theorem (TH8) — A→((A→B)→B)
More information #, wff ...
# |
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. |
Close
Theorem (TH9) — B→((A→B)→B)
More information #, wff ...
# |
wff |
reason |
1. | B→((A→B)→B) | THEN-1, with A := B, B := A→B. |
Close
Theorem (TH10) — A→(B→¬(A→¬B))
More information #, wff ...
# |
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. |
Close
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)
More information #, wff ...
# |
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. |
Close
TH11 is axiom NOT-1 of standard PC, called "reductio ad absurdum".
Theorem (TH12) — ((A→B)→C)→(A→(B→C))
More information #, wff ...
# |
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. |
Close
Theorem (TH13) — (B→(B→C))→(B→C)
More information #, wff ...
# |
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. |
Close
Rule (TH14) — A→(B→P), P→Q ⊢ A→(B→Q)
More information #, wff ...
# |
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. |
Close
Theorem (TH15) — ((A→B)→(A→C))→(A→(B→C))
More information #, wff ...
# |
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. |
Close
Theorem TH15 is the converse of axiom THEN-2.
Theorem (TH16) — (¬A→¬B)→(B→A)
More information #, wff ...
# |
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. |
Close
Theorem (TH17) — (¬A→B)→(¬B→A)
More information #, wff ...
# |
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. |
Close
Compare TH17 with theorem TH5.
Theorem (TH18) — ((A→B)→B)→(¬A→B)
More information #, wff ...
# |
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. |
Close
Theorem (TH19) — (A→C)→ ((B→C)→(((A→B)→B)→C))
More information #, wff ...
# |
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. |
Close
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
More information #, wff ...
# |
wff |
reason |
1. | (A→A)→((A→¬A)→¬A) | TH11 |
2. | A→A | TH7 |
3. | (A→¬A)→¬A | MP 2,1. |
Close
TH20 corresponds to axiom NOT-3 of standard PC, called "tertium non datur".
Theorem (TH21) — A→(¬A→B)
More information #, wff ...
# |
wff |
reason |
1. | A→(¬A→¬¬B) | TH2, with B := ~B |
2. | ¬¬B→B | FRG-2 |
3. | A→(¬A→B) | TH14* 1,2. |
Close
TH21 corresponds to axiom NOT-2 of standard PC, called "ex contradictione quodlibet".
All the axioms of standard PC have been 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.
More information #, wff ...
# |
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. |
Close
More information #, wff ...
# |
wff |
reason |
1. | A | hypothesis |
2. | A→(¬A→A) | THEN-1 |
3. | ¬A→A | MP 1,2 |
4. | ¬A→¬A | ST1 |
5. | (¬A→A)→((¬A→¬A)→¬¬A) | NOT-1 |
6. | (¬A→¬A)→¬¬A | MP 3,5 |
7. | ¬¬A | MP 4,6 |
8. |
A ⊢ ¬¬A |
summary 1-7 |
9. | A→¬¬A | DT 8. |
Close
ST2 is axiom FRG-3 of Frege's PC.
Theorem (ST3) — B∨C→(¬C→B)
More information #, wff ...
# |
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. |
Close
More information #, wff ...
# |
wff |
reason |
1. | A∨¬A | NOT-3 |
2. | (A∨¬A)→(¬¬A→A) | ST3 |
3. | ¬¬A→A | MP 1,2. |
Close
ST4 is axiom FRG-2 of Frege's PC.
Prove ST5: (A→(B→C))→(B→(A→C))
More information #, wff ...
# |
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. |
Close
ST5 is axiom THEN-3 of Frege's PC.
Theorem (ST6) — (A→B)→(¬B→¬A)
More information #, wff ...
# |
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. |
Close
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 that 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.)