Frege

Frege, Gottlob, 1848-1925, German philosopher and mathematician. He was professor of mathematics (1879-1918) at the Univ. of Jena. Frege was one of the founders of modern symbolic logic, and his work profoundly influenced Bertrand Russell. He claimed that all mathematics could be derived from purely logical principles and definitions. He considered verbal concepts to be expressible as symbolic functions with one or more variables. His books include Begriffsschrift (1879); Die Grundlagen der Arithmetik (1884; tr. The Foundations of Arithmetic, 1950); Grundgesetze der Arithmetik (2 vol., 1893-1903).

(born Nov. 8, 1848, Wismar, Mecklenburg-Schwerin—died July 26, 1925, Bad Kleinen, Ger.) German mathematician and logician, inventor of modern mathematical logic and one of the founders of the analytic tradition in philosophy. He taught at the University of Jena from 1871 to 1917. His Begriffsschrift (1879, “Conceptscript”), was the first presentation of a system of mathematical logic in the modern sense. Using an original notation of quantifiers and variables, he was able to give formal expression to sentences containing multiple quantification, such as “Everybody loves someone”; this is impossible in the syllogistic derived from Aristotle, which had been considered complete until the time of Immanuel Kant (see predicate calculus). In the Die Grundlagen der Arithmetik he attempted to establish the doctrine later known as logicism. He also made significant contributions to the philosophy of language, including a highly influential theory of the distinction between sense and reference. Though Frege's work was admired by Bertrand Russell and the early Ludwig Wittgenstein, it was unknown to or ignored by most other philosophers and mathematicians during Frege's lifetime; its significance was not generally appreciated until the mid-20th century.

Learn more about Frege, (Friedrich Ludwig) Gottlob with a free trial on Britannica.com.

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 axioms 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 formulas. 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

#	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".

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 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 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

#	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.)

See also

• Begriffsschrift

References

• Buss, Samuel "An introduction to proof theory". Handbook of proof theory, 1–78. ISBN 0-444-89840-9. .