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 Arithmetic and proven more formally in his 1893 Grundgesetze der Arithmetik I (Basic Laws of Arithmetic I). 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 (now known as the axiom schema of unrestricted comprehension): 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 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." This achievement has become known as Frege's theorem.
Frege's theorem in propositional logic
In propositional logic, Frege's theorem refers to this tautology:
( P → ( Q → R ) ) → ( ( P → Q ) → ( P → R ) ) {\displaystyle {\big (}P\to (Q\to R){\big )}\to {\big (}(P\to Q)\to (P\to R){\big )}}
The theorem already holds in one of the weakest logics imaginable, the constructive implicational calculus. The proof under the Brouwer–Heyting–Kolmogorov interpretation reads f ↦ g ↦ p ↦ ( f ( p ) ∘ g ) ( p ) {\displaystyle f\mapsto g\mapsto p\mapsto (f(p)\circ g)(p)} . 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 ¬ P {\displaystyle \neg P} to mean P → ⊥ {\displaystyle P\to \bot } , where ⊥ {\displaystyle \bot } denotes a false proposition. With ⊥ {\displaystyle \bot } for R {\displaystyle R} , the theorem entails the curried form of the negation introduction principle,
( ( P → ¬ Q ) ∧ ( P → Q ) ) → ¬ P {\displaystyle {\big (}(P\to \neg Q{\big )}\land (P\to Q){\big )}\to \neg P}
Notes
References Gottlob Frege (1884). Die Grundlagen der Arithmetik – eine logisch-mathematische Untersuchung über den Begriff der Zahl (PDF) (in German). Breslau: Verlag von Wilhelm Koebner. Gottlob Frege (1893). Grundgesetze der Arithmetik (in German). Vol. 1. Jena: Verlag Hermann Pohle. – Edition Archived 2016-10-21 at the Wayback Machine in modern notation Gottlob Frege (1903). Grundgesetze der Arithmetik (in German). Vol. 2. Jena: Verlag Hermann Pohle. – Edition Archived 2017-08-29 at the Wayback Machine in modern notation