In metalogic and metamathematics, Frege's theorem is a metatheorem stating that the Peano axioms of arithmetic can be derived in second-order logic from Hume's principle. Gottlob Frege first proved it informally in his 1884 The Foundations of Arithmetic and more formally in his 1893 Grundgesetze der Arithmetik I, and Crispin Wright rediscovered it in the early 1980s, since which it has been the focus of significant work at the core of the philosophy of mathematics known as neo-logicism.
Facts
StatementThe Peano axioms of arithmetic can be derived in second-order logic from Hume's principle. 1 Classification
Statement FormCharacterization Theorem 1 Connections
Has Statement Form
Entity-backed identity for the statement-form enum value this theorem already carries, resolved to a mathematics concept by an explicit value-to-entity map (phase 3 bucket conversion, docs\design_entity_backed_browse_buckets_20260928.md). The statement-form fact itself stays on the theorem unchanged.
In Branch
Source Frege's theorem, Wikipedia
Sources
1. Frege's theorem, Wikipedia
Introduction, statement
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.
Introduction, first proof
It was first proven, informally, by Gottlob Frege in his 1884 The Foundations of Arithmetic
In Branch: Logic and Foundations, Lead sentence
In metalogic and metamathematics, Frege's theorem is a metatheorem that states that the Peano axioms of arithmetic can be derived
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.