Modal logic: axioms, the lattice of normal logics, and the modal square

[dowty-wall-peters-1981] [Kra81] [Kri63]

Builds on the polymorphic Kripke foundation in Defs.lean. This file adds:

1. Modal axiom correspondence (T, D, 4, B, 5): which frame conditions on R validate which modal axioms when interpreted via box/diamond. The K axiom holds for any R.

2. Monotonicity, distribution, restriction: standard properties of normal modal operators. Restriction (box_restrict) is Kratzer's insight that conversational backgrounds strengthen necessity.

3. Decidable instances: box R p w, diamond R p w are decidable over finite worlds with decidable accessibility and propositions.

4. Logic lattice: Axiom, Logic, named logics (K, T, D, S4, S5, KD45), lattice instances, frameConditions predicate.

5. Gallin hierarchy ([Gal75]): PropOp (general propositional operators), indicialNec/indicialPoss (Kripke-type), s5Nec/s5Poss (universal-accessibility = classical IL S5). The architectural anchor showing that classical IL S5 = the universal-accessibility special case of the polymorphic theory, and that non-Kripke operators (tense, progressive) live outside IsIndicial.

6. Modal square of opposition (modalSquare, [CP08a]): under seriality the box/diamond corners satisfy all six Aristotelian relations — subalternAI is the D axiom, contradEI the box–diamond duality.

Connection to Kratzer semantics

Kratzer's conversational backgrounds derive accessibility from a modal base: R_f(w, w') ≡ w' ∈ ⋂f(w). The ordering source further restricts to "best" worlds. In IL terms:

• Simple Kratzer necessity = box R_f (no ordering source)
• Full Kratzer necessity = box R_{f,g} where R_{f,g} restricts to best worlds
• S5 necessity = box universalR

theorem Core.Logic.Modal.box_K {W : Type u_1} (R : AccessRel W) (p q : W → Prop) (w : W) (hpq : box R (fun (v : W) => p v → q v) w) (hp : box R p w) : box R q w

K axiom: □_R(p → q) → (□_R p → □_R q). Holds for any accessibility relation.

theorem Core.Logic.Modal.box_T {W : Type u_1} (R : AccessRel W) [Std.Refl R] (p : W → Prop) (w : W) (h : box R p w) : p w

T axiom: reflexive R gives □_R p w → p w. What is necessary is actual.

theorem Core.Logic.Modal.box_D {W : Type u_1} (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) (w : W) (h : box R p w) : diamond R p w

D axiom: serial R gives □_R p w → ◇_R p w. What is necessary is possible.

theorem Core.Logic.Modal.box_four {W : Type u_1} (R : AccessRel W) [IsTrans W R] (p : W → Prop) (w : W) (h : box R p w) : box R (box R p) w

4 axiom: transitive R gives □_R p → □_R □_R p. Positive introspection.

theorem Core.Logic.Modal.box_B {W : Type u_1} (R : AccessRel W) [Std.Symm R] (p : W → Prop) (w : W) (h : p w) : box R (diamond R p) w

B axiom: symmetric R gives p w → □_R ◇_R p w. What is actual is necessarily possible.

theorem Core.Logic.Modal.box_five {W : Type u_1} (R : AccessRel W) [hE : IsEuclidean R] (p : W → Prop) (w : W) (h : diamond R p w) : box R (diamond R p) w

5 axiom: euclidean R gives ◇_R p w → □_R ◇_R p w. Positive possibility introspection.

theorem Core.Logic.Modal.box_not_moore {W : Type u_1} (R : AccessRel W) [hS : IsSerial R] [IsTrans W R] (p : W → Prop) (w : W) : ¬box R (fun (v : W) => p v ∧ ¬box R p v) w

Moore reductio for KD4: no world satisfies □_R (p ∧ ¬□_R p) when R is serial and transitive. The content p ∧ ¬□_R p is itself satisfiable; what fails is boxing it. Specialise to belief ([Hin62]), knowledge, or any other KD4 modality.

