Inmetalogic andmetamathematics,Frege's theorem is ametatheorem that states that thePeano axioms ofarithmetic can be derived insecond-order logic fromHume's principle. It was first proven, informally, byGottlob Frege in his 1884Die Grundlagen der Arithmetik (The Foundations of Arithmetic)^[1] and proven more formally in his 1893Grundgesetze der Arithmetik I (Basic Laws of Arithmetic I).^[2] The theorem was re-discovered byCrispin Wright in the early 1980s and has since been the focus of significant work. It is at the core of thephilosophy of mathematics known asneo-logicism (at least of theScottish School variety).

InThe Foundations of Arithmetic (1884), and later, inBasic 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 (seelogicism). Most of these axioms were carried over from hisBegriffsschrift; the one truly new principle was one he called theBasic Law V^[2] (now known as theaxiom schema of unrestricted comprehension):^[3] the "value-range" of the functionf(x) is the same as the "value-range" of the functiong(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 toRussell's paradox.^[4]

The inconsistency in Frege'sGrundgesetze overshadowed Frege's achievement: according toEdward Zalta, theGrundgesetze "contains all the essential steps of a valid proof (insecond-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

Inpropositional logic, Frege's theorem refers to thistautology:

${\displaystyle (P\to (Q\to R))\to ((P\to Q)\to (P\to R))}$

The theorem already holds in one of the weakest logics imaginable, the constructiveimplicational calculus. The proof under theBrouwer–Heyting–Kolmogorov interpretation reads${\displaystyle f\mapsto g\mapsto p\mapsto (f(p)\circ g)(p)}$. In words: "Letf denote a reason thatP implies thatQ impliesR. And letg denote a reason thatP impliesQ. Then given af, then given ag, then given a reasonp forP, we know that bothQ holds byg and thatQ impliesR holds byf. SoR holds."

Thetruth table to the right gives a semantic proof. For all possible assignments offalse (✗) ortrue (✓) toP,Q, andR (columns 1, 3, 5), each subformula is evaluated according to the rules formaterial conditional, the result being shown below its main operator. Column 6 shows that the whole formula evaluates totrue in every case, i.e. that it is a tautology. In fact, itsantecedent (column 2) and itsconsequent (column 10) are even equivalent.

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

${\displaystyle ((P\to \mathrm{\neg }Q)\wedge (P\to Q))\to \mathrm{\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. –EditionArchived 2016-10-21 at theWayback Machine in modern notation
• Gottlob Frege (1903).Grundgesetze der Arithmetik (in German). Vol. 2. Jena: Verlag Hermann Pohle. –EditionArchived 2017-08-29 at theWayback Machine in modern notation

• Theorems in the foundations of mathematics
• Theorems in propositional logic
• Metatheorems

• Articles with short description
• Short description is different from Wikidata
• CS1 German-language sources (de)
• Webarchive template wayback links