README⤓ .txt 2026-10-22T165042.936 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-10-22T092930.000 000000000039808 Blok and Pigozzi (1989). Classify logics by algebraic behavior. Leibniz operator. Protoalgebraic to algebraizable hierarchy. Foundation for metalogical classification.
Abstract Elementary Classes⤓ .md 2026-10-22T180154.561 000000000000960 Saharon Shelah, "Classification of nonelementary classes II: Abstract elementary classes" (in Classification Theory, Chicago 1985, Lecture Notes in Mathematics 1292, 1987), distilled the working assumptions of his earlier work on L_{ω₁,ω} into a short list of axioms on a class of structures and a strong-substructure relation. The aim was a classification theory — stability, categoricity, independence — for classes that compactness does not reach. Shelah's two-volume Classification Theory for Abstract Elementary Classes (2009) is the reference statement of the programme.
Abstract Model Theory⤓ .md 2026-08-20T010655.000 000000000038680 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.
Admissible Sets⤓ .md 2026-10-22T165042.936 000000000000864 Saul Kripke ("Transfinite recursions on admissible ordinals, I and II", abstracts, Journal of Symbolic Logic 29, 1964) and Richard Platek ("Foundations of Recursion Theory", dissertation, Stanford 1966) independently isolated the set theory KP whose transitive models are the admissible sets, to generalize computability from ω to the ordinals — see Kripke–Platek Set Theory. Jon Barwise joined admissibility to infinitary logic after reading Platek's thesis and Lopez-Escobar's Berkeley thesis on infinitary logic: his own dissertation "Infinitary Logic and Admissible Sets" (Stanford 1967, under Solomon Feferman), the paper of the same title (Journal of Symbolic Logic 34, 1969, 226–252), and the monograph Admissible Sets and Structures (Perspectives in Mathematical Logic, Springer 1975) that fixed the subject. Keisler and Knight's survey (Bulletin of Symbolic Logic 10, 2004, 4–26) is the retrospective.
Alternative Semantics⤓ .md 2026-08-20T014720.000 000000000039928 Hamblin (1973), Rooth (1985). Sets of alternatives. Questions as alternative sets. Focus interpretation. Foundation of question semantics.
Automatic Structures⤓ .md 2026-10-22T180154.561 000000000000904 Bernard R. Hodgson, "Décidabilité par automate fini" (Annales des sciences mathématiques du Québec 7, 1983, 39–57), developing his thesis "Théories décidables par automate fini" (Université de Montréal, 1976), defined structures whose relations are recognized by finite automata and proved their first-order theories decidable; the work went unnoticed through the 1980s. Bakhadyr Khoussainov and Anil Nerode, "Automatic presentations of structures" (Logic and Computational Complexity workshop, Indianapolis 1994; LNCS 960, 1995, 367–392), rediscovered the notion and began the systematic theory. Achim Blumensath and Erich Grädel, "Automatic structures" (LICS 2000, 51–62), the third independent formalization, added the ω-automatic case, the characterization by first-order interpretations, and the non-automaticity of Skolem arithmetic and the divisibility order.
Bishop-Style Constructive⤓ .md 2026-10-22T092707.000 000000000051848 Errett Bishop, Foundations of Constructive Analysis (McGraw-Hill, 1967), rebuilt measure theory, Banach space theory, and complex analysis without excluded middle, answering the standing objection that constructive mathematics could not carry ordinary analysis. The revised edition, Bishop and Bridges, Constructive Analysis (Grundlehren 279, Springer, 1985), is the standard reference. Unlike Brouwer, Bishop imposed no philosophy of the continuum and added no principle that classical mathematics rejects.
Buchi Automata⤓ .md 2026-10-22T180154.561 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-10-22T165042.936 000000000000872 Brouwer (1920s). Intuitionist foundations. Sequences created by free choice. Not predetermined. Foundation for Brouwerian analysis.
Compactness⤓ .md 2026-08-20T013347.000 000000000033960 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-08-20T014437.000 000000000038864 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-10-22T180154.561 000000000000928 Chang and Keisler, Continuous Model Theory (1966), gave a first many-valued framework that saw little use. The working version is Henson's logic of positive bounded formulas with approximate satisfaction, developed with Iovino for Banach space structures, and its reformulation by Ben Yaacov, Berenstein, Henson, and Usvyatsov in "Model theory for metric structures" (LMS Lecture Notes 350, 2008), which is the standard reference. Ben Yaacov and Usvyatsov, "Continuous first order logic and local stability" (Transactions of the AMS, 2010), carried stability theory across.
Counting Logic⤓ .md 2026-10-22T165042.936 000000000000856 Neil Immerman and Eric Lander, "Describing graphs: a first-order approach to graph canonization" (in Complexity Theory Retrospective, 1990), introduced the fragments C^k — k variables plus counting quantifiers — as a logical measure of how hard a graph is to identify, and matched them to the Weisfeiler–Leman refinement algorithm. Martin Otto's Bounded Variable Logics and Counting (Lecture Notes in Logic 9, 1997) is the systematic treatment.
Craig Interpolation⤓ .md 2026-08-20T015730.000 000000000042624 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-10-22T090936.000 000000000041312 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-10-22T085910.000 000000000052800 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-08-20T022144.000 000000000052960 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-08-20T022605.000 000000000039352 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-10-22T085913.000 000000000054304 Hans Kamp, "A theory of truth and semantic representation" (in Groenendijk, Janssen, and Stokhof, eds., Formal Methods in the Study of Language, 1981), introduced discourse referents and DRS boxes to handle cross-sentential anaphora and donkey sentences, which static Montague semantics cannot bind. Irene Heim's dissertation The Semantics of Definite and Indefinite Noun Phrases (UMass, 1982) reached an equivalent system, File Change Semantics, independently. Kamp and Reyle, From Discourse to Logic (Kluwer, 1993), is the standard reference.
Dunn Semantics⤓ .md 2026-08-20T023700.000 000000000037224 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-10-22T085918.000 000000000059072 Irene Heim's File Change Semantics (dissertation, UMass 1982; "On the projection problem for presuppositions", 1983) and Hans Kamp's DRT independently made meaning a context-change operation. Groenendijk and Stokhof, "Dynamic Predicate Logic" (Linguistics and Philosophy 14, 1991), gave the compositional, representation-free version in which formulas denote relations between assignments. Veltman, "Defaults in update semantics" (Journal of Philosophical Logic 25, 1996), extended the idea to epistemic modality with states as sets of possibilities and might as a test. Stalnaker's (1978) common ground is the pragmatic ancestor.
Ehrenfeucht-Fraisse Games⤓ .md 2026-08-20T025129.000 000000000041592 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-10-22T085856.000 000000000043664 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-08-20T030450.000 000000000039304 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-10-22T085920.000 000000000062112 Donald Davidson, "The Logical Form of Action Sentences" (in Rescher, ed., The Logic of Decision and Action, University of Pittsburgh Press, 1967), argued that action sentences quantify over events, so that adverbial modification is conjunction and adverb-drop inferences become logical rather than lexical. Castañeda, commenting on that paper in the same volume (1967), proposed the neo-Davidsonian variant in which every participant is severed into its own role conjunct. Terence Parsons, Events in the Semantics of English: A Study in Subatomic Semantics (MIT Press, 1990), developed it; Angelika Kratzer, "Severing the External Argument from its Verb" (1996), gave it a syntactic basis. Vendler (1957) and Dowty (1979) supplied the aspectual classes; Bach, "The Algebra of Events" (Linguistics and Philosophy 9, 1986), the mereology.
Feferman-Vaught Theorem⤓ .md 2026-10-22T090836.000 000000000072560 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-08-20T033231.000 000000000053672 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-10-22T085853.000 000000000042200 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-10-22T085923.000 000000000045824 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-08-20T040616.000 000000000045760 Cohen (1963). Proved the independence of the Continuum Hypothesis from ZFC and of the Axiom of Choice from ZF. The two base theories are different and must be kept apart: AC is one of ZFC's own axioms, so it cannot be independent of ZFC; the choiceless theory ZF is what Cohen's symmetric-submodel argument works over. CH is independent of ZFC proper. A general method for building models of set theory with prescribed properties.
Fraisse Limits⤓ .md 2026-08-20T041354.000 000000000043472 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-10-22T180154.561 000000000000888 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-10-22T090015.000 000000000037568 Mary Dalrymple, John Lamping and Vijay Saraswat, "LFG Semantics via Constraints" (EACL 1993); Fernando Pereira joined the group for "Linear Logic for Meaning Assembly" (1995), which is where the linear-logic formulation is set out in full. LFG interface. Resource-sensitive composition. Foundation of LFG semantics.
Godel Completeness Theorem⤓ .md 2026-08-20T044814.000 000000000040176 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-10-22T165042.936 000000000000872 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-08-20T051228.000 000000000062448 Jacques Herbrand, Recherches sur la théorie de la démonstration (thesis, Paris, 1930), where the fundamental theorem appears — a year before his death at twenty-three. Skolem (1920, 1928) had supplied the normal-form machinery, and the result is often called the Skolem–Herbrand–Gödel theorem. Herbrand's own proof contained an error, located and repaired by Dreben, Andrews, and Aanderaa (1963). Robinson (1965) turned the theorem into an algorithm with unification and resolution; van Emden and Kowalski (1976) made the least Herbrand model the declarative semantics of logic programming.
Institutions⤓ .md 2026-10-22T165042.936 000000000000840 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.
Interpretations Between Theories⤓ .md 2026-10-22T180154.561 000000000001000 Alfred Tarski, Andrzej Mostowski, and Raphael Robinson, Undecidable Theories (North-Holland, 1953), made relative interpretation a method: translate one theory's language into another's, relativize the quantifiers to a definable domain, and demand that theorems translate to theorems. Solomon Feferman, "Arithmetization of metamathematics in a general setting" (Fundamenta Mathematicae 49, 1960), proved the interpretability of inconsistency. Steven Orey, "Relative interpretations" (Zeitschrift für mathematische Logik 7, 1961), and Petr Hájek, "On interpretability in set theories I–II" (Commentationes Mathematicae Universitatis Carolinae, 1971–72), characterized interpretability over reflexive theories. Per Lindström, "Some results on interpretability" (Proceedings of the 5th Scandinavian Logic Symposium, 1979), developed the degree structure over PA; Jan Mycielski, Pavel Pudlák, and Alan Stern, A Lattice of Chapters of Mathematics (Memoirs of the AMS 426, 1990), organized the degrees into a lattice; Albert Visser, "Categories of theories and interpretations" (in Logic in Tehran, Lecture Notes in Logic 26, 2006), gave the categorical formulation.
Kripke Fixed Point⤓ .md 2026-10-22T085853.000 000000000042552 Kripke (1975). Truth predicate treatment. Self-reference via fixed points. Grounded truth. Foundation for semantic paradoxes.
Large Cardinals⤓ .md 2026-10-22T085118.000 000000000042472 Hausdorff described weakly inaccessible cardinals (1908); Mahlo added his hierarchy (1911); Ulam 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-10-22T180154.561 000000000000880 Per Lindström, "On extensions of elementary logic", Theoria 35 (1969), 1–11. The abstract-logic framework descends from Mostowski's generalized quantifiers and Barwise's abstract model theory; Barwise and Feferman's Model-Theoretic Logics (1985) is the standard collection. The theorem settles the question the generalized quantifiers had opened — whether a richer logic could keep first-order logic's metatheoretic properties. It cannot.
Logical Matrix⤓ .md 2026-10-22T085300.000 000000000046952 Ł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-10-22T085118.000 000000000040024 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-08-20T010738.000 000000000047456 Richard Montague, "English as a Formal Language" (1970), "Universal Grammar" (1970), and "The Proper Treatment of Quantification in Ordinary English" (PTQ, 1973) — three papers, the last published after his death in 1971. The thesis of the first is that there is no theoretically important difference between natural and formal languages, and that English can be given a model-theoretic semantics by the same means as a logistic system. Barbara Partee brought the programme into linguistics; Dowty, Wall, and Peters, Introduction to Montague Semantics (1981), is the standard textbook; Gallin, Intensional and Higher-Order Modal Logic (1975), gave the metatheory.
Morley Categoricity Theorem⤓ .md 2026-08-20T011006.000 000000000040168 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-08-20T011357.000 000000000034096 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-10-22T165042.936 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-08-20T012210.000 000000000037344 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-08-20T110640.000 000000000043696 The method predates its name: Löwenheim (1915) and Skolem used elimination for the calculus of relatives, Langford (1927) for dense linear orders, Presburger (1929) for the additive integers. Tarski turned it into a general technique and applied it to real closed fields in work of the early 1930s, published as A Decision Method for Elementary Algebra and Geometry (1948, revised 1951). Remove quantifiers from formulas. Quantifier-free equivalents. Decidability. Foundation for effective model theory.
Rabin Tree Theorem⤓ .md 2026-10-22T180154.561 000000000000816 Michael O. Rabin, "Decidability of second-order theories and automata on infinite trees" (announced Bulletin of the AMS 1968; full proof Transactions of the AMS 141, 1969, 1–35): S2S, the monadic second-order theory of the infinite binary tree, is decidable. The proof invented automata on infinite trees, and its hardest step was the complementation lemma, which Rabin proved by transfinite induction. Yuri Gurevich and Leo Harrington, "Trees, automata, and games" (STOC 1982), reproved the lemma by the forgetful determinacy of infinite games; Andrey Muchnik gave a proof avoiding transfinite induction (published in Russian in 1984, circulated through Alexei Semenov's lectures, written out in full by Igor Walukiewicz); E. Allen Emerson and Charanjit Jutla, "Tree automata, mu-calculus and determinacy" (FOCS 1991), recast it through parity acceptance and memoryless determinacy, the form the field now uses.
Real Closed Fields⤓ .md 2026-07-16T165328.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-10-22T092654.000 000000000061896 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-10-22T085857.000 000000000037984 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-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 000000000000816 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-08-20T014005.000 000000000047352 Jónsson (1956, 1960) built homogeneous universal structures in the algebraic setting, generalizing Hausdorff's η_α orders. Morley and Vaught, "Homogeneous universal models" (Mathematica Scandinavica, 1962), transposed the construction to elementary classes and proved the uniqueness theorem that makes saturation usable; Keisler's contemporaneous work on ultrapowers supplied the standard existence method. Chang and Keisler, Model Theory (1973), consolidated the subject, including the special models that stand in where saturated ones fail to exist.
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.
Segmented Discourse Representation Theory⤓ .md 2026-10-22T180154.561 000000000001064 Nicholas Asher, Reference to Abstract Objects in Discourse (Kluwer, 1993), extended DRT with rhetorical relations over labelled segments to handle anaphoric reference to propositions and eventualities, which DRT's accessibility both over- and under-generates. Lascarides and Asher, "Temporal Interpretation, Discourse Relations and Commonsense Entailment" (Linguistics and Philosophy 16, 1993, 437–493), supplied the defeasible inference of the relations and their temporal effects. Asher and Lascarides, Logics of Conversation (Cambridge University Press, 2003), is the standard formulation. The glue logic's conditional comes from Asher and Morreau, "Commonsense Entailment: A Modal Theory of Non-monotonic Reasoning" (IJCAI 1991, 387–392); the right frontier constraint is Livia Polanyi's (1985, 1988), proposed for pronouns and generalized by SDRT to all anaphora and all attachment.
Sheaf Semantics⤓ .md 2026-10-22T090413.000 000000000053960 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-10-22T180154.561 000000000000888 Jon Barwise and John Perry, Situations and Attitudes (MIT Press, 1983), following Barwise's "Scenes and other situations" (1981). The driving argument was linguistic: naked-infinitive perception reports — "Ralph saw Mary run" — permit substitution of coreferring terms and support existential generalization, yet fail to be closed under logical equivalence, which no possible-worlds semantics can deliver. Keith Devlin, Logic and Information (1991), gave the infon algebra; Barwise and Etchemendy, The Liar (1987), applied the framework to semantic paradox using Aczel's anti-foundation axiom; Barwise and Seligman, Information Flow (1997), developed the constraint machinery into channel theory.
Stability Theory⤓ .md 2026-08-20T021538.000 000000000044232 Shelah (1970s). Classification of first-order theories. Stable theories: well-behaved model theory. Counting types. Foundation for modern model theory.
Tarski Undefinability⤓ .md 2026-08-20T015622.000 000000000032104 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-08-20T015843.000 000000000032912 Tarski (1933). Model-theoretic truth definition. Recursive satisfaction. Convention T. Foundation for formal semantics.
Team Semantics⤓ .md 2026-10-22T085858.000 000000000037416 Hodges (1997), Väänänen (2007). Dependence logic. Sets of assignments. Independence-friendly logic semantics. Foundation for dependence concepts.
Truthmaker Semantics⤓ .md 2026-08-20T020402.000 000000000034896 Fine (2010s). Exact verification. States as truthmakers. Hyperintensional. Foundation of exact semantics.
Ultraproducts⤓ .md 2026-08-20T020512.000 000000000033520 Ł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-08-20T061741.000 000000000046784 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-10-22T165042.936 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).