Modal square of opposition

[CP08a]. The □/◇ pair forms an Aristotelian square (A = □p, E = □¬p, I = ◇p, O = ¬□p). Under seriality — the modal D axiom (box_D) — it satisfies all six relations of the square of opposition, so every serial modality (epistemic, deontic, temporal, doxastic) inherits the square.

theorem Core.Logic.Modal.box_disjoint_compl {W : Type u_1} (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) : Disjoint (box R p) (box R pᶜ)

Under seriality, □p and □¬p are incompatible: no world satisfies both.

theorem Core.Logic.Modal.diamond_eq_compl_box_compl {W : Type u_1} (R : AccessRel W) (p : W → Prop) : diamond R p = (box R pᶜ)ᶜ

Box–diamond duality as an equation of predicates: ◇p = ¬□¬p.

def Core.Logic.Modal.modalSquare {W : Type u_1} (R : AccessRel W) (p : W → Prop) : Aristotelian.Square (W → Prop)

The modal square of opposition over an accessibility relation R ([CP08a]): A = □p, E = □¬p, I = ◇p, O = ¬□p.

Equations

• Core.Logic.Modal.modalSquare R p = { A := Core.Logic.Modal.box R p, E := Core.Logic.Modal.box R pᶜ, I := Core.Logic.Modal.diamond R p, O := (Core.Logic.Modal.box R p)ᶜ }

theorem Core.Logic.Modal.modalSquare_relations {W : Type u_1} (R : AccessRel W) [IsSerial R] (p : W → Prop) : Aristotelian.SquareRelations (modalSquare R p)

The modal square satisfies all six Aristotelian relations whenever R is serial. subalternAI is exactly the D axiom (box_D : □p → ◇p); the two contradiction diagonals combine isCompl_compl with box–diamond duality; and contrariety/subcontrariety reduce to box_disjoint_compl.

theorem Core.Logic.Modal.box_mono {W : Type u_1} (R : AccessRel W) {p q : W → Prop} (h : ∀ (v : W), p v → q v) (w : W) (hb : box R p w) : box R q w

box R is monotone: if p ≤ q pointwise, then □_R p ≤ □_R q.

theorem Core.Logic.Modal.diamond_mono {W : Type u_1} (R : AccessRel W) {p q : W → Prop} (h : ∀ (v : W), p v → q v) (w : W) (hd : diamond R p w) : diamond R q w

diamond R is monotone.

theorem Core.Logic.Modal.box_conj {W : Type u_1} (R : AccessRel W) (p q : W → Prop) (w : W) : box R (fun (v : W) => p v ∧ q v) w = (box R p w ∧ box R q w)

□_R distributes over ∧.

theorem Core.Logic.Modal.diamond_disj {W : Type u_1} (R : AccessRel W) (p q : W → Prop) (w : W) : diamond R (fun (v : W) => p v ∨ q v) w = (diamond R p w ∨ diamond R q w)

◇_R distributes over ∨.

theorem Core.Logic.Modal.box_necessitation {W : Type u_1} (R : AccessRel W) (p : W → Prop) (h : ∀ (v : W), p v) (w : W) : box R p w

Necessitation: if p holds at every world, then □_R p holds everywhere.

theorem Core.Logic.Modal.box_restrict {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) (hb : box R₁ p w) : box R₂ p w

Restricting accessibility strengthens necessity: if R₂ ⊆ R₁, then □_{R₁} p → □_{R₂} p.

theorem Core.Logic.Modal.self_imp_box_flip_diamond {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) (h : p w) : box (flip R) (diamond R p) w

