Frege's propositional calculus


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.
It makes use of just two logical operators: implication and negation, and it is constituted by six axioms and one inference rule: modus ponens.
AxiomsInference Rule

;THEN-1: A →
;THEN-2: → → )
;THEN-3: →
;FRG-1: →
;FRG-2: ¬¬A → A
;FRG-3: A → ¬¬A
;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 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.

Rules

#wffreason
1.A premise
2.A→ THEN-1
3.B→AMP 1,2.

#wffreason
1.A→premise
2. → → )THEN-2
3.→MP 1,2.

#wffreason
1.A→premise
2. → THEN-3
3.B→MP 1,2.

#wffreason
1.→FRG-1
2.A→Bpremise
3.¬B→¬AMP 2,1.

Theorems

#wffreason
1.→THEN-1
2.→→)THEN-2
3.→→)TH1* 1,2
4.→→))→→→))THEN-3
5.→→)MP 3,4.

#wffreason
1.A→THEN-1
2.→FRG-1
3.A→TH1* 1,2.

#wffreason
1.A→TH 2
2.→ THEN-3
3.¬A→MP 1,2.

#wffreason
1.¬A→TH3
2.→FRG-1
3.¬→¬¬A MP 1,2
4.¬¬A→AFRG-2
5.¬→ATH1* 3,4.

#wffreason
1.→FRG-1
2.→)→)THEN-3
3.¬¬B→MP 1,2
4.B→¬¬BFRG-3, with A := B
5.B→TH1* 4,3
6.)→→)THEN-3
7.→MP 5,6.

#wffreason
1.¬→BTH4, with A := B, B := A
2.→TH5, with A := B, B := A
3.→)→→¬)FRG-1
4.¬→¬MP 2,3
5.¬→BTH1* 4,1.

#wffreason
1.A→¬¬AFRG-3
2.¬¬A→AFRG-2
3.A→ATH1* 1,2.

#wffreason
1.→TH7, with A := A→B
2.→)→)THEN-3
3.A→MP 1,2.

#wffreason
1.B→THEN-1, with A := B, B := A→B.

#wffreason
1.→TH7
2.→)→THEN-3
3.A→MP 1,2
4.→TH5
5.A→TH1* 3,4.

Note: ¬→A, ¬→B, and A→, so ¬ behaves just like A∧B.
#wffreason
1.A→TH10
2.→THEN-2
3.→MP 1,2
4.→TH5
5.→TH1* 3,4.

TH11 is axiom NOT-1 of standard PC, called "reductio ad absurdum".
#wffreason
1.B→THEN-1
2.→→)TH1
3.→MP 1,2
4.→THEN-1
5.→TH1* 3,4.

#wffreason
1. → →)THEN-2
2.→ )THEN-3* 1
3.B→BTH7
4. → MP 3,2.

#wffreason
1.P→Qpremise
2.→THEN-1
3.B→MP 1,2
4.→→)THEN-2
5.→MP 3,4
6.→)→ →))THEN-1
7.A→→)MP 5,6
8.→THEN-2* 7
9.A→premise
10.A→MP 9,8.

#wffreason
1.→)→→)THEN-2
2.→TH12
3.→)→→)TH14* 1,2
4.→ →)→)THEN-3* 3
5.A→THEN-1
6.A→ →)→ )TH1* 5,4
7.→)→THEN-3* 6
8.→TH13
9.→)→TH1* 7,8.

Theorem TH15 is the converse of axiom THEN-2.
#wffreason
1.→FRG-1
2.¬¬B→THEN-3* 1
3.B→¬¬BFRG-3
4.B→TH1* 3,2
5.→THEN-3* 4
6.¬¬A→AFRG-2
7.→THEN-1
8.B→MP 6,7
9.→→)THEN-2
10.→MP 8,9
11.→TH1* 5,10.

#wffreason
1.→TH16, with B := ¬B
2.B→¬¬BFRG-3
3.→THEN-1
4.¬A→MP 2,3
5.→→)THEN-2
6.→MP 4,5
7.→TH1* 6,1.

Compare TH17 with theorem TH5.
#wffreason
1.→THEN-1
2.→TH16
3.→TH1* 2,1
4.→TH15
5.¬B→MP 3,4
6.→TH17
7.¬B→TH1* 5,6
8.→ )THEN-2
9.→MP 7,8
10. → FRG-1
11.→TH1* 10,9
12.→TH17
13.→TH1* 11,12.

#wffreason
1.¬A→TH10
2.B→¬¬BFRG-3
3.→THEN-1
4.¬A→MP 2,3
5.→→)THEN-2
6.→MP 4,5
7.¬→¬FRG-1* 6
8.¬A→TH14* 1,7
9.→TH18
10.¬→¬FRG-1* 9
11.¬A→)TH14* 8,10
12.¬C→))THEN-1* 11
13.→))THEN-2* 12
14.)) → →))THEN-2
15.→ →))TH1* 13,14
16.→FRG-1
17.→→))TH1* 16,15
18.)→→C)TH16
19.→ →→C))TH14* 17,18
20.→FRG-1
21.→)→
→ →C) ) → → →C)))		TH1
22.→ →C) ) → → →C))MP 20,21
23.→ →→C))TH1* 19,22.

Note: A→, B→, and
→→→C)), so behaves just like A∨B.
#wffreason
1.→TH11
2.A→ATH7
3.→¬AMP 2,1.

TH20 corresponds to axiom NOT-3 of standard PC, called "tertium non datur".
#wffreason
1.A→TH2, with B := ~B
2.¬¬B→BFRG-2
3.A→TH14* 1,2.

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 := ¬ and A∨B := →B. These expressions are not unique, e.g. A∨B could also have been defined as →A, ¬A→B, or ¬B→A. Notice, though, that the definition 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.
#wffreason
1.)→)THEN-2
2.A→THEN-1
3.→MP 2,1
4.A→THEN-1
5.A→AMP 4,3.

#wffreason
1.Ahypothesis
2.A→THEN-1
3.¬A→AMP 1,2
4.¬A→¬AST1
5.→NOT-1
6.→¬¬AMP 3,5
7.¬¬AMP 4,6
8.A ⊢ ¬¬Asummary 1-7
9.A→¬¬ADT 8.

ST2 is axiom FRG-3 of Frege's PC.
#wffreason
1.C→NOT-2
2.B→THEN-1
3.→ →))OR-3
4.→→)MP 2,3
5.B∨C→MP 1,4.

#wffreason
1.A∨¬ANOT-3
2.→ST3
3.¬¬A→AMP 1,2.

ST4 is axiom FRG-2 of Frege's PC.
Prove ST5: →
#wffreason
1.A→hypothesis
2.Bhypothesis
3.Ahypothesis
4.B→CMP 3,1
5.CMP 2,4
6.A→, B, A ⊢ Csummary 1-5
7.A→, B ⊢ A→CDT 6
8.A→ ⊢ B→DT 7
9. → DT 8.

ST5 is axiom THEN-3 of Frege's PC.
#wffreason
1.A→Bhypothesis
2.¬Bhypothesis
3.¬B→THEN-1
4.A→¬BMP 2,3
5.→NOT-1
6.→¬AMP 1,5
7.¬AMP 4,6
8.A→B, ¬B ⊢ ¬Asummary 1-7
9.A→B ⊢ ¬B→¬ADT 8
10.→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.