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).

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]

(	P	→	(	Q	→	R	))	→	((	P	→	Q	)	→	(	P	→	R	))
		Y			✓			Y		✗	✓	✗		Y		✗	✓	✗
		Y			✓			Y		✗	✓	✗		Y		✗	✓	✓
		Y			✗			Y		✗	✓	✓		Y		✗	✓	✗
		Y			✓			Y		✗	✓	✓		Y		✗	✓	✓
		Y			✓			Y		✓	✗	✗		Y		✓	✗	✗
		Y			✓			Y		✓	✗	✗		Y		✓	✓	✓
		N			✗			Y		✓	✓	✓		N		✓	✗	✗
		Y			✓			Y		✓	✓	✓		Y		✓	✓	✓
	1	2		3	4	5		6		7	8	9		10		11	12	13

In propositional logic, Frege's theorem refers to this tautology:

${\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 ${\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.

One commonly takes ${\displaystyle \neg P}$ to mean ${\displaystyle P\to \bot }$, where ${\displaystyle \bot }$ denotes a false proposition. With ${\displaystyle \bot }$ for ${\displaystyle R}$, the theorem entails the curried form of the negation introduction principle,

${\displaystyle {\big (}(P\to \neg Q{\big )}\land (P\to Q){\big )}\to \neg P}$

• 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