README⤓ .txt 2026-10-22T165042.936 000000000000720 Logics of necessity and possibility and their close relatives, interpreted over Kripke frames or neighborhood models. The operators read as metaphysical, logical, or physical necessity; the systems are individuated by the frame conditions they impose and the axioms those conditions validate.
Adjoint Logic⤓ .md 2026-10-22T180154.561 000000000000744 Nick Benton, "A mixed linear and non-linear logic: proofs, terms and models" (CSL 1994, LNCS 933, 1995), which presented intuitionistic and linear logic as two judgments related by a monoidal adjunction whose round trip is the exponential !; Jason Reed, "A judgmental deconstruction of modal logic" (2009, unpublished manuscript — the title plays on Pfenning and Davies' "A judgmental reconstruction of modal logic"), which derived □ and the lax ○ from adjoint pairs and parametrized the construction over a preorder of modes; Daniel Licata and Michael Shulman, "Adjoint logic with a 2-category of modes" (LFCS 2016), generalizing the adjoint logics of Benton and Wadler (1994, 1996) and Reed (2009) to many adjunctions between the same modes; Licata, Shulman, and Mitchell Riley, "A fibrational framework for substructural and modal logics" (FSCD 2017); Klaas Pruiksma and Frank Pfenning, "A message-passing interpretation of adjoint logic" (PLACES 2019; journal version in JLAMP 120, 2021).
B Modal Logic⤓ .md 2026-10-22T180154.561 000000000000768 Oskar Becker, "Zur Logik der Modalitäten" (Jahrbuch für Philosophie und phänomenologische Forschung 11, 1930), introduced the axiom and its name: he called A → □◇A the Brouwersche Axiom because reading negation as impossibility turns the intuitionistically valid A → ¬¬A into it. The analogy is the whole of the association — Brouwer never worked in modal logic — and Becker's own aim was to cut down the number of non-equivalent modalities. The system — T plus the axiom — is the Brouwersche system of Kripke, "Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi" (1963), which proved it complete for reflexive symmetric frames and decidable; the Lemmon–Scott nomenclature writes it KTB.
Bisimulation Modal Logic⤓ .md 2026-10-22T084838.000 000000000039792 Hennessy and Milner (1980) connected modal logic and bisimulation. Park coined "bisimulation." Modal logic is bisimulation-invariant fragment of FOL (van Benthem). Foundation for process algebra and model theory.
Conditional Logic⤓ .md 2026-08-20T020437.000 000000000042408 C.I. Lewis introduced strict conditional to fix paradoxes of material implication (1912). Robert Stalnaker (1968) and David Lewis (1973) developed possible worlds semantics for counterfactuals. Conditional logic generalizes: "If A were the case, then B" — not just "A materially implies B." Foundation for counterfactual reasoning and causal analysis.
Contingency Logic⤓ .md 2026-10-22T092213.000 000000000033672 Montgomery and Routley (1966). Contingency as primitive. Δφ: φ is contingent. Non-interdefinability with necessity. Foundation for modal analysis.
Counterpart Theory⤓ .md 2026-08-20T015422.000 000000000035624 Lewis (1968). No transworld identity. Counterparts represent de re. Modal realism. Foundation for modal metaphysics.
Discussive Logic⤓ .md 2026-10-22T180154.561 000000000000792 Stanisław Jaśkowski, "Propositional calculus for contradictory deductive systems" (Studia Societatis Scientiarum Torunensis, 1948; English 1969) — the first paraconsistent logic, published the year Priest was born and fifteen years before da Costa. Jaśkowski was answering Łukasiewicz's 1910 challenge to construct a system in which the law of non-contradiction fails without triviality. A second paper (1949) added the discussive conjunction, which the first had done without. Kotas (1974) gave the first axiomatization; da Costa and Dubikajtis (1977) worked it into Jaśkowski's own discussive language.
Dynamic Topological Logic⤓ .md 2026-10-22T224951.000 000000000082224 Two 1997 starting points. Sergei Artemov, Jennifer Davoren, and Anil Nerode, "Modal Logics and Topological Semantics for Hybrid Systems" (Technical Report MSI 97-05, Cornell University, 1997), introduced the bimodal system S4C and proved it finitely axiomatizable, decidable, and with the finite model property; Philip Kremer and Grigori Mints announced the program in the Bulletin of Symbolic Logic 3 (1997) — Kremer and Mints, "Dynamic Topological Logic" (371–372), Kremer, "Temporal Logic over S4: An Axiomatizable Fragment of Dynamic Topological Logic" (375–376), and Kremer, Mints, and Rybakov, "Axiomatizing the Next-Interior Fragment of Dynamic Topological Logic" (376–377). The full paper is Kremer and Mints, "Dynamic Topological Logic" (Annals of Pure and Applied Logic 131, 2005, 133–158), which added the henceforth operator and proposed an axiomatization of the trimodal logic, conjectured complete. The negative results are Boris Konev, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev, "Dynamic Topological Logics over Spaces with Continuous Functions" (Advances in Modal Logic 6, 2006, 299–318) and "On Dynamic Topological and Metric Logics" (Studia Logica 84, 2006, 129–160); the positive ones are David Fernández-Duque's, chiefly "A Sound and Complete Axiomatization for Dynamic Topological Logic" (Journal of Symbolic Logic 77(3), 2012, 947–969) and "Non-Finite Axiomatizability of Dynamic Topological Logic" (ACM Transactions on Computational Logic 15(1), 2014).
First-Order Modal Logic⤓ .md 2026-10-22T085724.000 000000000037568 Carnap, Kripke (1960s). Quantifiers meet modalities. Varying domains. Rigid vs non-rigid designators. Foundation for quantified intensional logic.
Fusion and Products⤓ .md 2026-08-20T033832.000 000000000052424 Fusion (independent join) was studied by Thomason (1980) and Fine and Schurz (1996); the transfer theorems are theirs and Kracht and Wolter's (1991). Products were introduced by Shehtman (1978) and Segerberg (1973), and the subject was systematized in Gabbay, Kurucz, Wolter, and Zakharyaschev, Many-Dimensional Modal Logics (2003). The two constructions look similar and behave completely differently, which is the point.
Goldblatt-Thomason Theorem⤓ .md 2026-10-22T085021.000 000000000038992 Goldblatt and Thomason (1974). Characterizes modally definable frame classes. Frame conditions expressible by modal formulas. Closure under bounded morphic images, generated subframes and disjoint unions — plus reflection of ultrafilter extensions, which runs in the opposite direction from the other three.
Graded Modal Logic⤓ .md 2026-10-22T090714.000 000000000040520 Fine (1972) and Goble (1970) introduced graded modalities. Extends modal logic with counting. ◇≥n φ: "at least n accessible worlds satisfy φ." Useful for cardinality constraints. Applications in description logics and database queries.
Grzegorczyk Logic⤓ .md 2026-10-22T085021.000 000000000035656 Grzegorczyk (1967). Modal companion of intuitionistic logic; the logic of provability-together-with-truth. S4 + Grzegorczyk axiom. No infinite ascending chains. Foundation for provability and intuitionism connection.
Hybrid Logic⤓ .md 2026-10-22T165042.936 000000000000760 Arthur Prior introduced nominals for temporal logic (1967). Modern hybrid logic developed by Patrick Blackburn and colleagues (1990s-2000s). Extends modal logic with explicit reference to worlds/states. Bridges modal and first-order logic while maintaining modal decidability. Useful for temporal databases, spatial reasoning, and description logics.
Impossible Worlds⤓ .md 2026-10-22T180154.561 000000000000800 Routley's non-classical worlds (1980) and Rescher–Brandom (1979); Priest's development (1997, 2005); Nolan's defence of impossible worlds (1997); Berto and Jago's Impossible Worlds (2019) is the standard treatment. Extension of possible worlds. Worlds where contradictions hold. Non-trivial impossible reasoning. Hyperintensional semantics.
Interpretability Logic⤓ .md 2026-08-20T033832.000 000000000040288 Visser (1990s). One theory interprets another. □ for provability, ⊳ for interpretability. IL systems. Foundation for relative consistency.
Jonsson-Tarski Duality⤓ .md 2026-10-22T180154.561 000000000000880 Bjarni Jónsson and Alfred Tarski, "Boolean algebras with operators, Parts I and II" (American Journal of Mathematics, 1951–52) — written before Kripke semantics existed, and containing it. Goldblatt's "Metamathematics of modal logic" (1976) and Thomason's work made the connection explicit; Blackburn, de Rijke, and Venema's Modal Logic (2001) is where the field learned to teach it.
Justification Logic⤓ .md 2026-10-22T092208.000 000000000043656 Sergei Artemov introduced the Logic of Proofs (LP) in 1995, solving a long-standing problem about the intended provability semantics of intuitionistic logic. Extended to justification logic more broadly (2000s). Replaces the box □φ with explicit justifications t:φ ("t is a justification for φ"). Makes evidence explicit where modal logic leaves it implicit.
K Modal Logic⤓ .md 2026-08-20T005813.000 000000000044768 The distribution axiom appears in Gödel, "Eine Interpretation des intuitionistischen Aussagenkalküls" (1933), as one of three axioms for his provability calculus. Kripke, "A Completeness Theorem in Modal Logic" (1959) and "Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi" (1963), supplied the relational semantics and the completeness proof. Lemmon and Scott's notes, circulated from 1966 and published as An Introduction to Modal Logic (1977), fixed the practice of naming systems as K plus a list of axioms. K is the smallest normal modal logic: every normal system extends it.
KB Modal Logic⤓ .md 2026-10-22T090714.000 000000000032784 The B axiom (p → □◇p) was named for Brouwer by Becker (1930), on an analogy with intuitionistic double negation that later commentators judged mistaken; Kripke's symmetric-frame semantics (1963) made KB a system rather than an axiom. KB = K + B. Symmetric frames. Brouwerian axiom. Possibility-necessity link.
Lewis Systems⤓ .md 2026-10-22T085534.000 000000000031744 Lewis (1912, 1918). Material conditional critique. Modal implication. S1-S5 systems. Foundation of modal logic.
Logic of Proofs⤓ .md 2026-10-22T092209.000 000000000038008 Artemov introduced Logic of Proofs LP (1995, 2001). Explicit justification logic. t:A means "t is a proof of A." Realizes modal logic S4: □A becomes t:A for some proof term t. Provides computational semantics for modality.
Modal Dependence Logic⤓ .md 2026-08-20T022201.000 000000000039064 Jouko Väänänen, "Modal dependence logic" (in New Perspectives on Games and Interaction, 2008), transposing his 2007 first-order dependence logic to the modal setting. Sevenster (2009) settled the complexity; Ebbing, Lohmann, Hella, Kontinen, Müller, and Vollmer mapped the fragments (2011–2013); Yang and Väänänen (2016) gave the propositional theory.
Modal Logic⤓ .md 2026-10-22T085201.000 000000000043384 C.I. Lewis introduced strict implication (1918) to address paradoxes of material implication. Saul Kripke (1959, 1963) provided the possible worlds semantics that made modal logic mathematically tractable. Ruth Barcan Marcus developed quantified modal logic. Jaakko Hintikka connected it to epistemology.
Modal Type Theory⤓ .md 2026-10-22T165042.936 000000000000800 Frank Pfenning and Rowan Davies, "A judgmental reconstruction of modal logic" (Mathematical Structures in Computer Science, 2001), which gave the dual-context system that everything since builds on; Davies and Pfenning's staged-computation reading (1996, 2001); Bierman and de Paiva's categorical account of intuitionistic S4 (2000). Fitch-style presentations descend from Fitch (1952) and were revived by Clouston (2018); Gratzer, Kavvos, Nuyts, and Birkedal's MTT (2020) parametrizes over a mode theory.
Neighborhood Semantics⤓ .md 2026-10-22T090714.000 000000000046648 Dana Scott and Richard Montague independently developed neighborhood semantics (1970). Generalizes Kripke semantics to non-normal modal logics. Each world has a neighborhood: sets of propositions that are "necessary" at that world. Captures modalities that don't satisfy all normal modal axioms. Foundation for various non-standard modalities.
Non-normal Modal Logics⤓ .md 2026-10-22T090714.000 000000000046648 Dana Scott and Richard Montague independently developed neighborhood semantics (1970). Generalizes Kripke semantics to non-normal modal logics. Each world has a neighborhood: sets of propositions that are "necessary" at that world. Captures modalities that don't satisfy all normal modal axioms. Foundation for various non-standard modalities.
Polyadic Modal Logic⤓ .md 2026-10-22T085752.000 000000000045408 Jónsson and Tarski, "Boolean Algebras with Operators" (1951), already worked with operators of arbitrary finite arity and proved the representation theorem at that generality. Goldblatt, "Varieties of Complex Algebras" (1989), and Venema's dissertation Many-Dimensional Modal Logic (1992) developed the modal side, and Blackburn, de Rijke and Venema, Modal Logic (2001), made the arbitrary modal similarity type the default setting rather than a generalization of the unary case.
Propositionally Quantified Modal Logic⤓ .md 2026-10-22T180154.561 000000000000968 R. A. Bull, "On modal logic with propositional quantifiers" (Journal of Symbolic Logic 34, 1969, 257–263), extended modal calculi with ∀p and its introduction rules. Kit Fine, "Propositional quantifiers in modal logic" (Theoria 36, 1970, 336–346), set the field's agenda: the systems Kπ+, Tπ+, K4π+, S4π+, S4.2π+, Bπ+, and S5π+ with the quantifiers ranging over all sets of worlds, decidability for S5 — shown also by David Kaplan (1970) — and the encoding of second-order arithmetic in the rest. Michael Kaminski and Michael Tiomkin, "The expressive power of second-order propositional modal logic" (Notre Dame Journal of Formal Logic 37, 1996, 35–43), published the full second-order equivalence. Peter Fritz, "Axiomatizability of propositionally quantified modal logics on relational frames" (Journal of Symbolic Logic 89, 2024, 758–793), The Foundations of Modality: From Propositions to Possible Worlds (Oxford 2023), and Propositional Quantifiers (Cambridge Elements, 2024) are the current book-length and survey treatments.
Provability Logic⤓ .md 2026-10-22T085307.000 000000000041808 Gödel noted the connection between modal logic and provability (1933). Robert Solovay proved arithmetic completeness of GL (1976): the modal logic of provability in Peano Arithmetic. George Boolos developed the field extensively (The Logic of Provability, 1993). Bridges modal logic, proof theory, and foundations of mathematics.
S4 Modal Logic⤓ .md 2026-10-22T085340.000 000000000044768 Lewis and Langford, Symbolic Logic (1932), Appendix II, introduced S1–S5 as systems of strict implication. Gödel, "Eine Interpretation des intuitionistischen Aussagenkalküls" (1933), gave the modern axiomatization as K + T + 4 and translated intuitionistic propositional logic into it. McKinsey and Tarski, "The Algebra of Topology" (1944) and "Some Theorems About the Sentential Calculi of Lewis and Heyting" (1948), supplied the topological and algebraic semantics and proved the translation faithful. Kripke's relational semantics (1963) identified the frame condition as reflexive transitivity.
S5 Modal Logic⤓ .md 2026-08-20T010732.000 000000000046152 Lewis and Langford, Symbolic Logic (1932), Appendix II, listed S5 as the strongest of the systems of strict implication. Carnap, Meaning and Necessity (1947), read necessity as truth in all state-descriptions, which validates exactly S5. Kripke, "A Completeness Theorem in Modal Logic" (1959), proved completeness for S5 using the universal accessibility relation; Kripke (1963) then recast the condition as an equivalence relation. Scroggs, "Extensions of the Lewis System S5" (1951), had already mapped its proper normal extensions.
Sahlqvist Correspondence⤓ .md 2026-10-22T090413.000 000000000034744 Henrik Sahlqvist (1975). Modal formulas with first-order correspondents. Syntactic class guaranteeing correspondence. Canonical frame validity. Automatic axiomatization.
Spatial Logic⤓ .md 2026-08-20T102427.000 000000000037264 Multiple traditions: topology-based (McKinsey-Tarski, 1940s), mereotopology (Whitehead, Clarke), region-based (Randell et al., 1992). Logics for spatial reasoning. Modal interpretations on topological spaces. Region Connection Calculus (RCC) for qualitative spatial relations. Applications in GIS, robotics, image analysis.
Strict Conditional⤓ .md 2026-10-22T085534.000 000000000031744 Lewis (1912, 1918). Material conditional critique. Modal implication. S1-S5 systems. Foundation of modal logic.
Subvaluationism⤓ .md 2026-08-20T024101.000 000000000040280 Hyde (1997), Varzi: the dual of supervaluationism over the same precisification frame. Sub-truth is the possibility modality ◇—truth on at least one admissible precisification—so that borderline cases become truth-value gluts and the resulting consequence is paraconsistent.
Supervaluationism⤓ .md 2026-08-20T023930.000 000000000041904 Van Fraassen (1966) introduced supervaluations for truth-value gaps, but the semantics is modal in structure. The space of admissible precisifications is a Kripke frame, and the "definitely" operator D is a normal necessity □ quantifying over accessible precisifications. Classical theorems survive the gaps because every point of the frame is itself a classical valuation.
T Modal Logic⤓ .md 2026-10-22T085606.000 000000000038488 Robert Feys, "Les logiques nouvelles des modalités" (1937), introduced the system as t; von Wright, An Essay in Modal Logic (1951), arrived at the same logic and called it M. The two names converged on T, presented in Kripke-era notation as KT: the smallest normal modal logic containing □A → A. It is the weakest standard system in which necessity is veridical.
Two-Dimensionalism⤓ .md 2026-08-20T023429.000 000000000037080 Kaplan (1977), Stalnaker, Chalmers. Context and circumstance. A priori vs necessary. Primary and secondary intensions. Foundation for epistemology of modality.
CRITERIA⤓ .txt 2026-10-22T165042.936 000000000000736 Not sufficient: A conditional whose constraint is content containment, variable inclusion, or exact verification rather than a modal or similarity semantics (Hyperintensional). An essentialist operator advanced as an alternative to modal analysis rather than a form of it (Hyperintensional). An obligation reading (Deontic). A knowledge or belief reading (Epistemic). A temporal reading (Temporal). A program or action modality (Dynamic).