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 1884 ''Die Grundlagen der Arithmetik'' ('' The Foundations of Arithmetic'')Gottlob Frege, ''Die Grundlagen der Arithmetik'', Breslau: Verlag von Wilhelm Koebner, 1884, §63. and proven more formally in his 1893 ''Grundgesetze der Arithmetik'' I (''Basic Laws of Arithmetic'' I).Gottlob Frege, ''Grundgesetze der Arithmetik'' 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 ''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:

:$\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 \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 $\neg P$ to mean $P\to\bot$, where $\bot$ denotes a false proposition.
With $\bot$ for $R$, the theorem entails the curried form of the negation introduction principle,
:$\big((P\to \neg Q\big)\land (P\to Q)\big) \to \neg P$

Notes

References

*
* &ndash
Edition
in modern notation
* &ndash
Edition
in modern notation

{{DEFAULTSORT:Frege's Theorem
Theorems in the foundations of mathematics
Theorems in propositional logic
Metatheorems