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 1884 The Foundations of ArithmeticGottlob Frege, Die Grundlagen der Arithmetik, Breslau: Verlag von Wilhelm Koebner, 1884, §63. and proven more formally in his 1893 I (Basic Laws of Arithmetic I).Gottlob Frege, I, Jena: Verlag Hermann Pohle, 1893, §§20 and 47. 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 (at least of the Scottish School variety).
Overview In The Foundations of Arithmetic (1884), and later, in Basic Laws of Arithmetic (vol. 1, 1893; vol. 2, 1903), Frege attempted to derive all of the laws of arithmetic from axioms he asserted as logical (see logicism). Most of these axioms were carried over from his ; the one truly new principle was one he called the Basic Law V (now known as the axiom schema of unrestricted comprehension):Richard Pettigrew, "Basic set theory", January 26, 2012, p. 2. the "value-range" of the function f(x) is the same as the "value-range" of the function g(x) if and only if ∀x[f(x) = g(x)]. However, not only did Basic Law V fail to be a logical proposition, but the resulting system proved to be inconsistent, because it was subject to Russell's paradox..
The inconsistency in Frege's overshadowed Frege's achievement: according to Edward Zalta, the "contains all the essential steps of a valid proof (in second-order logic) of the fundamental propositions of arithmetic from a single consistent principle." This achievement has become known as Frege's theorem.
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 theorem refers to this tautology:
The theorem already holds in one of the weakest logics imaginable, the constructive implicational calculus. The proof under the Brouwer–Heyting–Kolmogorov interpretation reads . In words: "Let f denote a reason that P implies that Q implies R. And let g denote a reason that P implies Q. Then given a f, then given a g, then given a reason p for P, we know both that Q holds by g and that Q implies R holds by f. So R holds."
The truth table to the right gives a semantic 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.
Special cases One commonly takes to mean , where denotes a false proposition. With for , the theorem entails the curried form of the negation introduction principle,
Notes
References
– Edition in modern notation – Edition in modern notation