README⤓ .txt 2026-10-22T165042.936 000000000000656 First-order and higher-order theories: systems individuated by a non-logical signature and the axioms governing it, with the consequence relation inherited from a base logic rather than defined. Peano arithmetic does not have a logic of its own; it has classical first-order logic plus 0, S, +, ×, and induction. What makes it an object is the signature and the axioms, and what makes it worth an entry is that most of the collection's metatheory is about theories of this kind.
Structure Axiomatizations of order, algebra, and geometry: theories whose signature governs a structure rather than a foundation.
Ackermann Set Theory⤓ .md 2026-08-20T064854.000 000000000044800 Wilhelm Ackermann, "Zur Axiomatik der Mengenlehre" (Mathematische Annalen 131, 1956). Azriel Lévy ("On Ackermann's set theory", 1959; Lévy–Vaught 1961) proved ZF ⊆ A and showed a strong reflection principle holds in A, then asked whether the converse holds. William Reinhardt answered it: "Ackermann's set theory equals ZF" (Annals of Mathematical Logic 2, 1970).
Axiomatic Truth⤓ .md 2026-10-22T165042.936 000000000000720 Tarski (1933) showed truth is not definable in the object language and drew the hierarchy conclusion. The axiomatic alternative — add a truth predicate and axioms for it, rather than define it — was developed by Feferman (1962, 1991), Friedman and Sheard (1987), Cantini, Halbach (Axiomatic Theories of Truth, 2011), and Horsten. The Kripke–Feferman system axiomatizes what Kripke's fixed-point construction produces semantically.
Bounded Arithmetic⤓ .md 2026-08-20T062707.000 000000000054240 Buss introduced bounded arithmetic (S₂, 1986). Weak fragments of Peano arithmetic. Quantifiers bounded: ∀x≤t and ∃x≤t. Proof-theoretic characterization of complexity classes. Foundation for proof complexity and feasible mathematics.
Class Theories⤓ .md 2026-10-22T165042.936 000000000000712 John von Neumann (1925) axiomatized set theory with functions and a size restriction; Bernays (1937–1954) recast it with classes; Gödel used the result in his 1940 consistency proof for AC and GCH — which is why NBG is the system that constructibility was first done in. Morse and Kelley's stronger variant appeared in the appendix to Kelley's General Topology (1955).
Constructive Set Theory⤓ .md 2026-10-22T165042.936 000000000000784 Myhill and Aczel developed Constructive Zermelo-Fraenkel (CZF) set theory (1970s-80s). Intuitionistic set theory preserving constructive meaning. Alternative: Intuitionistic ZF (IZF). Foundation for constructive mathematics without choice or excluded middle.
Determinacy⤓ .md 2026-10-22T090550.000 000000000056408 Mycielski and Steinhaus, "A mathematical axiom contradicting the axiom of choice" (1962), proposed AD and showed it refutes AC. Solovay, Martin, and Moschovakis developed the structure theory through the 1970s; Martin (1975) proved Borel determinacy in ZF, and (1970) Π¹₁-determinacy from a measurable. Martin and Steel (1985/1989) derived projective determinacy from infinitely many Woodin cardinals; Woodin proved the converse direction and the theorem that L(ℝ) ⊨ AD.
Elementary Function Arithmetic⤓ .md 2026-10-22T090033.000 000000000041672 The theory IΔ₀+exp emerged from the study of weak fragments in the Paris–Wilkie school of the 1970s and 1980s. It acquired its programmatic importance from Harvey Friedman's grand conjecture (FOM posting, 1999): every theorem published in the Annals of Mathematics whose statement involves only finitary objects can be proved in EFA. Avigad's "Number theory and elementary arithmetic" (2003) is the standard case for the conjecture's plausibility.
ETCS⤓ .md 2026-10-22T090034.000 000000000045856 F. William Lawvere, "An elementary theory of the category of sets" (PNAS, 1964), written the year after his thesis and rejected by referees who could not see that it was a set theory. Lawvere and Rosebrugh's Sets for Mathematics (2003) is the textbook; Tom Leinster's "Rethinking set theory" (2014) is the readable case for it. The structural alternative to the cumulative hierarchy.
Fragments of Peano Arithmetic⤓ .md 2026-08-20T062815.000 000000000044736 Parsons, Mints, and Takeuti independently characterized the provably total functions of IΣ₁ (early 1970s). Paris and Kirby developed the model theory of the IΣₙ and BΣₙ hierarchies through the late 1970s; Paris and Harrington (1977) gave the first natural sentence independent of PA, sited exactly by this hierarchy. Hájek and Pudlák's Metamathematics of First-Order Arithmetic (1993) is the reference.
Frege Arithmetic⤓ .md 2026-08-20T062820.000 000000000042312 Frege's Grundlagen (1884) §63 states the principle and Grundgesetze (1893, 1903) derives arithmetic from it — but by way of Basic Law V, which Russell's paradox destroyed. Crispin Wright (Frege's Conception of Numbers as Objects, 1983) observed that the derivation only ever used Hume's Principle, and that HP is consistent where Law V is not. Boolos formalized and named the result: Frege's Theorem. Heck's work on Grundgesetze established that Frege himself had the derivation isolated.
Hereditarily Finite Set Theory⤓ .md 2026-08-20T062825.000 000000000044864 Ackermann, "Die Widerspruchsfreiheit der allgemeinen Mengenlehre" (1937), gave the coding of hereditarily finite sets by natural numbers that bears his name. Tarski, Mostowski, and Robinson (1953) identified adjunctive set theory as a minimal essentially undecidable theory; Nelson (Predicative Arithmetic, 1986) showed AS is interpretable in Q, closing the loop. Kaye and Wong ("On interpretations of arithmetic and set theory", 2007) established the precise bi-interpretability with PA; Damnjanović (BSL 23, 2017) tied the family to concatenation theory.
Heyting Arithmetic⤓ .md 2026-10-22T090552.000 000000000044040 Arend Heyting's formalization of intuitionistic logic (1930) supplied the base; the arithmetic is Peano's axioms over it. Gödel (1933) and Gentzen (independently) gave the negative translation showing PA is interpretable in HA, so the classical theory is consistent if the constructive one is. Kleene's realizability (1945) supplied the semantics that made HA an object of study rather than a restriction.
Inconsistent Mathematics⤓ .md 2026-10-22T090631.000 000000000049440 Robert K. Meyer's relevant arithmetic R# (1976) and his conjecture that it proves its own non-triviality; Ross Brady's non-triviality proof for naive set theory (1971, 1989); Chris Mortensen's Inconsistent Mathematics (1995), which named the programme; Graham Priest, "Inconsistent models of arithmetic" (1997); Zach Weber's Paradoxes and Inconsistent Mathematics (2021) for the current state.
Internal Set Theory⤓ .md 2026-10-22T090553.000 000000000045368 Edward Nelson, "Internal set theory: a new approach to nonstandard analysis" (Bulletin of the AMS 83, 1977). Robinson's nonstandard analysis (1966) built the hyperreals as an ultrapower and needed model theory to justify transfer; Nelson's move was syntactic — leave the universe alone, add a predicate to the language, and axiomatize it. Kanovei, Reeken, and Hrbáček developed the theory and its variants; Kanovei (1993) showed the reduction algorithm does not extend to all IST formulas.
Kripke-Platek Set Theory⤓ .md 2026-08-20T062832.000 000000000034840 Saul Kripke and Richard Platek, independently around 1964, from the same motivation: a set theory whose models are the right setting for generalized recursion theory. Jon Barwise's Admissible Sets and Structures (1975) is the reference and is where the theory acquired its name and its audience. The abbreviation collides with Kreisel–Putnam logic, which is unrelated.
Mereology⤓ .md 2026-10-22T090555.000 000000000042088 Leśniewski developed mereology (1916). Formal theory of parts and wholes. Alternative to set theory for some purposes. Developed by Leonard, Goodman, Simons, and others. Foundation for ontology and spatial reasoning.
New Foundations⤓ .md 2026-08-19T220636.000 000000000039984 W. V. Quine, "New foundations for mathematical logic" (American Mathematical Monthly, 1937), motivated by Russell's type theory: Quine's idea was to keep the type restriction on formulas and drop it from the ontology, so that there is one sort of object and the stratification is a syntactic condition. Specker (1953) proved NF refutes choice; Jensen (1969) showed the urelement variant NFU is consistent; Rosser's Logic for Mathematicians (1953) developed mathematics in it.
Non-well-founded Set Theory⤓ .md 2026-10-22T180154.561 000000000000816 Aczel formalized anti-foundation axiom (AFA, 1988). Allows sets to contain themselves and circular membership. Motivated by computer science (co-induction, bisimulation). Generalizes ZFC by replacing foundation axiom. Forti and Honsell had stated an equivalent axiom earlier (1983).
Omega-Logic⤓ .md 2026-10-22T165042.936 000000000000808 W. Hugh Woodin, The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal (1999) and "The continuum hypothesis, parts I and II" (Notices of the AMS, 2001). Bagaria, Castells, and Larson's survey (2006) is the standard introduction. Built for one question: whether the continuum hypothesis has a truth value that forcing cannot touch.
Ordinal Logic⤓ .md 2026-10-22T090631.000 000000000036496 Alan Turing, Systems of Logic Based on Ordinals (PhD thesis under Church, 1938; published 1939) — the work he did between the halting problem and Bletchley Park, and the deepest response to incompleteness anyone made. Solomon Feferman, "Transfinite recursive progressions of axiomatic theories" (1962), reworked it and drew the conclusions; Feferman and Spector (1962) supplied the limitative results.
Peano Arithmetic⤓ .md 2026-08-20T061919.000 000000000042224 Peano formalized arithmetic axioms (1889). Gödel proved incompleteness (1931): PA cannot prove its own consistency. Gentzen proved PA consistent using transfinite induction (1936). Foundation of metamathematics and proof theory. Various subsystems studied in reverse mathematics.
Positive Set Theory⤓ .md 2026-08-20T064841.000 000000000044448 Helen Skala and Isaac Malitz proposed positive comprehension in the 1970s; Forti and Hinnion, "The consistency problem for positive comprehension principles" (JSL 54, 1989), settled the basic questions and connected the theory to hyperuniverses (Forti–Honsell). Olivier Esser gave the theory its modern form and its metatheory in a sequence of papers (1996–2004), including the interpretation of ZF and Kelley–Morse in GPK⁺∞ (1997) and the inconsistency of choice with it (2000).
Presburger Arithmetic⤓ .md 2026-10-22T090557.000 000000000042360 Mojżesz Presburger, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt", presented at the First Congress of Mathematicians of Slavic Countries (Warsaw 1929, published 1930), written as a student exercise set by Tarski. Fischer and Rabin (1974) proved the doubly exponential lower bound that made the decision procedure a landmark in complexity rather than only in logic.
Primitive Recursive Arithmetic⤓ .md 2026-08-20T062908.000 000000000033296 Thoralf Skolem, "Begründung der elementaren Arithmetik" (1923), giving an arithmetic with no quantifiers at all. Hilbert and Bernays adopted it, and Tait ("Finitism", 1981) argued it is the exact formal counterpart of Hilbert's finitary standpoint — a claim that made PRA the benchmark against which finitistic reducibility is measured.
Relativity Theories⤓ .md 2026-10-22T161354.000 000000000065656 The idea is old — Hilbert's sixth problem asked for the axiomatization of physics, and Reichenbach, Carnap, Gödel, Robb, and Suppes each attempted parts of it. The programme this entry describes is Hajnal Andréka, Judit Madarász, and István Németi's at the Rényi Institute from the late 1990s (On the Logical Structure of Relativity Theories, 2002, 1312 pp.), with Gergely Székely's thesis (2009) supplying the accelerated-observer analysis. Its ancestry runs through Tarski's elementary geometry, and directly: Tarski's 1959 paper appeared in a volume titled The Axiomatic Method, with Special Reference to Geometry and Physics**.
Reverse Mathematics⤓ .md 2026-08-20T013702.000 000000000040456 Friedman initiated reverse mathematics (1970s). Simpson systematized (1999). Studies which axioms are needed to prove theorems. Five main subsystems of second-order arithmetic. Calibrates logical strength of ordinary mathematics.
Revision Theory of Truth⤓ .md 2026-10-22T165042.936 000000000000792 Anil Gupta, "Truth and paradox" (1982), and Hans Herzberger, "Notes on naive semantics" (1982), independently; systematized by Gupta and Belnap, The Revision Theory of Truth (1993). The semantic alternative to Kripke's fixed points: where Kripke stops when the extension of T stabilizes, revision keeps going and reads the pattern.
Robinson Arithmetic⤓ .md 2026-08-20T062948.000 000000000037808 Raphael Robinson, "An essentially undecidable axiom system" (1950); Tarski, Mostowski, and Robinson, Undecidable Theories (1953), where Q and R are isolated together as base theories and Q became the standard instrument. Built for one purpose: a finitely axiomatized arithmetic still strong enough for Gödel's argument, so that undecidability could be proved for anything interpreting it.
Second-Order Arithmetic⤓ .md 2026-07-15T232136.000 000000000028672 Hilbert and Bernays formalized analysis in a two-sorted arithmetic (Grundlagen der Mathematik II, 1939). Its subsystems were mapped by Friedman (1970s) and systematized by Simpson (Subsystems of Second Order Arithmetic, 1999). Z₂ is the setting in which reverse mathematics is conducted, and the reason that programme has a fixed scale to measure against.
Set Theory⤓ .md 2026-08-20T061943.000 000000000046896 Georg Cantor created set theory (1874-1897), introducing infinite cardinals and ordinals. Paradoxes (Russell 1901, Burali-Forti 1897) required axiomatization. Ernst Zermelo (1908) and Abraham Fraenkel (1922) developed ZF. John von Neumann added the axiom of regularity. ZFC (ZF + Axiom of Choice) became the standard foundation for mathematics.
Skolem Arithmetic⤓ .md 2026-10-22T090040.000 000000000037016 Thoralf Skolem, "Über einige Satzfunktionen in der Arithmetik" (1930), claiming decidability for multiplication alone; the first complete proof is Mostowski's "On direct products of theories" (1952), and Feferman and Vaught (1959) generalized the method to arbitrary direct products. The result is the mirror of Presburger's, and the pair is the point.
Subsystems of Second-Order Arithmetic⤓ .md 2026-08-20T013702.000 000000000040456 Friedman initiated reverse mathematics (1970s). Simpson systematized (1999). Studies which axioms are needed to prove theorems. Five main subsystems of second-order arithmetic. Calibrates logical strength of ordinary mathematics.
Tarski-Grothendieck Set Theory⤓ .md 2026-10-22T092426.000 000000000049912 Alfred Tarski, "Über unerreichbare Kardinalzahlen" (Fundamenta Mathematicae 30, 1938) and "On well-ordered subsets of any set" (Fund. Math. 32, 1939), where the axiom now called Tarski's axiom A appears — a closure condition on sets, formulated for the theory of inaccessible cardinals rather than for foundations. Grothendieck introduced universes in the 1960s (SGA 4) to make category theory usable in algebraic geometry without proper-class evasions. The two are the same axiom, and the name records that they were arrived at independently. Trybulec ("Tarski–Grothendieck Set Theory", Journal of Formalized Mathematics, 1989) made it the base of Mizar; Metamath uses it too.
Theory of Concatenation⤓ .md 2026-10-22T092424.000 000000000041504 Quine, "Concatenation as a basis for arithmetic" (JSL 11, 1946), took the syntactic operation as primitive and built arithmetic on it; Tarski formulated the editor axiom. Andrzej Grzegorczyk revived the programme in "Undecidability without arithmetization" (Studia Logica 79, 2005), where TC is introduced and proved undecidable; Grzegorczyk and Zdanowski (2008) proved it essentially undecidable. Švejdar (2009), Ganea (2009), and Visser independently settled the open question left there: TC and Q are mutually interpretable.
Theory R⤓ .md 2026-10-22T092421.000 000000000055600 Tarski, Mostowski, and Robinson, Undecidable Theories (1953), chapter 2, where R and Q are isolated together as the two minimal base theories for metamathematical arguments. R was the weaker half and was long treated as Q's shadow; Visser's "Why the theory R is special" (in Foundational Adventures, 2012) is where its interpretability class was explained. Cobham proved a minimality result for R (reported in Jones–Shepherdson 1983); Pakhomov, Murwanashyaka, and Visser (2022) settled the question R poses.
True Arithmetic⤓ .md 2026-08-20T063028.000 000000000042616 The object is implicit in Gödel (1931) — the set of true sentences is what PA fails to exhaust — and made explicit by Tarski's undefinability theorem (1933, published 1936), which shows the set is not arithmetically definable. Its recursion-theoretic location, degree 0^(ω), follows from the Kleene arithmetical hierarchy and Post's theorem.
Zermelo Set Theory⤓ .md Set Theory.md 000000000000104 Georg Cantor created set theory (1874-1897), introducing infinite cardinals and ordinals. Paradoxes (Russell 1901, Burali-Forti 1897) required axiomatization. Ernst Zermelo (1908) and Abraham Fraenkel (1922) developed ZF. John von Neumann added the axiom of regularity. ZFC (ZF + Axiom of Choice) became the standard foundation for mathematics.
CRITERIA⤓ .txt 2026-07-16T150018.000 000000000014352 Not sufficient: Having axioms, since every system in the collection has them. This division is for systems whose individuation is the signature and the axioms, with the logic taken as given. If the entry changes what follows from what — the variety, the accessibility relation, the structural rules, the typing judgment, the object of evaluation — it belongs in the apparatus division that names the change, not here.