README⤓ .txt 2026-07-17T121634.146 000000000000800 The metatheory of the satisfaction relation: results and techniques about the models of a logic, their construction, classification, and the definability of properties within them. Where an entry elsewhere in the collection defines a logic, an entry here proves something about the class of structures a logic can describe.
Abstract Algebraic Logic⤓ .md 2026-07-15T071850.000 000000000016616 Blok and Pigozzi (1989). Classify logics by algebraic behavior. Leibniz operator. Protoalgebraic to algebraizable hierarchy. Foundation for metalogical classification.
Abstract Model Theory⤓ .md 2026-07-15T062347.000 000000000019160 Lindström's theorem (1969): FOL is maximal compact logic with Löwenheim-Skolem. Barwise, Feferman: "Model-theoretic logics" (1985). Studies logics abstractly via their properties. Characterization theorems for logics. Meta-study of logics.
Alternative Semantics⤓ .md 2026-07-17T120407.600 000000000000904 Hamblin (1973), Rooth (1985). Sets of alternatives. Questions as alternative sets. Focus interpretation. Foundation of question semantics.
Bishop-Style Constructive⤓ .md 2026-07-17T120407.600 000000000000944 Errett Bishop (1967). Foundations of Constructive Analysis. Minimal philosophy. Compatible with classical. Foundation of constructive analysis.
Buchi Automata⤓ .md 2026-07-17T120407.600 000000000000872 J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.
Choice Sequences⤓ .md 2026-07-15T072104.000 000000000014776 Brouwer (1920s). Intuitionist foundations. Sequences created by free choice. Not predetermined. Foundation for Brouwerian analysis.
Compactness⤓ .md 2026-07-15T064856.000 000000000015392 Gödel completeness theorem (1929) implies compactness. Fundamental model-theoretic property. If every finite subset satisfiable, whole set satisfiable. Fails for many extensions.
Constructible Universe⤓ .md 2026-07-17T120407.600 000000000000920 Gödel (1938). The inner model L, built by iterating first-order definability. Established the consistency of the Axiom of Choice and the Generalized Continuum Hypothesis with ZF.
Continuous Model Theory⤓ .md 2026-07-17T120407.600 000000000000928 Ben Yaacov, Berenstein, Henson (2000s). Metric structures. [0,1]-valued logic. Approximate satisfaction. Analysis meets model theory.
Counting Logic⤓ .md 2026-07-17T120407.600 000000000000856 Immerman, Lander (1990), various. Counting quantifiers. Cardinality comparison. Extends first-order. Foundation of descriptive complexity.
Craig Interpolation⤓ .md 2026-07-15T064854.000 000000000014776 William Craig (1957). If A ⊨ B, there exists interpolant C. C uses only shared vocabulary. Fundamental theorem linking syntax and semantics. Applications across logic.
Cylindric Algebras⤓ .md 2026-07-15T060042.000 000000000021752 Tarski with Henkin and Monk developed cylindric algebras (1950s-70s). Algebraic approach to first-order logic. Cylindrifications model existential quantification. Diagonal elements model equality. Part of algebraic logic tradition alongside relation algebras.
Degree Semantics⤓ .md 2026-07-15T235628.000 000000000014560 Cresswell, "The semantics of degree" (1976); von Stechow (1984) on comparatives; Kennedy's Projecting the Adjective (1997, published 1999) and his work with McNally (2005); Heim (2000) on degree operators and scope. Gradable adjectives. Degree arguments. Scales and measure functions. Foundation of scalar semantics.
Dense Linear Orders⤓ .md 2026-07-16T165328.000 000000000041552 Cantor (1895) proved that any two countable dense linear orders without endpoints are isomorphic — the back-and-forth argument, and the first categoricity theorem in mathematics. Langford (1927) gave the quantifier elimination and the decision procedure, making DLO the first nontrivial theory shown complete and decidable, two years before Presburger's arithmetic.
Descriptive Complexity⤓ .md 2026-07-17T120407.600 000000000000920 Fagin (1974), Immerman, Vardi (1982). Characterizes computational complexity classes by logical expressiveness over finite structures. Companion to Finite Model Theory, focused on the capture program.
Discourse Representation Theory⤓ .md 2026-07-17T120407.600 000000000000984 Hans Kamp (1981). Discourse referents. DRS structures. Anaphora and scope. Foundation of computational semantics.
Dunn Semantics⤓ .md 2026-07-15T064537.000 000000000015592 J. Michael Dunn (1966, 1976). Generalized semantics via sets of values. Valuations assign {t}, {f}, {t,f}, or {} to formulas. Relational semantics for relevance logic. Foundation for Belnap's four-valued logic.
Dynamic Semantics⤓ .md 2026-07-17T120407.600 000000000000880 Groenendijk, Stokhof, Veltman (1980s-90s). Meaning as context change. Anaphora resolution. Information update. Foundation of discourse semantics.
Ehrenfeucht-Fraisse Games⤓ .md 2026-07-15T065144.000 000000000015216 Ehrenfeucht (1961) building on Fraïssé (1954). Game characterization of elementary equivalence. Spoiler vs Duplicator. n-round game captures n-quantifier equivalence.
Elementary Embeddings⤓ .md 2026-07-15T235628.000 000000000016864 Tarski and Vaught, "Arithmetical extensions of relational systems" (1957), which introduced elementary substructures and the Tarski–Vaught test; Robinson's model-completeness and diagram method (1956); Frayne, Morel, and Scott (1962) for ultrapower embeddings. Structure preservation. Elementary equivalence. Chains and limits. Foundation of model-theoretic algebra.
Elementary Equivalence⤓ .md 2026-07-15T235628.000 000000000016072 Tarski's notion of arithmetical equivalence (1936) and its development with Vaught (1957); Fraïssé's back-and-forth characterization (1954) and Ehrenfeucht's game formulation (1961), which made the relation checkable. Same first-order theory. Indistinguishable by FOL. Ehrenfeucht-Fraïssé games. Foundation for model comparison.
Event Semantics⤓ .md 2026-07-17T120407.600 000000000000864 Davidson (1967), Parsons, Kratzer. Events as arguments. Thematic roles. Modification explained. Foundation of neo-Davidsonian semantics.
Feferman-Vaught Theorem⤓ .md 2026-07-17T120407.600 000000000000920 Solomon Feferman and Robert Vaught, "The first order properties of products of algebraic systems" (Fundamenta Mathematicae 47, 1959), generalizing Mostowski's "On direct products of theories" (JSL 17, 1952), which had proved the case Skolem arithmetic needs. Läuchli, Shelah, and Gurevich extended the method to monadic second-order logic, where it is called the composition method. Makowsky's "Algorithmic uses of the Feferman–Vaught theorem" (APAL 126, 2004) is the survey and the argument for its computational reading.
Finite Model Theory⤓ .md 2026-07-15T061331.000 000000000020840 Emerged from Trakhtenbrot (1950): validity over finite models undecidable. Fagin (1974): NP = existential second-order. Immerman, Vardi: descriptive complexity (1980s). Studies logic over finite structures. Connections to complexity theory and databases.
Finite Variable Logic⤓ .md 2026-07-15T235628.000 000000000016512 Barwise (1977) on infinitary logic with finitely many variables; Immerman (1982) on relational queries and the FO^k hierarchy; Poizat (1982) on deux ou trois variables; Kolaitis and Vardi (1990s) for the pebble-game analysis; Cai, Fürer, and Immerman (1992) for the counting-logic separation. Bounded variables. Expressiveness hierarchy. Pebble games. Foundation of finite model theory.
Fixed-Point Logic⤓ .md 2026-07-15T060052.000 000000000020680 Fixed-point extensions of first-order logic emerged in 1970s-80s. LFP (least fixed point) and IFP (inflationary fixed point) capture P on ordered structures (Immerman, Vardi). Connects logic and complexity theory. Foundation for descriptive complexity.
Forcing⤓ .md 2026-07-17T120407.600 000000000000800 Cohen (1963). Proved the independence of the Continuum Hypothesis and the Axiom of Choice from ZFC. A general method for building models of set theory with prescribed properties.
Fraisse Limits⤓ .md 2026-07-17T120407.600 000000000000856 Roland Fraïssé (1953, 1954), with roots in Cantor's back-and-forth argument. A construction building a canonical countable homogeneous structure from a class of finite structures, and the model-theoretic analysis of ultrahomogeneity via amalgamation.
Full Lambek Calculus⤓ .md 2026-07-15T235854.000 000000000035992 Lambek's syntactic calculus (1958) supplies the residuated core; the additives and constants were added and the family systematized by Ono and Komori (1985) and Ono (1993, 2003). Galatos, Jipsen, Kowalski, and Ono, Residuated Lattices: An Algebraic Glimpse at Substructural Logics (2007), is the standard reference and the reason FL is the base of the field rather than one system in it.
Glue Semantics⤓ .md 2026-07-17T120407.600 000000000000856 Dalrymple, Lamping, Saul (1993). LFG interface. Linear logic for meaning assembly. Resource-sensitive composition. Foundation of LFG semantics.
Godel Completeness Theorem⤓ .md 2026-07-17T120407.600 000000000000952 Gödel (1929 dissertation, 1930). First-order semantic consequence coincides with formal derivability. The foundational adequacy result for first-order logic — distinct from his incompleteness theorems.
Henkin Semantics⤓ .md 2026-07-15T063635.000 000000000017896 Henkin introduced general models for higher-order logic (1950). Alternative to standard semantics. Function spaces need not be full. Completeness theorem holds (unlike standard semantics). Foundation for much of higher-order logic.
Herbrand Semantics⤓ .md 2026-07-15T073536.000 000000000014592 Herbrand (1930). Term models. Syntactic interpretation. Herbrand universe. Foundation for logic programming.
Institutions⤓ .md 2026-07-15T063120.000 000000000018648 Goguen and Burstall introduced institutions (1984, 1992). Category-theoretic framework for abstract model theory. Formalizes "what is a logic?" Signature, sentences, models, satisfaction. Foundation for heterogeneous specification.
Kripke Fixed Point⤓ .md 2026-07-15T074643.000 000000000014248 Kripke (1975). Truth predicate treatment. Self-reference via fixed points. Grounded truth. Foundation for semantic paradoxes.
Large Cardinals⤓ .md 2026-07-15T225705.000 000000000029376 Hausdorff described weakly inaccessible cardinals (1908); Mahlo added his hierarchy (1911); Ulam and Tarski introduced measurables (1930). Scott (1961) proved that a measurable cardinal implies V ≠ L, which turned the subject from curiosity into method. Solovay, Martin, Woodin, and Magidor built the modern hierarchy and its connection to determinacy.
Lindstrom Theorem⤓ .md 2026-07-15T072259.000 000000000013768 Lindström (1969). First-order logic is maximal. Has compactness and Löwenheim-Skolem. Any extension loses one. Characterization theorem.
Logical Matrix⤓ .md 2026-07-17T120407.600 000000000000856 Łukasiewicz and Tarski, "Investigations into the sentential calculus" (1930), where the matrix method is set out; Jerzy Łoś and Roman Suszko, "Remarks on sentential logics" (1958), which gave the general theory and the notion of a structural consequence relation. Wójcicki's Theory of Logical Calculi (1988) is the reference; Font and Jansana's abstract algebraic logic is where it now lives.
Lowenheim-Skolem⤓ .md 2026-07-17T120407.600 000000000000872 Löwenheim (1915), Skolem (1920). Countable models exist for satisfiable first-order theories. Upward version: arbitrarily large models. Paradox: set theory has countable models.
Montague Grammar⤓ .md 2026-07-17T120407.600 000000000000872 Richard Montague (1970). "English as a formal language." Intensional logic for natural language. Compositionality. Foundation of formal semantics.
Morley Categoricity Theorem⤓ .md 2026-07-17T120407.600 000000000000960 Michael Morley (1965), "Categoricity in Power," answering Łoś's conjecture. The theorem that launched modern classification (stability) theory: for a countable theory, categoricity at one uncountable cardinal forces categoricity at every uncountable cardinal.
O-Minimality⤓ .md 2026-07-15T071629.000 000000000014512 van den Dries, Knight, Pillay, Steinhorn (1986). Tame geometry over the reals. Definable sets are finite unions of intervals. No pathological sets. Foundation for real algebraic geometry.
Omega-Logic⤓ .md 2026-07-17T120407.600 000000000000832 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.
Omitting Types Theorem⤓ .md 2026-07-17T120407.600 000000000000920 Independently by Henkin, Orey, and Grzegorczyk–Mostowski–Ryll-Nardzewski in the 1950s. A foundational construction theorem of classical model theory: a countable theory has a countable model omitting any given non-principal (non-isolated) type. The constructive complement to realizing types.
Quantifier Elimination⤓ .md 2026-07-15T074903.000 000000000013736 Tarski (1951). Remove quantifiers from formulas. Quantifier-free equivalents. Decidability. Foundation for effective model theory.
Real Closed Fields⤓ .md 2026-07-16T145838.000 000000000049512 Artin and Schreier (1927) gave the algebraic theory of real closed fields and used it to solve Hilbert's seventeenth problem. Tarski proved quantifier elimination, completeness, and decidability for the ordered field of reals — work of the early 1930s, delayed by the war, published as A Decision Method for Elementary Algebra and Geometry (1948, revised 1951). Collins (1975) gave cylindrical algebraic decomposition, the first implementable procedure. Van den Dries, Pillay, and Steinhorn founded o-minimality (1980s) with RCF as the motivating case.
Realizability⤓ .md 2026-07-15T055807.000 000000000022232 Kleene introduced realizability (1945) to interpret intuitionistic logic via computable functions. A formula is true if "realized" by a computation. Connects constructive logic to computability theory. Extended by Kreisel, Troelstra, and others. Foundation for program extraction from proofs.
Relation Algebra⤓ .md 2026-07-15T061316.000 000000000019360 De Morgan, Peirce, and Schröder developed algebra of relations (1860s-1890s). Tarski axiomatized relation algebras (1941). Algebraic approach to binary relations. Equivalent to three-variable first-order logic. Foundation for database theory and program semantics.
Reverse Mathematics⤓ .md 2026-07-15T063452.000 000000000019184 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-07-17T120407.600 000000000000936 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.
Saturated Models⤓ .md 2026-07-15T074908.000 000000000013944 Morley, Vaught (1950s-60s). Realize all types. Universal homogeneity. Rich structures. Foundation for stability theory.
Second-Order Arithmetic⤓ .md 2026-07-17T120407.600 000000000000928 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.
Sheaf Semantics⤓ .md 2026-07-17T121634.146 000000000000856 Grothendieck's sites and sheaves (SGA4, 1963–64, published 1972) supplied the machinery; Lawvere and Tierney's elementary topos (1970) made it logic. Kripke–Joyal forcing is Joyal's reformulation of Kripke's semantics inside a topos; Fourman and Scott, "Sheaves and logic" (1979), and Fourman and Hyland's sheaf models of intuitionistic analysis (1979) are where the model theory was built. Van Dalen and Troelstra's Constructivism in Mathematics (1988) is the standard exposition.
Situation Semantics⤓ .md 2026-07-17T120407.600 000000000000840 Barwise, Perry (1983). Situations vs possible worlds. Partial information. Constraints and infons. Foundation of situated cognition.
Stability Theory⤓ .md 2026-07-15T071119.000 000000000014936 Shelah (1970s). Classification of first-order theories. Stable theories: well-behaved model theory. Counting types. Foundation for modern model theory.
Tarski Undefinability⤓ .md 2026-07-17T120407.600 000000000000912 Tarski (1933, 1936). Arithmetical truth is not arithmetically definable. The semantic counterpart of Gödel incompleteness and the formal resolution of the Liar paradox.
Tarskian Semantics⤓ .md 2026-07-15T073531.000 000000000015296 Tarski (1933). Model-theoretic truth definition. Recursive satisfaction. Convention T. Foundation for formal semantics.
Team Semantics⤓ .md 2026-07-17T120407.600 000000000000856 Hodges (1997), Väänänen (2007). Dependence logic. Sets of assignments. Independence-friendly logic semantics. Foundation for dependence concepts.
Truthmaker Semantics⤓ .md 2026-07-17T120407.600 000000000000848 Fine (2010s). Exact verification. States as truthmakers. Hyperintensional. Foundation of exact semantics.
Ultraproducts⤓ .md 2026-07-15T071122.000 000000000015096 Łoś (1955). Construct new models from families. Ultrafilter averages structures. Łoś's theorem: first-order transfer. Foundation for nonstandard methods.
Zero-One Laws⤓ .md 2026-07-16T001339.000 000000000035424 Glebskii, Kogan, Liogon'kii, and Talanov (1969) in the Soviet literature and Ronald Fagin, "Probabilities on finite models" (Journal of Symbolic Logic, 1976), independently. Compton, Kolaitis, and Vardi extended the subject through the 1980s and 90s; Shelah and Spencer (1988) settled the sparse random-graph case.
CRITERIA⤓ .txt 2026-07-17T121634.146 000000000000816 Not sufficient: A named logic evaluated on teams rather than on assignments (that belongs in Team; the semantics as a technique is cross-listed here). A named logic built on truthmaker or state-based semantics (that belongs in Hyperintensional; the semantics as a technique is cross-listed here). A proof calculus or a result about derivations (Proof-Systems). A category-theoretic semantics (Categorical). A theory of computability or degrees (Computability).