Conversion (Prior's tense axiom A ⊃ G P A / A ⊃ H F A): for R and its converse flip R, p w → □_{flip R} ◇_R p w. The correspondence fact that two modalities over a relation and its converse are temporally adjoint (holds for any R).

theorem Core.Logic.Modal.diamond_restrict {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) (hd : diamond R₂ p w) : diamond R₁ p w

Restricting accessibility weakens possibility: if R₂ ⊆ R₁, then ◇_{R₂} p → ◇_{R₁} p.

theorem Core.Logic.Modal.S5_frame_all_axioms {W : Type u_1} (R : AccessRel W) [Std.Refl R] [IsEuclidean R] : (∀ (p : W → Prop) (w : W), box R p w → p w) ∧ (∀ (p : W → Prop) (w : W), box R p w → diamond R p w) ∧ (∀ (p : W → Prop) (w : W), box R p w → box R (box R p) w) ∧ (∀ (p : W → Prop) (w : W), p w → box R (diamond R p) w) ∧ ∀ (p : W → Prop) (w : W), diamond R p w → box R (diamond R p) w

With reflexive + euclidean accessibility (= S5 frame conditions), box validates all of T, D, 4, B, 5.

theorem Core.Logic.Modal.KD45_frame_all_axioms {W : Type u_1} (R : AccessRel W) [IsKD45Frame R] : (∀ (p : W → Prop) (w : W), box R p w → diamond R p w) ∧ (∀ (p : W → Prop) (w : W), box R p w → box R (box R p) w) ∧ ∀ (p : W → Prop) (w : W), diamond R p w → box R (diamond R p) w

KD45 frame conditions validate all three KD45 axioms (D, 4, 5).

theorem Core.Logic.Modal.box_eq_forall {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : box R p w = ∀ (v : W), R w v → p v

box R p i is the infimum of p v over worlds v accessible from w.

theorem Core.Logic.Modal.diamond_eq_exists {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : diamond R p w = ∃ (v : W), R w v ∧ p v

diamond R p w is the supremum of p v over worlds v accessible from w.

The Gallin hierarchy ([Gal75])

In IL/ML_p, propositional operators form a three-level hierarchy:

1. General (PropOp): Any (W → Prop) → W → Prop — arbitrary properties of propositions, varying by world.

2. Indicial (= Kripke-type): Operators definable via an accessibility relation R. The necessity variant is ∀ v, R w v → p v (= box); the possibility variant is ∃ v, R w v ∧ p v (= diamond).

3. S5: The indicial case with R = universalR — IL's box/diamond.

All PropOps  ⊋  Indicial (Kripke)  ⊋  S5 (IL's □)

Why this is here even with no current downstream consumer. These theorems are the architectural anchor for the design choice that restricted modality lives in Semantics/Intensional/: they prove that classical IL S5 is exactly the universal-accessibility special case of the polymorphic theory, and that every box R is a normal modal operator (monotone, distribConj). Non-indicial PropOps (e.g., tense, present progressive) are the formal extension point for tense / non-Kripke modal operators that cannot be expressed as box R for any R. Removing this section would erase the formal record of why the directory layout is what it is.

@[reducible, inline]

abbrev Core.Logic.Modal.PropOp (W : Type u_2) : Type u_2

A propositional operator: any function from propositions to propositions, parametrized by world. This is Gallin's most general level — an arbitrary property of propositions varying by index.

Examples: necessity (box R), possibility (diamond R), past tense (∃ v, v < w ∧ p v), present progressive, habituals.

Equations

• Core.Logic.Modal.PropOp W = ((W → Prop) → W → Prop)

def Core.Logic.Modal.PropOp.Monotone {W : Type u_2} (N : PropOp W) : Prop

A propositional operator N is monotone if p ≤ q pointwise implies N p ≤ N q pointwise. Every K-operator (= normal modal operator) is monotone.

Equations

• N.Monotone = ∀ {p q : W → Prop}, (∀ (v : W), p v → q v) → ∀ (w : W), N p w → N q w

def Core.Logic.Modal.PropOp.DistribConj {W : Type u_2} (N : PropOp W) : Prop

A propositional operator distributes over conjunction (one direction of the K axiom: □(p ∧ q) → □p ∧ □q).

Equations

• N.DistribConj = ∀ (p q : W → Prop) (w : W), N (fun (v : W) => p v ∧ q v) w → N p w ∧ N q w

def Core.Logic.Modal.indicialNec {W : Type u_2} (R : AccessRel W) : PropOp W

An indicial necessity operator: the restriction of PropOp to operators definable via an accessibility relation. indicialNec R p w ↔ ∀ v, R w v → p v.

This is box viewed as a member of the Gallin hierarchy.

Equations

• Core.Logic.Modal.indicialNec R p w = ∀ (v : W), R w v → p v

def Core.Logic.Modal.indicialPoss {W : Type u_2} (R : AccessRel W) : PropOp W

An indicial possibility operator (dual). indicialPoss R p w ↔ ∃ v, R w v ∧ p v.

Equations

• Core.Logic.Modal.indicialPoss R p w = ∃ (v : W), R w v ∧ p v

theorem Core.Logic.Modal.box_eq_indicialNec {W : Type u_1} (R : AccessRel W) : box R = indicialNec R

box IS indicialNec — definitional equality.

theorem Core.Logic.Modal.diamond_eq_indicialPoss {W : Type u_1} (R : AccessRel W) : diamond R = indicialPoss R

diamond IS indicialPoss — definitional equality.

def Core.Logic.Modal.IsIndicial {W : Type u_2} (N : PropOp W) : Prop

A propositional operator is indicial if there exists an accessibility relation R such that N = indicialNec R. The non-indicial case is where tense and other non-Kripke operators live.

Equations

• Core.Logic.Modal.IsIndicial N = ∃ (R : Core.Logic.Modal.AccessRel W), N = Core.Logic.Modal.indicialNec R

theorem Core.Logic.Modal.box_isIndicial {W : Type u_1} (R : AccessRel W) : IsIndicial (box R)

Every box R is indicial.

theorem Core.Logic.Modal.indicial_monotone {W : Type u_1} (R : AccessRel W) : (indicialNec R).Monotone

Every indicial operator is monotone (every Kripke operator is a K-operator).

theorem Core.Logic.Modal.indicial_distribConj {W : Type u_1} (R : AccessRel W) : (indicialNec R).DistribConj

Every indicial operator distributes over conjunction.

def Core.Logic.Modal.s5Nec {W : Type u_2} : PropOp W

S5 necessity as a PropOp: p holds at all worlds.

Equations

• Core.Logic.Modal.s5Nec p x✝ = ∀ (w : W), p w

def Core.Logic.Modal.s5Poss {W : Type u_2} : PropOp W

S5 possibility as a PropOp: p holds at some world.

Equations

• Core.Logic.Modal.s5Poss p x✝ = ∃ (w : W), p w

Flat S5 operators (world-collapsed)

poss/nec are the genuinely flat existential/universal modals (∃ w / ∀ w), the world-collapsed projection of s5Poss/s5Nec, whose evaluation world is vestigial. These are the canonical flat modals consumed by the implicature calculus (Exhaustification.FreeChoice) and free-choice scope theory, which do not track an evaluation world; s5Poss_apply/s5Nec_apply connect them back to the PropOp hierarchy.

def Core.Logic.Modal.poss {W : Type u_1} (p : W → Prop) : Prop

Flat S5 possibility: ◇p = ∃ w, p w (no evaluation world).

Equations

• Core.Logic.Modal.poss p = ∃ (w : W), p w

def Core.Logic.Modal.nec {W : Type u_1} (p : W → Prop) : Prop

Flat S5 necessity: □p = ∀ w, p w (no evaluation world).

Equations

• Core.Logic.Modal.nec p = ∀ (w : W), p w

@[simp]

theorem Core.Logic.Modal.s5Poss_apply {W : Type u_1} (p : W → Prop) (w : W) : s5Poss p w = poss p

@[simp]

theorem Core.Logic.Modal.s5Nec_apply {W : Type u_1} (p : W → Prop) (w : W) : s5Nec p w = nec p

theorem Core.Logic.Modal.poss_or {W : Type u_1} (p q : W → Prop) : (poss fun (w : W) => p w ∨ q w) = (poss p ∨ poss q)

◇ distributes over ∨ (flat): ◇(p ∨ q) = ◇p ∨ ◇q.

theorem Core.Logic.Modal.nec_and {W : Type u_1} (p q : W → Prop) : (nec fun (w : W) => p w ∧ q w) = (nec p ∧ nec q)

□ distributes over ∧ (flat): □(p ∧ q) = □p ∧ □q.

theorem Core.Logic.Modal.poss_mono {W : Type u_1} {p q : W → Prop} (h : ∀ (w : W), p w → q w) : poss p → poss q

◇ is monotone.

theorem Core.Logic.Modal.nec_mono {W : Type u_1} {p q : W → Prop} (h : ∀ (w : W), p w → q w) : nec p → nec q

□ is monotone.

theorem Core.Logic.Modal.s5Nec_eq_indicialNec_universalR {W : Type u_1} : s5Nec = indicialNec universalR

S5 = indicialNec universalR: the S5 necessity operator is the indicial operator with universal accessibility. The formal statement that S5 sits at the top of the indicial hierarchy.

theorem Core.Logic.Modal.s5Nec_isIndicial {W : Type u_1} : IsIndicial s5Nec

S5 necessity is indicial.

theorem Core.Logic.Modal.indicialNec_weaker_of_sub {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) : indicialNec R₁ p w → indicialNec R₂ p w

Restriction order on indicial operators: if R₂ ⊆ R₁ then indicialNec R₁ is weaker than indicialNec R₂ — fewer accessible worlds means a stronger necessity.

S5 (R = universal) is the weakest; empty R is the strongest (vacuously true). This is Kratzer's insight that conversational backgrounds restrict the modal base, formalized at the PropOp level.

theorem Core.Logic.Modal.s5Nec_weakest {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) (h : s5Nec p w) : indicialNec R p w

S5 necessity is the weakest indicial operator: for any R, s5Nec p w → indicialNec R p w.

theorem Core.Logic.Modal.indicialNec_emptyR {W : Type u_1} (p : W → Prop) (w : W) : indicialNec emptyR p w

Empty accessibility gives the strongest (vacuously true) indicial operator.

Decidability over finite worlds

@[implicit_reducible]

instance Core.Logic.Modal.box_decidable {W : Type u_2} [Fintype W] (R : AccessRel W) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (box R p w)

box R p w is decidable when worlds enumerate, accessibility is decidable, and the proposition is decidable.

Equations

• Core.Logic.Modal.box_decidable R p w = decidable_of_iff (∀ v ∈ Finset.univ, R w v → p v) ⋯

@[implicit_reducible]

instance Core.Logic.Modal.diamond_decidable {W : Type u_2} [Fintype W] (R : AccessRel W) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (diamond R p w)

diamond R p w is decidable under the same conditions as box.

Equations

• Core.Logic.Modal.diamond_decidable R p w = decidable_of_iff (∃ v ∈ Finset.univ, R w v ∧ p v) ⋯

inductive Core.Logic.Modal.Axiom : Type

Axiom schemas addable to K.

• M : Axiom
• D : Axiom
• B : Axiom
• four : Axiom
• five : Axiom

@[implicit_reducible]

instance Core.Logic.Modal.instDecidableEqAxiom : DecidableEq Axiom

Equations

• Core.Logic.Modal.instDecidableEqAxiom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Logic.Modal.instReprAxiom : Repr Axiom

Equations

• Core.Logic.Modal.instReprAxiom = { reprPrec := Core.Logic.Modal.instReprAxiom.repr }

def Core.Logic.Modal.instReprAxiom.repr : Axiom → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.instReprAxiom.repr Core.Logic.Modal.Axiom.M prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Logic.Modal.Axiom.M")).group prec✝
• Core.Logic.Modal.instReprAxiom.repr Core.Logic.Modal.Axiom.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Logic.Modal.Axiom.D")).group prec✝
• Core.Logic.Modal.instReprAxiom.repr Core.Logic.Modal.Axiom.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Logic.Modal.Axiom.B")).group prec✝

@[implicit_reducible]

instance Core.Logic.Modal.instInhabitedAxiom : Inhabited Axiom

Equations

• Core.Logic.Modal.instInhabitedAxiom = { default := Core.Logic.Modal.instInhabitedAxiom.default }

@[implicit_reducible]

instance Core.Logic.Modal.instHashableAxiom : Hashable Axiom

Equations

• Core.Logic.Modal.instHashableAxiom = { hash := Core.Logic.Modal.instHashableAxiom.hash }

def Core.Logic.Modal.instHashableAxiom.hash : Axiom → UInt64

Equations

• Core.Logic.Modal.instHashableAxiom.hash Core.Logic.Modal.Axiom.M = 0
• Core.Logic.Modal.instHashableAxiom.hash Core.Logic.Modal.Axiom.D = 1
• Core.Logic.Modal.instHashableAxiom.hash Core.Logic.Modal.Axiom.B = 2
• Core.Logic.Modal.instHashableAxiom.hash Core.Logic.Modal.Axiom.four = 3
• Core.Logic.Modal.instHashableAxiom.hash Core.Logic.Modal.Axiom.five = 4

@[implicit_reducible]

instance Core.Logic.Modal.instToStringAxiom : ToString Axiom

Equations

• One or more equations did not get rendered due to their size.

structure Core.Logic.Modal.Logic : Type

A normal modal logic is K plus axiom schemas.

• axioms : Finset Axiom

def Core.Logic.Modal.instDecidableEqLogic.decEq (x✝ x✝¹ : Logic) : Decidable (x✝ = x✝¹)

Equations

• Core.Logic.Modal.instDecidableEqLogic.decEq { axioms := a } { axioms := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Logic.Modal.instDecidableEqLogic : DecidableEq Logic

Equations

• Core.Logic.Modal.instDecidableEqLogic = Core.Logic.Modal.instDecidableEqLogic.decEq

def Core.Logic.Modal.Logic.K : Logic

Equations

• Core.Logic.Modal.Logic.K = { axioms := ∅ }

def Core.Logic.Modal.Logic.T : Logic

Equations

• Core.Logic.Modal.Logic.T = { axioms := {Core.Logic.Modal.Axiom.M} }

def Core.Logic.Modal.Logic.D : Logic

Equations

• Core.Logic.Modal.Logic.D = { axioms := {Core.Logic.Modal.Axiom.D} }

def Core.Logic.Modal.Logic.KB : Logic

Equations

• Core.Logic.Modal.Logic.KB = { axioms := {Core.Logic.Modal.Axiom.B} }

def Core.Logic.Modal.Logic.K4 : Logic

Equations

• Core.Logic.Modal.Logic.K4 = { axioms := {Core.Logic.Modal.Axiom.four} }

def Core.Logic.Modal.Logic.K5 : Logic

Equations

• Core.Logic.Modal.Logic.K5 = { axioms := {Core.Logic.Modal.Axiom.five} }

def Core.Logic.Modal.Logic.S4 : Logic

Equations

• Core.Logic.Modal.Logic.S4 = { axioms := {Core.Logic.Modal.Axiom.M, Core.Logic.Modal.Axiom.four} }

def Core.Logic.Modal.Logic.S5 : Logic

Equations

• Core.Logic.Modal.Logic.S5 = { axioms := {Core.Logic.Modal.Axiom.M, Core.Logic.Modal.Axiom.five} }

def Core.Logic.Modal.Logic.KTB : Logic

Equations

• Core.Logic.Modal.Logic.KTB = { axioms := {Core.Logic.Modal.Axiom.M, Core.Logic.Modal.Axiom.B} }

def Core.Logic.Modal.Logic.KD45 : Logic

Equations

• Core.Logic.Modal.Logic.KD45 = { axioms := {Core.Logic.Modal.Axiom.D, Core.Logic.Modal.Axiom.four, Core.Logic.Modal.Axiom.five} }

def Core.Logic.Modal.Logic.K45 : Logic

Equations

• Core.Logic.Modal.Logic.K45 = { axioms := {Core.Logic.Modal.Axiom.four, Core.Logic.Modal.Axiom.five} }

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instLE : LE Logic

L₁ ≤ L₂ means L₁ is weaker (fewer axioms).

Equations

• Core.Logic.Modal.Logic.instLE = { le := fun (L₁ L₂ : Core.Logic.Modal.Logic) => L₁.axioms ⊆ L₂.axioms }

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instPartialOrder : PartialOrder Logic

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instLattice : Lattice Logic

Equations

• One or more equations did not get rendered due to their size.

def Core.Logic.Modal.Logic.top : Logic

Equations

• Core.Logic.Modal.Logic.top = { axioms := {Core.Logic.Modal.Axiom.M, Core.Logic.Modal.Axiom.D, Core.Logic.Modal.Axiom.B, Core.Logic.Modal.Axiom.four, Core.Logic.Modal.Axiom.five} }

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instOrderBot : OrderBot Logic

Equations

• Core.Logic.Modal.Logic.instOrderBot = { bot := Core.Logic.Modal.Logic.K, bot_le := Core.Logic.Modal.Logic.instOrderBot._proof_1 }

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instOrderTop : OrderTop Logic

Equations

• Core.Logic.Modal.Logic.instOrderTop = { top := Core.Logic.Modal.Logic.top, le_top := Core.Logic.Modal.Logic.instOrderTop._proof_1 }

@[implicit_reducible]

instance Core.Logic.Modal.Logic.instBoundedOrder : BoundedOrder Logic

Equations

• Core.Logic.Modal.Logic.instBoundedOrder = { toOrderTop := Core.Logic.Modal.Logic.instOrderTop, toOrderBot := Core.Logic.Modal.Logic.instOrderBot }

theorem Core.Logic.Modal.Logic.K_bot : K = ⊥

theorem Core.Logic.Modal.Logic.top_all_axioms : top = ⊤

def Core.Logic.Modal.Logic.hasAxiom (L : Logic) (a : Axiom) : Bool

Equations

• L.hasAxiom a = decide (a ∈ L.axioms)

def Core.Logic.Modal.Logic.frameConditions {W : Type u_2} (L : Logic) (R : AccessRel W) : Prop

Frame conditions required by a logic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Core.Logic.Modal.Logic.frameConditions_S5_iff {W : Type u_2} (R : AccessRel W) : S5.frameConditions R ↔ Std.Refl R ∧ IsEuclidean R

The syntactic-semantic bridge for S5: frameConditions Logic.S5 R iff R is an S5 frame.

@[simp]

theorem Core.Logic.Modal.Logic.frameConditions_KD45_iff {W : Type u_2} (R : AccessRel W) : KD45.frameConditions R ↔ IsSerial R ∧ IsTrans W R ∧ IsEuclidean R

The syntactic-semantic bridge for KD45.

@[simp]

theorem Core.Logic.Modal.Logic.frameConditions_KTB_iff {W : Type u_2} (R : AccessRel W) : KTB.frameConditions R ↔ Std.Refl R ∧ Std.Symm R

The syntactic-semantic bridge for KTB.