From b71898e1051067ab4f4f906002449d7ba621f547 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sun, 1 Mar 2026 17:40:02 +0900 Subject: [PATCH 1/2] wip --- Foundation/Modal/Hilbert/Normal/Alt.lean | 434 +++++++++++++++++++++++ 1 file changed, 434 insertions(+) create mode 100644 Foundation/Modal/Hilbert/Normal/Alt.lean diff --git a/Foundation/Modal/Hilbert/Normal/Alt.lean b/Foundation/Modal/Hilbert/Normal/Alt.lean new file mode 100644 index 000000000..88170c453 --- /dev/null +++ b/Foundation/Modal/Hilbert/Normal/Alt.lean @@ -0,0 +1,434 @@ +module + +public import Foundation.Modal.Entailment.GL +public import Foundation.Modal.Entailment.Grz +public import Foundation.Modal.Entailment.K4Hen +public import Foundation.Modal.Entailment.K4Henkin +public import Foundation.Modal.Entailment.S5Grz +public import Foundation.Modal.Hilbert.Axiom +public import Foundation.Modal.Logic.Basic +public import Foundation.Modal.Logic.Basic +public import Foundation.Propositional.Entailment.Cl.Łukasiewicz + +@[expose] public section + +namespace LO.Modal + +open LO.Entailment LO.Modal.Entailment + +inductive Hilbert.Normal2 {α} (Ax : Set (Formula α)) : Logic α +| axm {φ} : φ ∈ Ax → Normal2 Ax φ +| mdp {φ ψ} : Normal2 Ax (φ ➝ ψ) → Normal2 Ax φ → Normal2 Ax ψ +| nec {φ} : Normal2 Ax φ → Normal2 Ax (□φ) +| implyK φ ψ : Normal2 Ax $ Axioms.ImplyK φ ψ +| implyS φ ψ χ : Normal2 Ax $ Axioms.ImplyS φ ψ χ +| ec φ ψ : Normal2 Ax $ Axioms.ElimContra φ ψ + +namespace Hilbert.Normal2 + +variable {Ax Ax₁ Ax₂ : Axiom α} + +instance : Entailment.Łukasiewicz (Hilbert.Normal2 Ax) where + implyK {_ _} := by constructor; apply Hilbert.Normal2.implyK; + implyS {_ _ _} := by constructor; apply Hilbert.Normal2.implyS; + elimContra {_ _} := by constructor; apply Hilbert.Normal2.ec; + mdp h₁ h₂ := by + constructor; + apply Hilbert.Normal2.mdp; + . exact h₁.1; + . exact h₂.1; + +instance : Entailment.Necessitation (Hilbert.Normal2 Ax) where + nec h := by constructor; apply Hilbert.Normal2.nec; exact h.1; + +lemma axm' {φ} : φ ∈ Ax → Hilbert.Normal2 Ax ⊢ φ := fun h ↦ ⟨⟨axm h⟩⟩ + +protected lemma rec! + {motive : (φ : Formula α) → (Normal2 Ax ⊢ φ) → Sort} + (axm : ∀ {φ : Formula α}, (h : φ ∈ Ax) → motive φ (axm' h)) + (mdp : ∀ {φ ψ : Formula α}, {hφψ : (Normal2 Ax) ⊢ φ ➝ ψ} → {hφ : (Normal2 Ax) ⊢ φ} → motive (φ ➝ ψ) hφψ → motive φ hφ → motive ψ (hφψ ⨀ hφ)) + (nec : ∀ {φ}, {hφψ : (Normal2 Ax) ⊢ φ} → motive (φ) hφψ → motive (□φ) (nec! hφψ)) + (implyK : ∀ {φ ψ}, motive (Axioms.ImplyK φ ψ) $ by simp) + (implyS : ∀ {φ ψ χ}, motive (Axioms.ImplyS φ ψ χ) $ by simp) + (ec : ∀ {φ ψ}, motive (Axioms.ElimContra φ ψ) $ by simp) + : ∀ {φ}, (d : Normal2 Ax ⊢ φ) → motive φ d := by + rintro φ d; + replace d := Logic.iff_provable.mp d; + induction d with + | axm h => apply axm h; + | mdp hφψ hφ ihφψ ihφ => + apply mdp; + . exact ihφψ (Logic.iff_provable.mpr hφψ); + . exact ihφ (Logic.iff_provable.mpr hφ); + | nec hφ ihφ => apply nec; exact ihφ (Logic.iff_provable.mpr hφ); + | implyK φ ψ => apply implyK; + | implyS φ ψ χ => apply implyS; + | ec φ ψ => apply ec; + +lemma weakerThan_of_provable_axioms (hs : Normal2 Ax₂ ⊢* Ax₁) : (Normal2 Ax₁) ⪯ (Normal2 Ax₂) := by + apply Entailment.weakerThan_iff.mpr; + intro φ h; + induction h using Normal2.rec! with + | axm h => apply hs; assumption; + | nec ihφ => apply nec!; simpa; + | mdp ih₁ ih₂ => exact ih₁ ⨀ ih₂; + | _ => simp; + +@[grind <=] +lemma weakerThan_of_subset_axioms (h : Ax₁ ⊆ Ax₂) : (Normal2 Ax₁) ⪯ (Normal2 Ax₂) := by + apply weakerThan_of_provable_axioms; + intro φ hφ; + exact Normal2.axm' $ h hφ; + +open Axiom + + +section + +inductive buildAxioms.Symbol + | B + | C4 + | CD + | D + | Dum + | Five + | Four + | Grz + | H + | Hen + | K + | L + | McK + | Mk + | P + | Point2 + | Point3 + | Point4 + | T + | Tc + | Ver + | WeakPoint2 + | WeakPoint3 + | Z +deriving DecidableEq + +def buildAxioms.Symbol.arity : buildAxioms.Symbol → ℕ + | K + | Mk + | Point3 + | WeakPoint2 + | WeakPoint3 => 2 + | P => 0 + | _ => 1 + +def buildAxioms (α : Type*) (l : List buildAxioms.Symbol) + : Set (Formula α) := + (if l.contains .B then { Axioms.B φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .C4 then { Axioms.C4 φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .CD then { Axioms.CD φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .D then { Axioms.D φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Dum then { Axioms.Dum φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Five then { Axioms.Five φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Four then { Axioms.Four φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Grz then { Axioms.Grz φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .H then { Axioms.H φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Hen then { Axioms.Hen φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .K then { Axioms.K φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪ + (if l.contains .L then { Axioms.L φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .McK then { Axioms.McK φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Mk then { Axioms.Mk φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪ + (if l.contains .P then { Axioms.P } else ∅) ∪ + (if l.contains .Point2 then { Axioms.Point2 φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Point3 then { Axioms.Point3 φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪ + (if l.contains .T then { Axioms.T φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Tc then { Axioms.Tc φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .Ver then { Axioms.Ver φ | (φ : Formula α) } else ∅) ∪ + (if l.contains .WeakPoint2 then { Axioms.WeakPoint2 φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪ + (if l.contains .WeakPoint3 then { Axioms.WeakPoint3 φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪ + (if l.contains .Z then { Axioms.Z φ | (φ : Formula α) } else ∅) + +namespace buildAxioms + +variable {l : List buildAxioms.Symbol} {φ ψ χ : Formula α} + +@[grind <=] +lemma subset_of_subset (h : l₁ ⊆ l₂) : buildAxioms α l₁ ⊆ buildAxioms α l₂ := by + intro A hA; + simp only [buildAxioms, List.contains_eq_mem, decide_eq_true_eq, Set.mem_union, + Set.mem_ite_empty_right, Set.mem_setOf_eq, Set.mem_singleton_iff] at hA ⊢; + repeat rw [or_assoc] at hA; + rcases hA with _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ | _ <;> + grind only [= List.subset_def]; + +lemma mem_axiomK (h : .K ∈ l := by decide) : Axioms.K φ ψ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomD (h : .D ∈ l := by decide) : Axioms.D φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomT (h : .T ∈ l := by decide) : Axioms.T φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomB (h : .B ∈ l := by decide) : Axioms.B φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomFour (h : .Four ∈ l := by decide) : Axioms.Four φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomFive (h : .Five ∈ l := by decide) : Axioms.Five φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomPoint2 (h : .Point2 ∈ l := by decide) : Axioms.Point2 φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomPoint3 (h : .Point3 ∈ l := by decide) : Axioms.Point3 φ ψ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomGrz (h : .Grz ∈ l := by decide) : Axioms.Grz φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomL (h : .L ∈ l := by decide) : Axioms.L φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomP (h : .P ∈ l := by decide) : Axioms.P ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomMcK (h : .McK ∈ l := by decide) : Axioms.McK φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +lemma mem_axiomTc (h : .Tc ∈ l := by decide) : Axioms.Tc φ ∈ buildAxioms α l := by + simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; + grind; + +attribute [simp, grind <=] + mem_axiomK + mem_axiomD + mem_axiomT + mem_axiomB + mem_axiomFour + mem_axiomFive + mem_axiomPoint2 + mem_axiomPoint3 + mem_axiomGrz + mem_axiomP + mem_axiomL + mem_axiomMcK + mem_axiomTc + +end buildAxioms + +end + +end Hilbert.Normal2 + + +section + + +open Lean in +macro "defineModalLogic" name:ident "[" xs:ident,* "]" : command => do + let xs ← xs.getElems.mapM $ λ stx => pure (Lean.mkIdentFrom stx stx.getId) + + let logicName := mkIdent (name.getId.appendAfter "'") + + let instHasAxiomK ← + if xs.contains (mkIdent `K) + then `(command| instance {α} : Entailment.HasAxiomK ($logicName α) where K φ ψ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomD ← + if xs.contains (mkIdent `D) + then `(command| instance {α} : Entailment.HasAxiomD ($logicName α) where D φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomT ← + if xs.contains (mkIdent `T) + then `(command| instance {α} : Entailment.HasAxiomT ($logicName α) where T φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomB ← + if xs.contains (mkIdent `B) + then `(command| instance {α} : Entailment.HasAxiomB ($logicName α) where B φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomFour ← + if xs.contains (mkIdent `Four) + then `(command| instance {α} : Entailment.HasAxiomFour ($logicName α) where Four φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomFive ← + if xs.contains (mkIdent `Five) + then `(command| instance {α} : Entailment.HasAxiomFive ($logicName α) where Five φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomPoint2 ← + if xs.contains (mkIdent `Point2) + then `(command| instance {α} : Entailment.HasAxiomPoint2 ($logicName α) where Point2 φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomPoint3 ← + if xs.contains (mkIdent `Point3) + then `(command| instance {α} : Entailment.HasAxiomPoint3 ($logicName α) where Point3 φ ψ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomGrz ← + if xs.contains (mkIdent `Grz) + then `(command| instance {α} : Entailment.HasAxiomGrz ($logicName α) where Grz φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomL ← + if xs.contains (mkIdent `L) + then `(command| instance {α} : Entailment.HasAxiomL ($logicName α) where L φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomP ← + if xs.contains (mkIdent `P) + then `(command| instance {α} : Entailment.HasAxiomP ($logicName α) where P := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomMcK ← + if xs.contains (mkIdent `McK) + then `(command| instance {α} : Entailment.HasAxiomMcK ($logicName α) where McK φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + let instHasAxiomTc ← + if xs.contains (mkIdent `Tc) + then `(command| instance {α} : Entailment.HasAxiomTc ($logicName α) where Tc φ := by constructor; apply Hilbert.Normal2.axm; simp) + else `(section end) + + `( + abbrev $logicName (α : Type*) := Hilbert.Normal2 $ Hilbert.Normal2.buildAxioms α [$[$xs],*] + + namespace $logicName + + $instHasAxiomK + $instHasAxiomT + $instHasAxiomD + $instHasAxiomPoint2 + $instHasAxiomPoint3 + $instHasAxiomGrz + $instHasAxiomL + $instHasAxiomB + $instHasAxiomFour + $instHasAxiomFive + $instHasAxiomP + $instHasAxiomMcK + $instHasAxiomTc + + end $logicName + ) + +open Hilbert.Normal2.buildAxioms.Symbol + +defineModalLogic Dum [K, T, Four, Dum] +defineModalLogic DumPoint2 [K, T, Four, Dum, Point2] +defineModalLogic DumPoint3 [K, T, Four, Dum, Point3] +defineModalLogic GL [K, L] +defineModalLogic GLPoint2 [K, L, WeakPoint2] +defineModalLogic GLPoint3 [K, L, WeakPoint3] +defineModalLogic Grz [K, Grz] +defineModalLogic GrzPoint2 [K, Grz, Point2] +defineModalLogic GrzPoint3 [K, Grz, Point3] +defineModalLogic K [K] +defineModalLogic K4 [K, Four] +defineModalLogic K45 [K, Four, Five] +defineModalLogic K4Hen [K, Four, Hen] +defineModalLogic K4McK [K, Four, McK] +defineModalLogic K4Point2 [K, Four, WeakPoint2] +defineModalLogic K4Point2Z [K, Four, WeakPoint2, Z] +defineModalLogic K4Point3 [K, Four, WeakPoint3] +defineModalLogic K4Point3Z [K, Four, WeakPoint3, Z] +defineModalLogic K4Z [K, Four, Z] +defineModalLogic K5 [K, Five] +defineModalLogic KB [K, B] +defineModalLogic KP [K, P] +defineModalLogic KB4 [K, B, Four] +defineModalLogic KB5 [K, B, Five] +defineModalLogic KD [K, D] +defineModalLogic KD4 [K, D, Four] +defineModalLogic KD45 [K, D, Four, Five] +defineModalLogic KD4Point3Z [K, D, Four, Point3, Z] +defineModalLogic KD5 [K, D, Five] +defineModalLogic KDB [K, D, B] +defineModalLogic KHen [K, Hen] +defineModalLogic KT [K, T] +defineModalLogic KT4B [K, T, Four, B] +defineModalLogic KTB [K, T, B] +defineModalLogic KTc [K, Tc] +defineModalLogic KTMk [K, T, Mk] +defineModalLogic N [] +defineModalLogic NP [P] +defineModalLogic S4 [K, T, Four] +defineModalLogic S4H [K, T, Four, H] +defineModalLogic S4McK [K, T, Four, McK] +defineModalLogic S4Point2 [K, T, Four, Point2] +defineModalLogic S4Point2McK [K, T, Four, Point2, McK] +defineModalLogic S4Point3 [K, T, Four, Point3] +defineModalLogic S4Point3McK [K, T, Four, Point3, McK] +defineModalLogic S4Point4 [K, T, Four, Point4] +defineModalLogic S4Point4McK [K, T, Four, Point4, McK] +defineModalLogic S5 [K, T, Five] +defineModalLogic S5Grz [K, T, Five, Grz] +defineModalLogic Triv [K, T, Tc] +defineModalLogic Ver [K, Ver] + +end + +section + +open Hilbert.Normal2 + +variable {α} + +instance [DecidableEq α] {L : Logic α} [L.IsNormal] : (Modal.K' α) ⪯ L := by + apply Logic.weakerThan_of_provable; + intro φ hφ; + induction hφ using Hilbert.Normal2.rec! with + | axm h => + rcases (by simpa [Hilbert.Normal2.buildAxioms] using h) with (⟨_, _, rfl⟩) + . simp; + | nec hφ => apply nec! hφ; + | mdp hφψ hφ => exact mdp! hφψ hφ + | implyK | implyS | ec => simp; + + +instance : Entailment.KP (Modal.KP' α) where +instance : Entailment.KD (Modal.KD' α) where + +instance [DecidableEq α] : Modal.KP' α ≊ Modal.KD' α := by + apply Entailment.Equiv.antisymm_iff.mpr; + constructor; + . apply weakerThan_of_provable_axioms; + rintro φ hφ; + rcases (by simpa [Hilbert.Normal2.buildAxioms] using hφ) with (rfl | ⟨_, _, rfl⟩) <;> simp; + . apply weakerThan_of_provable_axioms; + rintro φ hφ; + rcases (by simpa [Hilbert.Normal2.buildAxioms] using hφ) with (⟨_, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; + + +instance : Entailment.S5Grz (Modal.S5Grz' α) where +instance : Entailment.Triv (Modal.Triv' α) where + +instance [DecidableEq α] : Modal.S5Grz' α ≊ Modal.Triv' α := by + apply Entailment.Equiv.antisymm_iff.mpr; + constructor; + . apply weakerThan_of_provable_axioms; + rintro φ hφ; + rcases (by simpa [Hilbert.Normal2.buildAxioms, or_assoc] using hφ) with ⟨_, rfl⟩ | ⟨_, rfl⟩ | ⟨_, _, rfl⟩ | ⟨_, rfl⟩ <;> + simp only [axiomK!, axiomT!, axiomFive!, axiomGrz!]; + . apply weakerThan_of_provable_axioms; + rintro φ hφ; + rcases (by simpa [Hilbert.Normal2.buildAxioms, or_assoc] using hφ) with ⟨_, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ <;> + simp only [axiomK!, axiomT!, axiomTc!]; + + +noncomputable instance [DecidableEq α] [Modal.K4McK' α ⪯ Hilbert.Normal2 Ax] : Entailment.K4McK (Hilbert.Normal2 Ax) where + K _ _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomK! |>.some + Four _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomFour! |>.some + McK _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomMcK! |>.some + +end + +end LO.Modal + +end From b196f4d373f17222e5633bc0f349beca119ebb98 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sun, 1 Mar 2026 20:01:54 +0900 Subject: [PATCH 2/2] refactor hilbert system --- Foundation/Modal/Entailment/Basic.lean | 230 +++++++++--------- Foundation/Modal/Entailment/EM.lean | 3 +- Foundation/Modal/Entailment/EMC.lean | 2 +- Foundation/Modal/Entailment/ET.lean | 2 +- Foundation/Modal/Entailment/ET5.lean | 6 +- Foundation/Modal/Entailment/GL.lean | 8 +- Foundation/Modal/Entailment/Grz.lean | 6 +- Foundation/Modal/Entailment/K.lean | 4 +- Foundation/Modal/Entailment/K4Loeb.lean | 2 +- Foundation/Modal/Entailment/KP.lean | 2 +- Foundation/Modal/Entailment/KT.lean | 2 +- Foundation/Modal/Entailment/KTc.lean | 8 +- Foundation/Modal/Entailment/S5Grz.lean | 2 +- Foundation/Modal/Entailment/Ver.lean | 4 +- Foundation/Modal/Hilbert/Normal/Alt.lean | 185 +++++++++----- .../Modal/Hilbert/WithHenkin/Basic.lean | 2 +- 16 files changed, 268 insertions(+), 200 deletions(-) diff --git a/Foundation/Modal/Entailment/Basic.lean b/Foundation/Modal/Entailment/Basic.lean index aeacbb64f..c81ccb0ed 100644 --- a/Foundation/Modal/Entailment/Basic.lean +++ b/Foundation/Modal/Entailment/Basic.lean @@ -130,19 +130,19 @@ end HasDiaDuality class HasAxiomK [LogicalConnective F] [Box F](𝓢 : S) where - K (φ ψ : F) : 𝓢 ⊢! Axioms.K φ ψ + K {φ ψ : F} : 𝓢 ⊢! Axioms.K φ ψ section HasAxiomK variable [HasAxiomK 𝓢] -def axiomK : 𝓢 ⊢! □(φ ➝ ψ) ➝ □φ ➝ □ψ := HasAxiomK.K _ _ +def axiomK : 𝓢 ⊢! □(φ ➝ ψ) ➝ □φ ➝ □ψ := HasAxiomK.K @[simp] lemma axiomK! : 𝓢 ⊢ □(φ ➝ ψ) ➝ □φ ➝ □ψ := ⟨axiomK⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomK Γ := ⟨fun _ _ ↦ FiniteContext.of axiomK⟩ -instance (Γ : Context F 𝓢) : HasAxiomK Γ := ⟨fun _ _ ↦ Context.of axiomK⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomK Γ := ⟨FiniteContext.of axiomK⟩ +instance (Γ : Context F 𝓢) : HasAxiomK Γ := ⟨Context.of axiomK⟩ def axiomK' (h : 𝓢 ⊢! □(φ ➝ ψ)) : 𝓢 ⊢! □φ ➝ □ψ := axiomK ⨀ h @[simp] lemma axiomK'! (h : 𝓢 ⊢ □(φ ➝ ψ)) : 𝓢 ⊢ □φ ➝ □ψ := ⟨axiomK' h.some⟩ @@ -154,19 +154,19 @@ end HasAxiomK class HasAxiomM [LogicalConnective F] [Box F] (𝓢 : S) where - M (φ ψ : F) : 𝓢 ⊢! Axioms.M φ ψ + M {φ ψ : F} : 𝓢 ⊢! Axioms.M φ ψ section HasAxiomM variable [HasAxiomM 𝓢] -def axiomM : 𝓢 ⊢! □(φ ⋏ ψ) ➝ (□φ ⋏ □ψ) := HasAxiomM.M _ _ +def axiomM : 𝓢 ⊢! □(φ ⋏ ψ) ➝ (□φ ⋏ □ψ) := HasAxiomM.M @[simp] lemma axiomM! : 𝓢 ⊢ □(φ ⋏ ψ) ➝ (□φ ⋏ □ψ) := ⟨axiomM⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomM Γ := ⟨fun _ _ ↦ FiniteContext.of axiomM⟩ -instance (Γ : Context F 𝓢) : HasAxiomM Γ := ⟨fun _ _ ↦ Context.of axiomM⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomM Γ := ⟨FiniteContext.of axiomM⟩ +instance (Γ : Context F 𝓢) : HasAxiomM Γ := ⟨Context.of axiomM⟩ def axiomM' (h : 𝓢 ⊢! □(φ ⋏ ψ)) : 𝓢 ⊢! □φ ⋏ □ψ := axiomM ⨀ h lemma axiomM'! (h : 𝓢 ⊢ □(φ ⋏ ψ)) : 𝓢 ⊢ □φ ⋏ □ψ := ⟨axiomM' h.some⟩ @@ -175,19 +175,19 @@ end HasAxiomM class HasAxiomC [LogicalConnective F] [Box F] (𝓢 : S) where - C (φ ψ : F) : 𝓢 ⊢! Axioms.C φ ψ + C {φ ψ : F} : 𝓢 ⊢! Axioms.C φ ψ section HasAxiomC variable [HasAxiomC 𝓢] -def axiomC : 𝓢 ⊢! (□φ ⋏ □ψ) ➝ □(φ ⋏ ψ) := HasAxiomC.C _ _ +def axiomC : 𝓢 ⊢! (□φ ⋏ □ψ) ➝ □(φ ⋏ ψ) := HasAxiomC.C @[simp] lemma axiomC! : 𝓢 ⊢ (□φ ⋏ □ψ) ➝ □(φ ⋏ ψ) := ⟨axiomC⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomC Γ := ⟨fun _ _ ↦ FiniteContext.of axiomC⟩ -instance (Γ : Context F 𝓢) : HasAxiomC Γ := ⟨fun _ _ ↦ Context.of axiomC⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomC Γ := ⟨FiniteContext.of axiomC⟩ +instance (Γ : Context F 𝓢) : HasAxiomC Γ := ⟨Context.of axiomC⟩ def axiomC' (h : 𝓢 ⊢! □φ ⋏ □ψ) : 𝓢 ⊢! □(φ ⋏ ψ) := axiomC ⨀ h lemma axiomC'! (h : 𝓢 ⊢ □φ ⋏ □ψ) : 𝓢 ⊢ □(φ ⋏ ψ) := ⟨axiomC' h.some⟩ @@ -196,19 +196,19 @@ end HasAxiomC class HasAxiomT (𝓢 : S) where - T (φ : F) : 𝓢 ⊢! Axioms.T φ + T {φ : F} : 𝓢 ⊢! Axioms.T φ section HasAxiomT variable [HasAxiomT 𝓢] -def axiomT : 𝓢 ⊢! □φ ➝ φ := HasAxiomT.T _ +def axiomT : 𝓢 ⊢! □φ ➝ φ := HasAxiomT.T @[simp] lemma axiomT! {φ} : 𝓢 ⊢ □φ ➝ φ := ⟨axiomT⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomT Γ := ⟨fun _ ↦ FiniteContext.of axiomT⟩ -instance (Γ : Context F 𝓢) : HasAxiomT Γ := ⟨fun _ ↦ Context.of axiomT⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomT Γ := ⟨FiniteContext.of axiomT⟩ +instance (Γ : Context F 𝓢) : HasAxiomT Γ := ⟨Context.of axiomT⟩ def axiomT' (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! φ := axiomT ⨀ h @[simp] lemma axiomT'! (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ φ := ⟨axiomT' h.some⟩ @@ -217,19 +217,19 @@ end HasAxiomT class HasAxiomDiaTc (𝓢 : S) where - diaTc (φ : F) : 𝓢 ⊢! Axioms.DiaTc φ + diaTc {φ : F} : 𝓢 ⊢! Axioms.DiaTc φ section HasAxiomDiaTc variable [HasAxiomDiaTc 𝓢] -def diaTc : 𝓢 ⊢! φ ➝ ◇φ := HasAxiomDiaTc.diaTc _ +def diaTc : 𝓢 ⊢! φ ➝ ◇φ := HasAxiomDiaTc.diaTc @[simp] lemma diaTc! : 𝓢 ⊢ φ ➝ ◇φ := ⟨diaTc⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomDiaTc Γ := ⟨fun _ ↦ FiniteContext.of diaTc⟩ -instance (Γ : Context F 𝓢) : HasAxiomDiaTc Γ := ⟨fun _ ↦ Context.of diaTc⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomDiaTc Γ := ⟨FiniteContext.of diaTc⟩ +instance (Γ : Context F 𝓢) : HasAxiomDiaTc Γ := ⟨Context.of diaTc⟩ def diaTc' (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ◇φ := diaTc ⨀ h lemma diaTc'! (h : 𝓢 ⊢ φ) : 𝓢 ⊢ ◇φ := ⟨diaTc' h.some⟩ @@ -238,19 +238,19 @@ end HasAxiomDiaTc class HasAxiomD [Dia F] (𝓢 : S) where - D (φ : F) : 𝓢 ⊢! Axioms.D φ + D {φ : F} : 𝓢 ⊢! Axioms.D φ section HasAxiomD variable [HasAxiomD 𝓢] -def axiomD : 𝓢 ⊢! □φ ➝ ◇φ := HasAxiomD.D _ +def axiomD : 𝓢 ⊢! □φ ➝ ◇φ := HasAxiomD.D @[simp] lemma axiomD! : 𝓢 ⊢ □φ ➝ ◇φ := ⟨axiomD⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomD Γ := ⟨fun _ ↦ FiniteContext.of axiomD⟩ -instance (Γ : Context F 𝓢) : HasAxiomD Γ := ⟨fun _ ↦ Context.of axiomD⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomD Γ := ⟨FiniteContext.of axiomD⟩ +instance (Γ : Context F 𝓢) : HasAxiomD Γ := ⟨Context.of axiomD⟩ def axiomD' (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! ◇φ := axiomD ⨀ h lemma axiomD'! (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ ◇φ := ⟨axiomD' h.some⟩ @@ -295,19 +295,19 @@ end HasAxiomN class HasAxiomB [Dia F] (𝓢 : S) where - B (φ : F) : 𝓢 ⊢! Axioms.B φ + B {φ : F} : 𝓢 ⊢! Axioms.B φ section HasAxiomB variable [HasAxiomB 𝓢] -def axiomB : 𝓢 ⊢! φ ➝ □◇φ := HasAxiomB.B _ +def axiomB : 𝓢 ⊢! φ ➝ □◇φ := HasAxiomB.B @[simp] lemma axiomB! : 𝓢 ⊢ φ ➝ □◇φ := ⟨axiomB⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomB Γ := ⟨fun _ ↦ FiniteContext.of axiomB⟩ -instance (Γ : Context F 𝓢) : HasAxiomB Γ := ⟨fun _ ↦ Context.of axiomB⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomB Γ := ⟨FiniteContext.of axiomB⟩ +instance (Γ : Context F 𝓢) : HasAxiomB Γ := ⟨Context.of axiomB⟩ def axiomB' (h : 𝓢 ⊢! φ) : 𝓢 ⊢! □◇φ := axiomB ⨀ h @[simp] lemma axiomB'! (h : 𝓢 ⊢ φ) : 𝓢 ⊢ □◇φ := ⟨axiomB' h.some⟩ @@ -316,19 +316,19 @@ end HasAxiomB class HasAxiomFour (𝓢 : S) where - Four (φ : F) : 𝓢 ⊢! Axioms.Four φ + Four {φ : F} : 𝓢 ⊢! Axioms.Four φ section HasAxiomFour variable [HasAxiomFour 𝓢] -def axiomFour : 𝓢 ⊢! □φ ➝ □□φ := HasAxiomFour.Four _ +def axiomFour : 𝓢 ⊢! □φ ➝ □□φ := HasAxiomFour.Four @[simp] lemma axiomFour! : 𝓢 ⊢ □φ ➝ □□φ := ⟨axiomFour⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomFour Γ := ⟨fun _ ↦ FiniteContext.of axiomFour⟩ -instance (Γ : Context F 𝓢) : HasAxiomFour Γ := ⟨fun _ ↦ Context.of axiomFour⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomFour Γ := ⟨FiniteContext.of axiomFour⟩ +instance (Γ : Context F 𝓢) : HasAxiomFour Γ := ⟨Context.of axiomFour⟩ def axiomFour' (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! □□φ := axiomFour ⨀ h def axiomFour'! (h : 𝓢 ⊢ □φ) : 𝓢 ⊢ □□φ := ⟨axiomFour' h.some⟩ @@ -337,7 +337,7 @@ end HasAxiomFour class HasAxiomFourN (n) (𝓢 : S) where - FourN (φ : F) : 𝓢 ⊢! Axioms.FourN n φ + FourN {φ : F} : 𝓢 ⊢! Axioms.FourN n φ section @@ -348,188 +348,188 @@ def axiomFourN : 𝓢 ⊢! □^[n]φ ➝ □^[(n + 1)]φ := by apply HasAxiomFou variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomFourN n Γ := ⟨fun _ ↦ FiniteContext.of axiomFourN⟩ -instance (Γ : Context F 𝓢) : HasAxiomFourN n Γ := ⟨fun _ ↦ Context.of axiomFourN⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomFourN n Γ := ⟨FiniteContext.of axiomFourN⟩ +instance (Γ : Context F 𝓢) : HasAxiomFourN n Γ := ⟨Context.of axiomFourN⟩ end class HasAxiomFive [Dia F] (𝓢 : S) where - Five (φ : F) : 𝓢 ⊢! Axioms.Five φ + Five {φ : F} : 𝓢 ⊢! Axioms.Five φ section HasAxiomFive variable [HasAxiomFive 𝓢] -def axiomFive : 𝓢 ⊢! ◇φ ➝ □◇φ := HasAxiomFive.Five _ +def axiomFive : 𝓢 ⊢! ◇φ ➝ □◇φ := HasAxiomFive.Five @[simp] lemma axiomFive! : 𝓢 ⊢ ◇φ ➝ □◇φ := ⟨axiomFive⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomFive Γ := ⟨fun _ ↦ FiniteContext.of axiomFive⟩ -instance (Γ : Context F 𝓢) : HasAxiomFive Γ := ⟨fun _ ↦ Context.of axiomFive⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomFive Γ := ⟨FiniteContext.of axiomFive⟩ +instance (Γ : Context F 𝓢) : HasAxiomFive Γ := ⟨Context.of axiomFive⟩ end HasAxiomFive class HasAxiomL (𝓢 : S) where - L (φ : F) : 𝓢 ⊢! Axioms.L φ + L {φ : F} : 𝓢 ⊢! Axioms.L φ section HasAxiomL variable [HasAxiomL 𝓢] -def axiomL : 𝓢 ⊢! □(□φ ➝ φ) ➝ □φ := HasAxiomL.L _ +def axiomL : 𝓢 ⊢! □(□φ ➝ φ) ➝ □φ := HasAxiomL.L @[simp] lemma axiomL! : 𝓢 ⊢ □(□φ ➝ φ) ➝ □φ := ⟨axiomL⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomL Γ := ⟨fun _ ↦ FiniteContext.of axiomL⟩ -instance (Γ : Context F 𝓢) : HasAxiomL Γ := ⟨fun _ ↦ Context.of axiomL⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomL Γ := ⟨FiniteContext.of axiomL⟩ +instance (Γ : Context F 𝓢) : HasAxiomL Γ := ⟨Context.of axiomL⟩ end HasAxiomL class HasAxiomPoint2 [Dia F] (𝓢 : S) where - Point2 (φ : F) : 𝓢 ⊢! Axioms.Point2 φ + Point2 {φ : F} : 𝓢 ⊢! Axioms.Point2 φ section HasAxiomPoint2 variable [HasAxiomPoint2 𝓢] -def axiomPoint2 : 𝓢 ⊢! ◇□φ ➝ □◇φ := HasAxiomPoint2.Point2 _ +def axiomPoint2 : 𝓢 ⊢! ◇□φ ➝ □◇φ := HasAxiomPoint2.Point2 @[simp] lemma axiomPoint2! : 𝓢 ⊢ ◇□φ ➝ □◇φ := ⟨axiomPoint2⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint2 Γ := ⟨fun _ ↦ FiniteContext.of axiomPoint2⟩ -instance (Γ : Context F 𝓢) : HasAxiomPoint2 Γ := ⟨fun _ ↦ Context.of axiomPoint2⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint2 Γ := ⟨FiniteContext.of axiomPoint2⟩ +instance (Γ : Context F 𝓢) : HasAxiomPoint2 Γ := ⟨Context.of axiomPoint2⟩ end HasAxiomPoint2 class HasAxiomWeakPoint2 [Dia F] (𝓢 : S) where - WeakPoint2 (φ ψ : F) : 𝓢 ⊢! Axioms.WeakPoint2 φ ψ + WeakPoint2 {φ ψ : F} : 𝓢 ⊢! Axioms.WeakPoint2 φ ψ section HasAxiomWeakPoint2 variable [HasAxiomWeakPoint2 𝓢] -def axiomWeakPoint2 : 𝓢 ⊢! ◇(□φ ⋏ ψ) ➝ □(◇φ ⋎ ψ) := HasAxiomWeakPoint2.WeakPoint2 _ _ +def axiomWeakPoint2 : 𝓢 ⊢! ◇(□φ ⋏ ψ) ➝ □(◇φ ⋎ ψ) := HasAxiomWeakPoint2.WeakPoint2 @[simp] lemma axiomWeakPoint2! : 𝓢 ⊢ ◇(□φ ⋏ ψ) ➝ □(◇φ ⋎ ψ) := ⟨axiomWeakPoint2⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomWeakPoint2 Γ := ⟨fun _ _ ↦ FiniteContext.of axiomWeakPoint2⟩ -instance (Γ : Context F 𝓢) : HasAxiomWeakPoint2 Γ := ⟨fun _ _ ↦ Context.of axiomWeakPoint2⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomWeakPoint2 Γ := ⟨FiniteContext.of axiomWeakPoint2⟩ +instance (Γ : Context F 𝓢) : HasAxiomWeakPoint2 Γ := ⟨Context.of axiomWeakPoint2⟩ end HasAxiomWeakPoint2 class HasAxiomPoint3 (𝓢 : S) where - Point3 (φ ψ : F) : 𝓢 ⊢! Axioms.Point3 φ ψ + Point3 {φ ψ : F} : 𝓢 ⊢! Axioms.Point3 φ ψ section HasAxiomPoint3 variable [HasAxiomPoint3 𝓢] -def axiomPoint3 : 𝓢 ⊢! □(□φ ➝ ψ) ⋎ □(□ψ ➝ φ) := HasAxiomPoint3.Point3 _ _ +def axiomPoint3 : 𝓢 ⊢! □(□φ ➝ ψ) ⋎ □(□ψ ➝ φ) := HasAxiomPoint3.Point3 @[simp] lemma axiomPoint3! : 𝓢 ⊢ □(□φ ➝ ψ) ⋎ □(□ψ ➝ φ) := ⟨axiomPoint3⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint3 Γ := ⟨fun _ _ ↦ FiniteContext.of axiomPoint3⟩ -instance (Γ : Context F 𝓢) : HasAxiomPoint3 Γ := ⟨fun _ _ ↦ Context.of axiomPoint3⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint3 Γ := ⟨FiniteContext.of axiomPoint3⟩ +instance (Γ : Context F 𝓢) : HasAxiomPoint3 Γ := ⟨Context.of axiomPoint3⟩ end HasAxiomPoint3 class HasAxiomWeakPoint3 [Dia F] (𝓢 : S) where - WeakPoint3 (φ ψ : F) : 𝓢 ⊢! Axioms.WeakPoint3 φ ψ + WeakPoint3 {φ ψ : F} : 𝓢 ⊢! Axioms.WeakPoint3 φ ψ section HasAxiomWeakPoint3 variable [HasAxiomWeakPoint3 𝓢] -def axiomWeakPoint3 : 𝓢 ⊢! □(⊡φ ➝ ψ) ⋎ □(⊡ψ ➝ φ) := HasAxiomWeakPoint3.WeakPoint3 _ _ +def axiomWeakPoint3 : 𝓢 ⊢! □(⊡φ ➝ ψ) ⋎ □(⊡ψ ➝ φ) := HasAxiomWeakPoint3.WeakPoint3 @[simp] lemma axiomWeakPoint3! : 𝓢 ⊢ □(⊡φ ➝ ψ) ⋎ □(⊡ψ ➝ φ) := ⟨axiomWeakPoint3⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomWeakPoint3 Γ := ⟨fun _ _ ↦ FiniteContext.of axiomWeakPoint3⟩ -instance (Γ : Context F 𝓢) : HasAxiomWeakPoint3 Γ := ⟨fun _ _ ↦ Context.of axiomWeakPoint3⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomWeakPoint3 Γ := ⟨FiniteContext.of axiomWeakPoint3⟩ +instance (Γ : Context F 𝓢) : HasAxiomWeakPoint3 Γ := ⟨Context.of axiomWeakPoint3⟩ end HasAxiomWeakPoint3 class HasAxiomGrz (𝓢 : S) where - Grz (φ : F) : 𝓢 ⊢! Axioms.Grz φ + Grz {φ : F} : 𝓢 ⊢! Axioms.Grz φ section HasAxiomGrz variable [HasAxiomGrz 𝓢] -def axiomGrz : 𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ φ := HasAxiomGrz.Grz _ +def axiomGrz : 𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ φ := HasAxiomGrz.Grz @[simp] lemma axiomGrz! : 𝓢 ⊢ □(□(φ ➝ □φ) ➝ φ) ➝ φ := ⟨axiomGrz⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomGrz Γ := ⟨fun _ ↦ FiniteContext.of axiomGrz⟩ -instance (Γ : Context F 𝓢) : HasAxiomGrz Γ := ⟨fun _ ↦ Context.of axiomGrz⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomGrz Γ := ⟨FiniteContext.of axiomGrz⟩ +instance (Γ : Context F 𝓢) : HasAxiomGrz Γ := ⟨Context.of axiomGrz⟩ end HasAxiomGrz class HasAxiomDum (𝓢 : S) where - Dum (φ : F) : 𝓢 ⊢! Axioms.Dum φ + Dum {φ : F} : 𝓢 ⊢! Axioms.Dum φ section HasAxiomDum variable [HasAxiomDum 𝓢] -def axiomDum : 𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ (◇□φ ➝ φ) := HasAxiomDum.Dum _ +def axiomDum : 𝓢 ⊢! □(□(φ ➝ □φ) ➝ φ) ➝ (◇□φ ➝ φ) := HasAxiomDum.Dum @[simp] lemma axiomDum! : 𝓢 ⊢ □(□(φ ➝ □φ) ➝ φ) ➝ (◇□φ ➝ φ) := ⟨axiomDum⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomDum Γ := ⟨fun _ ↦ FiniteContext.of axiomDum⟩ -instance (Γ : Context F 𝓢) : HasAxiomDum Γ := ⟨fun _ ↦ Context.of axiomDum⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomDum Γ := ⟨FiniteContext.of axiomDum⟩ +instance (Γ : Context F 𝓢) : HasAxiomDum Γ := ⟨Context.of axiomDum⟩ end HasAxiomDum class HasAxiomTc (𝓢 : S) where - Tc (φ : F) : 𝓢 ⊢! Axioms.Tc φ + Tc {φ : F} : 𝓢 ⊢! Axioms.Tc φ section HasAxiomTc variable [HasAxiomTc 𝓢] -def axiomTc : 𝓢 ⊢! φ ➝ □φ := HasAxiomTc.Tc _ +def axiomTc : 𝓢 ⊢! φ ➝ □φ := HasAxiomTc.Tc @[simp] lemma axiomTc! : 𝓢 ⊢ φ ➝ □φ := ⟨axiomTc⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomTc Γ := ⟨fun _ ↦ FiniteContext.of axiomTc⟩ -instance (Γ : Context F 𝓢) : HasAxiomTc Γ := ⟨fun _ ↦ Context.of axiomTc⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomTc Γ := ⟨FiniteContext.of axiomTc⟩ +instance (Γ : Context F 𝓢) : HasAxiomTc Γ := ⟨Context.of axiomTc⟩ end HasAxiomTc class HasAxiomDiaT (𝓢 : S) where - diaT (φ : F) : 𝓢 ⊢! Axioms.DiaT φ + diaT {φ : F} : 𝓢 ⊢! Axioms.DiaT φ section HasAxiomDiaT variable [HasAxiomDiaT 𝓢] -def diaT : 𝓢 ⊢! ◇φ ➝ φ := HasAxiomDiaT.diaT _ +def diaT : 𝓢 ⊢! ◇φ ➝ φ := HasAxiomDiaT.diaT @[simp] lemma diaT! : 𝓢 ⊢ ◇φ ➝ φ := ⟨diaT⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomDiaT Γ := ⟨fun _ ↦ FiniteContext.of diaT⟩ -instance (Γ : Context F 𝓢) : HasAxiomDiaT Γ := ⟨fun _ ↦ Context.of diaT⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomDiaT Γ := ⟨FiniteContext.of diaT⟩ +instance (Γ : Context F 𝓢) : HasAxiomDiaT Γ := ⟨Context.of diaT⟩ def diaT' (h : 𝓢 ⊢! ◇φ) : 𝓢 ⊢! φ := diaT ⨀ h lemma diaT'! (h : 𝓢 ⊢ ◇φ) : 𝓢 ⊢ φ := ⟨diaT' h.some⟩ @@ -538,153 +538,153 @@ end HasAxiomDiaT class HasAxiomVer (𝓢 : S) where - Ver (φ : F) : 𝓢 ⊢! Axioms.Ver φ + Ver {φ : F} : 𝓢 ⊢! Axioms.Ver φ section HasAxiomVer variable [HasAxiomVer 𝓢] -def axiomVer : 𝓢 ⊢! □φ := HasAxiomVer.Ver _ +def axiomVer : 𝓢 ⊢! □φ := HasAxiomVer.Ver @[simp] lemma axiomVer! : 𝓢 ⊢ □φ := ⟨axiomVer⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomVer Γ := ⟨fun _ ↦ FiniteContext.of axiomVer⟩ -instance (Γ : Context F 𝓢) : HasAxiomVer Γ := ⟨fun _ ↦ Context.of axiomVer⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomVer Γ := ⟨FiniteContext.of axiomVer⟩ +instance (Γ : Context F 𝓢) : HasAxiomVer Γ := ⟨Context.of axiomVer⟩ end HasAxiomVer class HasAxiomHen (𝓢 : S) where - Hen (φ : F) : 𝓢 ⊢! Axioms.Hen φ + Hen {φ : F} : 𝓢 ⊢! Axioms.Hen φ section HasAxiomHen variable [HasAxiomHen 𝓢] -def axiomHen : 𝓢 ⊢! □(□φ ⭤ φ) ➝ □φ := HasAxiomHen.Hen _ +def axiomHen : 𝓢 ⊢! □(□φ ⭤ φ) ➝ □φ := HasAxiomHen.Hen @[simp] lemma axiomHen! : 𝓢 ⊢ □(□φ ⭤ φ) ➝ □φ := ⟨axiomHen⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomHen Γ := ⟨fun _ ↦ FiniteContext.of axiomHen⟩ -instance (Γ : Context F 𝓢) : HasAxiomHen Γ := ⟨fun _ ↦ Context.of axiomHen⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomHen Γ := ⟨FiniteContext.of axiomHen⟩ +instance (Γ : Context F 𝓢) : HasAxiomHen Γ := ⟨Context.of axiomHen⟩ end HasAxiomHen class HasAxiomZ (𝓢 : S) where - Z (φ : F) : 𝓢 ⊢! Axioms.Z φ + Z {φ : F} : 𝓢 ⊢! Axioms.Z φ section HasAxiomZ variable [HasAxiomZ 𝓢] -def axiomZ : 𝓢 ⊢! □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := HasAxiomZ.Z _ +def axiomZ : 𝓢 ⊢! □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := HasAxiomZ.Z @[simp] lemma axiomZ! : 𝓢 ⊢ □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := ⟨axiomZ⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ FiniteContext.of axiomZ⟩ -instance (Γ : Context F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ Context.of axiomZ⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomZ Γ := ⟨FiniteContext.of axiomZ⟩ +instance (Γ : Context F 𝓢) : HasAxiomZ Γ := ⟨Context.of axiomZ⟩ end HasAxiomZ class HasAxiomMcK (𝓢 : S) where - McK (φ : F) : 𝓢 ⊢! Axioms.McK φ + McK {φ : F} : 𝓢 ⊢! Axioms.McK φ section HasAxiomMcK variable [HasAxiomMcK 𝓢] -def axiomMcK : 𝓢 ⊢! □◇φ ➝ ◇□φ := HasAxiomMcK.McK _ +def axiomMcK : 𝓢 ⊢! □◇φ ➝ ◇□φ := HasAxiomMcK.McK @[simp] lemma axiomMcK! : 𝓢 ⊢ □◇φ ➝ ◇□φ := ⟨axiomMcK⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomMcK Γ := ⟨fun _ ↦ FiniteContext.of axiomMcK⟩ -instance (Γ : Context F 𝓢) : HasAxiomMcK Γ := ⟨fun _ ↦ Context.of axiomMcK⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomMcK Γ := ⟨FiniteContext.of axiomMcK⟩ +instance (Γ : Context F 𝓢) : HasAxiomMcK Γ := ⟨Context.of axiomMcK⟩ end HasAxiomMcK class HasAxiomMk [LogicalConnective F] [Box F](𝓢 : S) where - Mk (φ ψ : F) : 𝓢 ⊢! Axioms.Mk φ ψ + Mk {φ ψ : F} : 𝓢 ⊢! Axioms.Mk φ ψ section HasAxiomMk variable [HasAxiomMk 𝓢] -def axiomMk : 𝓢 ⊢! □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ) := HasAxiomMk.Mk _ _ +def axiomMk : 𝓢 ⊢! □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ) := HasAxiomMk.Mk @[simp] lemma axiomMk! : 𝓢 ⊢ □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ) := ⟨axiomMk⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomMk Γ := ⟨fun _ _ ↦ FiniteContext.of axiomMk⟩ -instance (Γ : Context F 𝓢) : HasAxiomMk Γ := ⟨fun _ _ ↦ Context.of axiomMk⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomMk Γ := ⟨FiniteContext.of axiomMk⟩ +instance (Γ : Context F 𝓢) : HasAxiomMk Γ := ⟨Context.of axiomMk⟩ end HasAxiomMk class HasAxiomPoint4 [LogicalConnective F] [Box F] (𝓢 : S) where - Point4 (φ : F) : 𝓢 ⊢! Axioms.Point4 φ + Point4 {φ : F} : 𝓢 ⊢! Axioms.Point4 φ section HasAxiomPoint4 variable [HasAxiomPoint4 𝓢] -def axiomPoint4 : 𝓢 ⊢! ◇□φ ➝ φ ➝ □φ := HasAxiomPoint4.Point4 _ +def axiomPoint4 : 𝓢 ⊢! ◇□φ ➝ φ ➝ □φ := HasAxiomPoint4.Point4 @[simp] lemma axiomPoint4! : 𝓢 ⊢ ◇□φ ➝ φ ➝ □φ := ⟨axiomPoint4⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint4 Γ := ⟨fun _ ↦ FiniteContext.of axiomPoint4⟩ -instance (Γ : Context F 𝓢) : HasAxiomPoint4 Γ := ⟨fun _ ↦ Context.of axiomPoint4⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomPoint4 Γ := ⟨FiniteContext.of axiomPoint4⟩ +instance (Γ : Context F 𝓢) : HasAxiomPoint4 Γ := ⟨Context.of axiomPoint4⟩ end HasAxiomPoint4 class HasAxiomH [LogicalConnective F] [Box F] (𝓢 : S) where - H1 (φ : F) : 𝓢 ⊢! Axioms.H φ + H1 {φ : F} : 𝓢 ⊢! Axioms.H φ section variable [HasAxiomH 𝓢] -def axiomH : 𝓢 ⊢! φ ➝ □(◇φ ➝ φ) := HasAxiomH.H1 _ +def axiomH : 𝓢 ⊢! φ ➝ □(◇φ ➝ φ) := HasAxiomH.H1 @[simp] lemma axiomH! : 𝓢 ⊢ φ ➝ □(◇φ ➝ φ) := ⟨axiomH⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomH Γ := ⟨fun _ ↦ FiniteContext.of axiomH⟩ -instance (Γ : Context F 𝓢) : HasAxiomH Γ := ⟨fun _ ↦ Context.of axiomH⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomH Γ := ⟨FiniteContext.of axiomH⟩ +instance (Γ : Context F 𝓢) : HasAxiomH Γ := ⟨Context.of axiomH⟩ end class HasAxiomGeach [LogicalConnective F] (g) (𝓢 : S) where - Geach (φ : F) : 𝓢 ⊢! Axioms.Geach g φ + Geach {φ : F} : 𝓢 ⊢! Axioms.Geach g φ section HasAxiomGeach -instance [Entailment.HasAxiomT 𝓢] : Entailment.HasAxiomGeach ⟨0, 0, 1, 0⟩ 𝓢 := ⟨fun _ => axiomT⟩ -instance [Entailment.HasAxiomB 𝓢] : Entailment.HasAxiomGeach ⟨0, 1, 0, 1⟩ 𝓢 := ⟨fun _ => axiomB⟩ -instance [Entailment.HasAxiomD 𝓢] : Entailment.HasAxiomGeach ⟨0, 0, 1, 1⟩ 𝓢 := ⟨fun _ => axiomD⟩ -instance [Entailment.HasAxiomFour 𝓢] : Entailment.HasAxiomGeach ⟨0, 2, 1, 0⟩ 𝓢 := ⟨fun _ => axiomFour⟩ -instance [Entailment.HasAxiomFourN n 𝓢] : HasAxiomGeach ⟨0, n + 1, n, 0⟩ 𝓢 := ⟨fun _ ↦ axiomFourN⟩ -instance [Entailment.HasAxiomFive 𝓢] : Entailment.HasAxiomGeach ⟨1, 1, 0, 1⟩ 𝓢 := ⟨fun _ => axiomFive⟩ -instance [Entailment.HasAxiomTc 𝓢] : Entailment.HasAxiomGeach ⟨0, 1, 0, 0⟩ 𝓢 := ⟨fun _ => axiomTc⟩ -instance [Entailment.HasAxiomPoint2 𝓢] : Entailment.HasAxiomGeach ⟨1, 1, 1, 1⟩ 𝓢 := ⟨fun _ => axiomPoint2⟩ +instance [Entailment.HasAxiomT 𝓢] : Entailment.HasAxiomGeach ⟨0, 0, 1, 0⟩ 𝓢 := ⟨axiomT⟩ +instance [Entailment.HasAxiomB 𝓢] : Entailment.HasAxiomGeach ⟨0, 1, 0, 1⟩ 𝓢 := ⟨axiomB⟩ +instance [Entailment.HasAxiomD 𝓢] : Entailment.HasAxiomGeach ⟨0, 0, 1, 1⟩ 𝓢 := ⟨axiomD⟩ +instance [Entailment.HasAxiomFour 𝓢] : Entailment.HasAxiomGeach ⟨0, 2, 1, 0⟩ 𝓢 := ⟨axiomFour⟩ +instance [Entailment.HasAxiomFourN n 𝓢] : HasAxiomGeach ⟨0, n + 1, n, 0⟩ 𝓢 := ⟨axiomFourN⟩ +instance [Entailment.HasAxiomFive 𝓢] : Entailment.HasAxiomGeach ⟨1, 1, 0, 1⟩ 𝓢 := ⟨axiomFive⟩ +instance [Entailment.HasAxiomTc 𝓢] : Entailment.HasAxiomGeach ⟨0, 1, 0, 0⟩ 𝓢 := ⟨axiomTc⟩ +instance [Entailment.HasAxiomPoint2 𝓢] : Entailment.HasAxiomGeach ⟨1, 1, 1, 1⟩ 𝓢 := ⟨axiomPoint2⟩ variable [HasAxiomGeach g 𝓢] -def axiomGeach : 𝓢 ⊢! ◇^[g.i](□^[g.m]φ) ➝ □^[g.j](◇^[g.n]φ) := HasAxiomGeach.Geach _ +def axiomGeach : 𝓢 ⊢! ◇^[g.i](□^[g.m]φ) ➝ □^[g.j](◇^[g.n]φ) := HasAxiomGeach.Geach @[simp] lemma axiomGeach! : 𝓢 ⊢ ◇^[g.i](□^[g.m]φ) ➝ □^[g.j](◇^[g.n]φ) := ⟨axiomGeach⟩ variable [Entailment.Minimal 𝓢] -instance (Γ : FiniteContext F 𝓢) : HasAxiomGeach g Γ := ⟨fun _ ↦ FiniteContext.of axiomGeach⟩ -instance (Γ : Context F 𝓢) : HasAxiomGeach g Γ := ⟨fun _ ↦ Context.of axiomGeach⟩ +instance (Γ : FiniteContext F 𝓢) : HasAxiomGeach g Γ := ⟨FiniteContext.of axiomGeach⟩ +instance (Γ : Context F 𝓢) : HasAxiomGeach g Γ := ⟨Context.of axiomGeach⟩ end HasAxiomGeach diff --git a/Foundation/Modal/Entailment/EM.lean b/Foundation/Modal/Entailment/EM.lean index 9254e0991..2ba4f4ae4 100644 --- a/Foundation/Modal/Entailment/EM.lean +++ b/Foundation/Modal/Entailment/EM.lean @@ -24,7 +24,8 @@ instance [Entailment.EM 𝓢] : Entailment.RM 𝓢 := ⟨by ⟩ instance [Entailment.E 𝓢] [Entailment.RM 𝓢] : Entailment.EM 𝓢 where - M φ ψ := by + M := by + intro φ ψ; apply CK_of_C_of_C; . apply rm; exact and₁; . apply rm; exact and₂; diff --git a/Foundation/Modal/Entailment/EMC.lean b/Foundation/Modal/Entailment/EMC.lean index 3f5cdad6c..e2d35b266 100644 --- a/Foundation/Modal/Entailment/EMC.lean +++ b/Foundation/Modal/Entailment/EMC.lean @@ -12,7 +12,7 @@ variable {S F : Type*} [BasicModalLogicalConnective F] [DecidableEq F] [Entailme variable {𝓢 : S} instance [Entailment.EMC 𝓢] : Entailment.HasAxiomK 𝓢 where - K φ ψ := by + K {φ ψ} := by haveI h₁ : 𝓢 ⊢! (□(φ ➝ ψ) ⋏ □φ) ➝ □((φ ➝ ψ) ⋏ φ) := axiomC; haveI h₂ : 𝓢 ⊢! ((φ ➝ ψ) ⋏ φ) ➝ ψ := C_trans CKK innerMDP haveI h₃ : 𝓢 ⊢! □((φ ➝ ψ) ⋏ φ) ➝ □ψ := rm h₂; diff --git a/Foundation/Modal/Entailment/ET.lean b/Foundation/Modal/Entailment/ET.lean index 80a2f24c8..d4e66f0c3 100644 --- a/Foundation/Modal/Entailment/ET.lean +++ b/Foundation/Modal/Entailment/ET.lean @@ -20,7 +20,7 @@ lemma diabot : 𝓢 ⊢ ◇⊤ := ⟨diabot!⟩ namespace ET -instance : Entailment.HasAxiomD 𝓢 := ⟨fun _ ↦ C_trans axiomT diaTc⟩ +instance : Entailment.HasAxiomD 𝓢 := ⟨C_trans axiomT diaTc⟩ instance : Entailment.ED 𝓢 where diff --git a/Foundation/Modal/Entailment/ET5.lean b/Foundation/Modal/Entailment/ET5.lean index afec71f2f..effc8c4fa 100644 --- a/Foundation/Modal/Entailment/ET5.lean +++ b/Foundation/Modal/Entailment/ET5.lean @@ -22,15 +22,15 @@ variable [DecidableEq F] namespace ET5 -instance : Entailment.HasAxiomB 𝓢 := ⟨fun _ ↦ C_trans diaTc axiomFive⟩ +instance : Entailment.HasAxiomB 𝓢 := ⟨C_trans diaTc axiomFive⟩ instance : Entailment.ETB 𝓢 where instance : Entailment.EN 𝓢 where -instance : Entailment.HasAxiomPoint2 𝓢 := ⟨fun _ ↦ C_trans (C_trans axiomFiveDual! axiomT) axiomB⟩ +instance : Entailment.HasAxiomPoint2 𝓢 := ⟨C_trans (C_trans axiomFiveDual! axiomT) axiomB⟩ -instance : Entailment.HasAxiomFour 𝓢 := ⟨fun _ ↦ C_trans (C_trans axiomTDual! axiomFive) (K_left $ re $ K_intro axiomFiveDual! axiomTDual!)⟩ +instance : Entailment.HasAxiomFour 𝓢 := ⟨C_trans (C_trans axiomTDual! axiomFive) (K_left $ re $ K_intro axiomFiveDual! axiomTDual!)⟩ end ET5 diff --git a/Foundation/Modal/Entailment/GL.lean b/Foundation/Modal/Entailment/GL.lean index e1c5569f1..22faf3ff9 100644 --- a/Foundation/Modal/Entailment/GL.lean +++ b/Foundation/Modal/Entailment/GL.lean @@ -31,7 +31,7 @@ namespace GL variable {φ ψ : F} -instance : HasAxiomZ 𝓢 := ⟨fun _ ↦ C_trans axiomL implyK⟩ +instance : HasAxiomZ 𝓢 := ⟨C_trans axiomL implyK⟩ protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := by dsimp [Axioms.Four]; @@ -41,14 +41,14 @@ protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := by exact K_intro (FiniteContext.byAxm) (K_left (ψ := □□φ) $ FiniteContext.byAxm); have : 𝓢 ⊢! φ ➝ (□⊡φ ➝ ⊡φ) := C_trans this (CCC_of_C_left BoxBoxdot_BoxDotbox); exact C_trans (C_trans (implyBoxDistribute' this) axiomL) (implyBoxDistribute' $ and₂); -instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ GL.axiomFour⟩ +instance : HasAxiomFour 𝓢 := ⟨GL.axiomFour⟩ instance : Entailment.K4 𝓢 where protected def axiomHen : 𝓢 ⊢! Axioms.Hen φ := C_trans (implyBoxDistribute' and₁) axiomL -instance : HasAxiomHen 𝓢 := ⟨fun _ ↦ GL.axiomHen⟩ +instance : HasAxiomHen 𝓢 := ⟨GL.axiomHen⟩ protected def axiomZ : 𝓢 ⊢! Axioms.Z φ := C_trans axiomL implyK -instance : HasAxiomZ 𝓢 := ⟨fun _ ↦ GL.axiomZ⟩ +instance : HasAxiomZ 𝓢 := ⟨GL.axiomZ⟩ end GL diff --git a/Foundation/Modal/Entailment/Grz.lean b/Foundation/Modal/Entailment/Grz.lean index f93fa4443..a89102e35 100644 --- a/Foundation/Modal/Entailment/Grz.lean +++ b/Foundation/Modal/Entailment/Grz.lean @@ -16,14 +16,14 @@ namespace Grz noncomputable def lemma_axiomFour_axiomT : 𝓢 ⊢! □φ ➝ (φ ⋏ (□φ ➝ □□φ)) := C_trans (lemma_Grz₁ (φ := φ)) axiomGrz protected noncomputable def axiomFour : 𝓢 ⊢! □φ ➝ □□φ := C_of_CC $ C_trans lemma_axiomFour_axiomT and₂ -noncomputable instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ Grz.axiomFour⟩ +noncomputable instance : HasAxiomFour 𝓢 := ⟨Grz.axiomFour⟩ protected noncomputable def axiomT : 𝓢 ⊢! □φ ➝ φ := C_trans lemma_axiomFour_axiomT and₁ -noncomputable instance : HasAxiomT 𝓢 := ⟨fun _ ↦ Grz.axiomT⟩ +noncomputable instance : HasAxiomT 𝓢 := ⟨Grz.axiomT⟩ noncomputable instance : Entailment.S4 𝓢 where -instance : HasAxiomDum 𝓢 := ⟨fun _ ↦ C_trans axiomGrz implyK⟩ +instance : HasAxiomDum 𝓢 := ⟨C_trans axiomGrz implyK⟩ end Grz diff --git a/Foundation/Modal/Entailment/K.lean b/Foundation/Modal/Entailment/K.lean index 46d8ef390..a9529923b 100644 --- a/Foundation/Modal/Entailment/K.lean +++ b/Foundation/Modal/Entailment/K.lean @@ -107,7 +107,7 @@ def collect_boxItr_and : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ ➝ □^[n](φ ⋏ ψ def collect_box_and : 𝓢 ⊢! □φ ⋏ □ψ ➝ □(φ ⋏ ψ) := collect_boxItr_and (n := 1) @[simp] lemma collect_box_and! : 𝓢 ⊢ □φ ⋏ □ψ ➝ □(φ ⋏ ψ) := ⟨collect_box_and⟩ -instance : Entailment.HasAxiomC 𝓢 := ⟨λ _ _ => collect_box_and⟩ +instance : Entailment.HasAxiomC 𝓢 := ⟨collect_box_and⟩ def collect_boxItr_and' (h : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ) : 𝓢 ⊢! □^[n](φ ⋏ ψ) := collect_boxItr_and ⨀ h lemma collect_boxItr_and'! (h : 𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ) : 𝓢 ⊢ □^[n](φ ⋏ ψ) := ⟨collect_boxItr_and' h.some⟩ @@ -213,7 +213,7 @@ lemma distribute_boxItr_and'! (d : 𝓢 ⊢ □^[n](φ ⋏ ψ)) : 𝓢 ⊢ □^[ def distribute_box_and' (h : 𝓢 ⊢! □(φ ⋏ ψ)) : 𝓢 ⊢! □φ ⋏ □ψ := distribute_boxItr_and' (n := 1) h lemma distribute_box_and'! (d : 𝓢 ⊢ □(φ ⋏ ψ)) : 𝓢 ⊢ □φ ⋏ □ψ := ⟨distribute_box_and' d.some⟩ -instance : Entailment.HasAxiomM 𝓢 := ⟨λ _ _ => distribute_box_and⟩ +instance : Entailment.HasAxiomM 𝓢 := ⟨distribute_box_and⟩ def boxdotAxiomK : 𝓢 ⊢! ⊡(φ ➝ ψ) ➝ (⊡φ ➝ ⊡ψ) := by diff --git a/Foundation/Modal/Entailment/K4Loeb.lean b/Foundation/Modal/Entailment/K4Loeb.lean index 3c3ec805e..d13d1e849 100644 --- a/Foundation/Modal/Entailment/K4Loeb.lean +++ b/Foundation/Modal/Entailment/K4Loeb.lean @@ -29,7 +29,7 @@ protected def axiomL : 𝓢 ⊢! Axioms.L φ := by nth_rw 2 [←e]; apply deduct'; apply deduct; exact d₂ ⨀ (d₁ ⨀ ((of d₃) ⨀ (FiniteContext.byAxm))); exact loeb this; -instance : HasAxiomL 𝓢 := ⟨fun _ ↦ K4Loeb.axiomL⟩ +instance : HasAxiomL 𝓢 := ⟨K4Loeb.axiomL⟩ end K4Loeb diff --git a/Foundation/Modal/Entailment/KP.lean b/Foundation/Modal/Entailment/KP.lean index 01a138da8..c13e6630a 100644 --- a/Foundation/Modal/Entailment/KP.lean +++ b/Foundation/Modal/Entailment/KP.lean @@ -20,7 +20,7 @@ protected def axiomD [HasDiaDuality 𝓢] : 𝓢 ⊢! Axioms.D φ := by have : 𝓢 ⊢! □φ ➝ (∼□⊥ ➝ ∼□(∼φ)) := C_trans this CCCNN; have : 𝓢 ⊢! □φ ➝ ∼□(∼φ) := C_swap this ⨀ axiomP; exact C_trans this (K_right diaDuality); -instance : HasAxiomD 𝓢 := ⟨fun _ ↦ KP.axiomD⟩ +instance : HasAxiomD 𝓢 := ⟨KP.axiomD⟩ end KP diff --git a/Foundation/Modal/Entailment/KT.lean b/Foundation/Modal/Entailment/KT.lean index 9a4ff6834..5a0cb2caa 100644 --- a/Foundation/Modal/Entailment/KT.lean +++ b/Foundation/Modal/Entailment/KT.lean @@ -18,7 +18,7 @@ namespace KT' variable [Entailment.KT' 𝓢] -instance : HasAxiomT 𝓢 := ⟨fun _ ↦ C_trans box_dni (C_of_CNN (C_trans diaTc diaDuality_mp))⟩ +instance : HasAxiomT 𝓢 := ⟨C_trans box_dni (C_of_CNN (C_trans diaTc diaDuality_mp))⟩ instance : Entailment.KT 𝓢 where instance : Entailment.KP 𝓢 where instance : Entailment.KD 𝓢 where diff --git a/Foundation/Modal/Entailment/KTc.lean b/Foundation/Modal/Entailment/KTc.lean index d851629e1..c5a1cfc02 100644 --- a/Foundation/Modal/Entailment/KTc.lean +++ b/Foundation/Modal/Entailment/KTc.lean @@ -16,16 +16,16 @@ namespace KTc variable [Entailment.KTc 𝓢] protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := axiomTc -instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ KTc.axiomFour⟩ +instance : HasAxiomFour 𝓢 := ⟨KTc.axiomFour⟩ protected def axiomFive : 𝓢 ⊢! ◇φ ➝ □◇φ := axiomTc -instance : HasAxiomFive 𝓢 := ⟨fun _ ↦ KTc.axiomFive⟩ +instance : HasAxiomFive 𝓢 := ⟨KTc.axiomFive⟩ protected def axiomDiaT : 𝓢 ⊢! ◇φ ➝ φ := by apply C_trans (K_left diaDuality) ?_; apply CN_of_CN_left; exact axiomTc; -instance : HasAxiomDiaT 𝓢 := ⟨fun _ ↦ KTc.axiomDiaT⟩ +instance : HasAxiomDiaT 𝓢 := ⟨KTc.axiomDiaT⟩ end KTc @@ -35,7 +35,7 @@ namespace KTc' variable [Entailment.KTc' 𝓢] protected def axiomTc : 𝓢 ⊢! φ ➝ □φ := C_trans (C_of_CNN (C_trans (K_right diaDuality) diaT)) box_dne -instance : HasAxiomTc 𝓢 := ⟨fun _ ↦ KTc'.axiomTc⟩ +instance : HasAxiomTc 𝓢 := ⟨KTc'.axiomTc⟩ end KTc' diff --git a/Foundation/Modal/Entailment/S5Grz.lean b/Foundation/Modal/Entailment/S5Grz.lean index 47794937c..3812c995a 100644 --- a/Foundation/Modal/Entailment/S5Grz.lean +++ b/Foundation/Modal/Entailment/S5Grz.lean @@ -25,7 +25,7 @@ protected noncomputable def S5Grz.diaT : 𝓢 ⊢! ◇φ ➝ φ := by have : 𝓢 ⊢! □◇φ ➝ φ := C_trans this axiomGrz; exact C_trans axiomFive this; -noncomputable instance : HasAxiomDiaT 𝓢 := ⟨fun _ ↦ S5Grz.diaT⟩ +noncomputable instance : HasAxiomDiaT 𝓢 := ⟨S5Grz.diaT⟩ noncomputable instance : Entailment.KTc' 𝓢 where end LO.Modal.Entailment diff --git a/Foundation/Modal/Entailment/Ver.lean b/Foundation/Modal/Entailment/Ver.lean index af49a6433..71f69edfd 100644 --- a/Foundation/Modal/Entailment/Ver.lean +++ b/Foundation/Modal/Entailment/Ver.lean @@ -26,10 +26,10 @@ lemma bot_of_dia'! (h : 𝓢 ⊢ ◇φ) : 𝓢 ⊢ ⊥ := ⟨bot_of_dia' h.some namespace Ver protected def axiomTc : 𝓢 ⊢! Axioms.Tc φ := C_of_conseq axiomVer -instance : HasAxiomTc 𝓢 := ⟨fun _ ↦ Ver.axiomTc⟩ +instance : HasAxiomTc 𝓢 := ⟨Ver.axiomTc⟩ protected def axiomL : 𝓢 ⊢! Axioms.L φ := C_of_conseq axiomVer -instance : HasAxiomL 𝓢 := ⟨fun _ ↦ Ver.axiomL⟩ +instance : HasAxiomL 𝓢 := ⟨Ver.axiomL⟩ end Ver diff --git a/Foundation/Modal/Hilbert/Normal/Alt.lean b/Foundation/Modal/Hilbert/Normal/Alt.lean index 88170c453..5a812e39a 100644 --- a/Foundation/Modal/Hilbert/Normal/Alt.lean +++ b/Foundation/Modal/Hilbert/Normal/Alt.lean @@ -110,7 +110,7 @@ inductive buildAxioms.Symbol | WeakPoint2 | WeakPoint3 | Z -deriving DecidableEq +deriving DecidableEq, Repr def buildAxioms.Symbol.arity : buildAxioms.Symbol → ℕ | K @@ -164,80 +164,143 @@ lemma mem_axiomK (h : .K ∈ l := by decide) : Axioms.K φ ψ ∈ buildAxioms α simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; grind; -lemma mem_axiomD (h : .D ∈ l := by decide) : Axioms.D φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomT (h : .T ∈ l := by decide) : Axioms.T φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomB (h : .B ∈ l := by decide) : Axioms.B φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomFour (h : .Four ∈ l := by decide) : Axioms.Four φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomFive (h : .Five ∈ l := by decide) : Axioms.Five φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomPoint2 (h : .Point2 ∈ l := by decide) : Axioms.Point2 φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomPoint3 (h : .Point3 ∈ l := by decide) : Axioms.Point3 φ ψ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomGrz (h : .Grz ∈ l := by decide) : Axioms.Grz φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomL (h : .L ∈ l := by decide) : Axioms.L φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomP (h : .P ∈ l := by decide) : Axioms.P ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomMcK (h : .McK ∈ l := by decide) : Axioms.McK φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - -lemma mem_axiomTc (h : .Tc ∈ l := by decide) : Axioms.Tc φ ∈ buildAxioms α l := by - simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq]; - grind; - +/- attribute [simp, grind <=] - mem_axiomK - mem_axiomD - mem_axiomT mem_axiomB - mem_axiomFour + mem_axiomC4 + mem_axiomCD + mem_axiomD + mem_axiomDum mem_axiomFive - mem_axiomPoint2 - mem_axiomPoint3 + mem_axiomFour mem_axiomGrz - mem_axiomP + mem_axiomH + mem_axiomHen + mem_axiomK mem_axiomL mem_axiomMcK + mem_axiomMk + mem_axiomP + mem_axiomPoint2 + mem_axiomPoint3 + mem_axiomPoint4 + mem_axiomT mem_axiomTc + mem_axiomVer + mem_axiomWeakPoint2 + mem_axiomWeakPoint3 + mem_axiomZ +-/ end buildAxioms end -end Hilbert.Normal2 +section +open Lean Elab Command Term Meta Qq +open buildAxioms + +local elab "#defineModalLogic" name:ident axioms:term : command => do + let logicName := `_root_.LO.Modal |>.append name.getId + + -- let axioms ← axioms.getElems.mapM $ λ stx => pure (Lean.mkIdentFrom stx stx.getId) + + dbg_trace logicName + dbg_trace axioms + + elabCommand (←`(protected abbrev $(mkIdent logicName) (α) := Hilbert.Normal2 $ Hilbert.Normal2.buildAxioms α $axioms)) + -- elabCommand (←`(#eval String.toSlice $axioms)) + + /- + if axioms.contains (mkIdent `K) then elabCommand (←`( + instance {α} : Entailment.HasAxiomK ($(mkIdent logicName) α) := ⟨by intros; constructor; apply Hilbert.Normal2.axm $ mem_axiomK⟩ + )) + -/ + + /- + if axioms.contains (mkIdent `D) then + elabCommand (←`(instance {α} : Entailment.HasAxiomD ($logicName α) where D φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `T) then + elabCommand (←`(instance {α} : Entailment.HasAxiomT ($logicName α) where T φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `B) then + elabCommand (←`(instance {α} : Entailment.HasAxiomB ($logicName α) where B φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `Four) then + elabCommand (←`(instance {α} : Entailment.HasAxiomFour ($logicName α) where Four φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `Five) then + elabCommand (←`(instance {α} : Entailment.HasAxiomFive ($logicName α) where Five φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `Point2) then + elabCommand (←`(instance {α} : Entailment.HasAxiomPoint2 ($logicName α) where Point2 φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `Point3) then + elabCommand (←`(instance {α} : Entailment.HasAxiomPoint3 ($logicName α) where Point3 φ ψ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `Grz) then + elabCommand (←`(instance {α} : Entailment.HasAxiomGrz ($logicName α) where Grz φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `L) then + elabCommand (←`(instance {α} : Entailment.HasAxiomL ($logicName α) where L φ := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `P) then + elabCommand (←`(instance {α} : Entailment.HasAxiomP ($logicName α) where P := by constructor; apply Hilbert.Normal2.axm; simp)) + if axioms.contains (mkIdent `McK) then + elabCommand (←`(instance {α} : Entailment.HasAxiomMcK ($logicName α) where McK φ := by constructor; apply Hilbert.Normal2.axm; simp)) + -/ -section +open Hilbert.Normal2.buildAxioms.Symbol -open Lean in +whatsnew in +#defineModalLogic Dum [.K, .T, .Four, .Dum] +#defineModalLogic DumPoint2 [.K, .T, .Four, .Dum, .Point2] +#defineModalLogic DumPoint3 [.K, .T, .Four, .Dum, .Point3] +#defineModalLogic GL [.K, .L] +#defineModalLogic GLPoint2 [.K, .L, .WeakPoint2] +#defineModalLogic GLPoint3 [.K, .L, .WeakPoint3] +#defineModalLogic Grz [.K, .Grz] +#defineModalLogic GrzPoint2 [.K, .Grz, .Point2] +#defineModalLogic GrzPoint3 [.K, .Grz, .Point3] +#defineModalLogic K [.K] +#defineModalLogic K4 [.K, .Four] +#defineModalLogic K45 [.K, .Four, .Five] +#defineModalLogic K4Hen [.K, .Four, .Hen] +#defineModalLogic K4McK [.K, .Four, .McK] +#defineModalLogic K4Point2 [.K, .Four, .WeakPoint2] +#defineModalLogic K4Point2Z [.K, .Four, .WeakPoint2, .Z] +#defineModalLogic K4Point3 [.K, .Four, .WeakPoint3] +#defineModalLogic K4Point3Z [.K, .Four, .WeakPoint3, .Z] +#defineModalLogic K4Z [.K, .Four, .Z] +#defineModalLogic K5 [.K, .Five] +#defineModalLogic KB [.K, .B] +#defineModalLogic KB4 [.K, .B, .Four] +#defineModalLogic KB5 [.K, .B, .Five] +#defineModalLogic KD [.K, .D] +#defineModalLogic KD4 [.K, .D, .Four] +#defineModalLogic KD45 [.K, .D, .Four, .Five] +#defineModalLogic KD4Point3Z [.K, .D, .Four, .Point3, .Z] +#defineModalLogic KD5 [.K, .D, .Five] +#defineModalLogic KDB [.K, .D, .B] +#defineModalLogic KHen [.K, .Hen] +#defineModalLogic KP [.K, .P] +#defineModalLogic KT [.K, .T] +#defineModalLogic KT4B [.K, .T, .Four, .B] +#defineModalLogic KTB [.K, .T, .B] +#defineModalLogic KTc [.K, .Tc] +#defineModalLogic KTMk [.K, .T, .Mk] +#defineModalLogic N [] +#defineModalLogic NP [.P] +#defineModalLogic S4 [.K, .T, .Four] +#defineModalLogic S4H [.K, .T, .Four, .H] +#defineModalLogic S4McK [.K, .T, .Four, .McK] +#defineModalLogic S4Point2 [.K, .T, .Four, .Point2] +#defineModalLogic S4Point2McK [.K, .T, .Four, .Point2, .McK] +#defineModalLogic S4Point3 [.K, .T, .Four, .Point3] +#defineModalLogic S4Point3McK [.K, .T, .Four, .Point3, .McK] +#defineModalLogic S4Point4 [.K, .T, .Four, .Point4] +#defineModalLogic S4Point4McK [.K, .T, .Four, .Point4, .McK] +#defineModalLogic S5 [.K, .T, .Five] +#defineModalLogic S5Grz [.K, .T, .Five, .Grz] +#defineModalLogic Triv [.K, .T, .Tc] +#defineModalLogic Ver [.K, .Ver] + +/- +open Lean macro "defineModalLogic" name:ident "[" xs:ident,* "]" : command => do let xs ← xs.getElems.mapM $ λ stx => pure (Lean.mkIdentFrom stx stx.getId) @@ -301,6 +364,7 @@ macro "defineModalLogic" name:ident "[" xs:ident,* "]" : command => do namespace $logicName + $instHasAxiomK $instHasAxiomT $instHasAxiomD @@ -426,9 +490,12 @@ noncomputable instance [DecidableEq α] [Modal.K4McK' α ⪯ Hilbert.Normal2 Ax K _ _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomK! |>.some Four _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomFour! |>.some McK _ := Entailment.WeakerThan.pbl (𝓢 := Modal.K4McK' α) axiomMcK! |>.some +-/ end +end Hilbert.Normal2 + end LO.Modal end diff --git a/Foundation/Modal/Hilbert/WithHenkin/Basic.lean b/Foundation/Modal/Hilbert/WithHenkin/Basic.lean index 7a861043d..e8486da43 100644 --- a/Foundation/Modal/Hilbert/WithHenkin/Basic.lean +++ b/Foundation/Modal/Hilbert/WithHenkin/Basic.lean @@ -107,7 +107,7 @@ section variable [DecidableEq α] instance instHasAxiomK [Ax.HasK] : Entailment.HasAxiomK (Hilbert.WithHenkin Ax) where - K φ ψ := by + K := by constructor; simpa [HasK.ne_pq] using Hilbert.WithHenkin.axm (φ := Axioms.K (.atom (HasK.p Ax)) (.atom (HasK.q Ax)))