Frege's theorem
Template:Short description 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 Die Grundlagen der Arithmetik (The Foundations of Arithmetic)[1] and proven more formally in his 1893 Grundgesetze der Arithmetik I (Basic Laws of Arithmetic I).[2] 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 Begriffsschrift; the one truly new principle was one he called the Basic Law V[2] (now known as the axiom schema of unrestricted comprehension):[3] 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.[4]
The inconsistency in Frege's Grundgesetze overshadowed Frege's achievement: according to Edward Zalta, the Grundgesetze "contains all the essential steps of a valid proof (in second-order logic) of the fundamental propositions of arithmetic from a single consistent principle."[4] This achievement has become known as Frege's theorem.[4][5]
Frege's theorem in propositional logic
In propositional logic, Frege's theorem refers to this tautology:
- (P → (Q→R)) → ((P→Q) → (P→R))
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 that both 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 (Template:N&) or true (Template:Y&) 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.
Notes
References
- Template:Cite book
- Template:Cite book – Edition Template:Webarchive in modern notation
- Template:Cite book – Edition Template:Webarchive in modern notation
- ↑ Gottlob Frege, Die Grundlagen der Arithmetik, Breslau: Verlag von Wilhelm Koebner, 1884, §63.
- ↑ 2.0 2.1 Gottlob Frege, Grundgesetze der Arithmetik I, Jena: Verlag Hermann Pohle, 1893, §§20 and 47.
- ↑ Richard Pettigrew, "Basic set theory", January 26, 2012, p. 2.
- ↑ 4.0 4.1 4.2 Template:Citation.
- ↑ Template:Cite book