README⤓ .txt 2026-07-17T121634.146 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.
Bisimulation Modal Logic⤓ .md 2026-07-15T063642.000 000000000019264 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-07-15T054813.000 000000000026728 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-07-15T074445.000 000000000014616 Montgomery and Routley (1966). Contingency as primitive. Δφ: φ is contingent. Non-interdefinability with necessity. Foundation for modal analysis.
Counterpart Theory⤓ .md 2026-07-15T074647.000 000000000014712 Lewis (1968). No transworld identity. Counterparts represent de re. Modal realism. Foundation for modal metaphysics.
Discussive Logic⤓ .md 2026-07-16T004541.000 000000000034608 Stanisław Jaśkowski, "Propositional calculus for contradictory deductive systems" (Studia Societatis Scientiarum Torunensis, 1948; English 1969) — the first paraconsistent logic, four years before Priest was born and fifteen 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. Da Costa and Dubikajtis (1977) axiomatized it.
First-Order Modal Logic⤓ .md 2026-07-15T073259.000 000000000014744 Carnap, Kripke (1960s). Quantifiers meet modalities. Varying domains. Rigid vs non-rigid designators. Foundation for quantified intensional logic.
Fusion and Products⤓ .md 2026-07-15T233630.000 000000000035624 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.
Graded Modal Logic⤓ .md 2026-07-15T060708.000 000000000020584 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-07-15T071522.000 000000000014016 Grzegorczyk (1967). Modal logic of provability in intuitionistic arithmetic. S4 + Grzegorczyk axiom. No infinite ascending chains. Foundation for provability and intuitionism connection.
Hybrid Logic⤓ .md 2026-07-15T054121.000 000000000029176 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-07-15T233537.000 000000000017200 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-07-15T074922.000 000000000013672 Visser (1990s). One theory interprets another. □ for provability, ⊳ for interpretability. IL systems. Foundation for relative consistency.
Jonsson-Tarski Duality⤓ .md 2026-07-17T120407.600 000000000000840 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-07-15T054815.000 000000000026744 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-07-17T120407.600 000000000000768 Kripke (1959, 1963). Minimal normal modal. No frame conditions. Weakest normal system. Foundation of modal semantics.
KB Modal Logic⤓ .md 2026-07-15T235628.000 000000000014120 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.
Logic of Proofs⤓ .md 2026-07-15T063117.000 000000000018408 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-07-17T120407.600 000000000000768 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-07-15T052402.000 000000000025544 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-07-16T001655.000 000000000037448 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-07-15T055430.000 000000000025440 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-07-15T072719.000 000000000013416 Venema (1991), expanding modal operators to multiple arguments. Generalized modalities. n-ary accessibility. Foundation for complex modal interactions.
Provability Logic⤓ .md 2026-07-15T055414.000 000000000025672 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-07-17T120407.600 000000000000776 Lewis (1932), Kripke semantics (1963). Reflexive + transitive. Topological interpretation. Foundation of epistemic/provability readings.
S5 Modal Logic⤓ .md 2026-07-17T120407.600 000000000000776 Lewis (1932), Kripke (1963). Equivalence relations. Maximal normal modal. Metaphysical necessity. Foundation of possible worlds metaphysics.
Sahlqvist Correspondence⤓ .md 2026-07-15T064852.000 000000000015928 Henrik Sahlqvist (1975). Modal formulas with first-order correspondents. Syntactic class guaranteeing correspondence. Canonical frame validity. Automatic axiomatization.
Spatial Logic⤓ .md 2026-07-15T060659.000 000000000021672 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-07-17T120407.600 000000000000808 Lewis (1912, 1918). Material conditional critique. Modal implication. S1-S5 systems. Foundation of modal logic.
Subvaluationism⤓ .md 2026-07-15T202510.000 000000000021496 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-07-15T202451.000 000000000025056 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-07-17T120407.600 000000000000768 Feys (1937), von Wright. Reflexive frames. Truth axiom. Veridicality. Foundation of factive modality.
Two-Dimensionalism⤓ .md 2026-07-15T074651.000 000000000015352 Kaplan (1977), Stalnaker, Chalmers. Context and circumstance. A priori vs necessary. Primary and secondary intensions. Foundation for epistemology of modality.
CRITERIA⤓ .txt 2026-07-17T121634.146 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).