Frege's theorem
In metalogic and metamathematics, Frege's theorem is a metatheorem that states that the Peano axioms of arithmetic can be derived in second-order logic from Hume's principle. It was first proven, informally, by Gottlob Frege in his Die Grundlagen der Arithmetik (The Foundations of Arithmetic), published in 1884, and proven more formally in his Grundgesetze der Arithmetik (The Basic Laws of Arithmetic), published in two volumes, in 1893 and 1903. The theorem was re-discovered by Crispin Wright in the early 1980s and has since been the focus of significant work. It is at the core of the philosophy of mathematics known as neo-logicism.
Frege's theorem in propositional logic
( | P | → | ( | Q | → | R | )) | → | (( | P | → | Q | ) | → | ( | P | → | R | )) |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✗ | ![]() | ✗ | ✓ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✗ | ![]() | ✗ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✗ | ![]() | ![]() | ✗ | ✓ | ✓ | ![]() | ✗ | ✓ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✗ | ✓ | ✓ | ![]() | ✗ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✗ | ✗ | ![]() | ✓ | ✗ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✗ | ✗ | ![]() | ✓ | ✓ | ✓ | |||||||
![]() | ![]() | ![]() | ✗ | ![]() | ![]() | ✓ | ✓ | ✓ | ![]() | ✓ | ✗ | ✗ | |||||||
![]() | ![]() | ![]() | ✓ | ![]() | ![]() | ✓ | ✓ | ✓ | ![]() | ✓ | ✓ | ✓ | |||||||
1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 |
In propositional logic, Frege's theorems refers to this tautology:
- (P → (Q→R)) → ((P→Q) → (P→R))
The truth table to the right gives a proof. For all possible assignments of false (✗) or true (✓) to P, Q, and R (columns 1, 3, 5), each subformula is evaluated according to the rules for material conditional, the result being shown below its main operator. Column 6 shows that the whole formula evaluates to true in every case, i.e. that it is a tautology. In fact, its antecedent (column 2) and its consequent (column 10) are even equivalent.
References
- Zalta, Edward (2013), "Frege's Theorem and Foundations for Arithmetic", Stanford Encyclopedia of Philosophy.
- Gottlob Frege (1884). Die Grundlagen der Arithmetik — eine logisch-mathematische Untersuchung über den Begriff der Zahl (PDF) (in German). Breslau: Verlage Wilhelm Koebner.
- Gottlob Frege (1893). Grundgesetze der Arithmetik (in German). 1. Jena: Verlag Hermann Pohle. — Edition in modern notation
- Gottlob Frege (1903). Grundgesetze der Arithmetik (in German). 2. Jena: Verlag Hermann Pohle. — Edition in modern notation