From d30eb5bdd08cd85b8154ba495d5bb1787bc99ee7 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 6 Dec 2024 11:08:48 +0900 Subject: [PATCH] hilbert emulation --- LabelledSystem/Gentzen/Basic.lean | 112 +++++++++++++++------------- LabelledSystem/Gentzen/Hilbert.lean | 71 ++++++++++++++++++ 2 files changed, 132 insertions(+), 51 deletions(-) create mode 100644 LabelledSystem/Gentzen/Hilbert.lean diff --git a/LabelledSystem/Gentzen/Basic.lean b/LabelledSystem/Gentzen/Basic.lean index 80b789c..73e748e 100644 --- a/LabelledSystem/Gentzen/Basic.lean +++ b/LabelledSystem/Gentzen/Basic.lean @@ -17,10 +17,6 @@ namespace SequentPart @[simp] def isFreshLabel (x : Label) (Γ : SequentPart) : Prop := (x ∉ Γ.fmls.map LabelledFormula.label) ∧ (∀ y, (x, y) ∉ Γ.rels) ∧ (∀ y, (y, x) ∉ Γ.rels) -abbrev replaceLabel (σ : Label → Label) (Γ : SequentPart) : SequentPart := - ⟨Γ.fmls.map (LabelledFormula.labelReplace σ), Γ.rels.map (LabelTerm.replace σ)⟩ -notation Γ "⟦" σ "⟧" => SequentPart.replaceLabel σ Γ - /- instance : Decidable (isFreshLabel Γ x) := by simp [isFreshLabel]; @@ -34,6 +30,14 @@ lemma not_include_relTerm_of_isFreshLabel₁ (h : Γ.isFreshLabel x) : ∀ y, (x lemma not_include_relTerm_of_isFreshLabel₂ (h : Γ.isFreshLabel x) : ∀ y, (y, x) ∉ Γ.rels := by have := h.2.2; aesop; + +abbrev replaceLabel (σ : Label → Label) (Γ : SequentPart) : SequentPart := + ⟨Γ.fmls.map (LabelledFormula.labelReplace σ), Γ.rels.map (LabelTerm.replace σ)⟩ +notation Γ "⟦" σ "⟧" => SequentPart.replaceLabel σ Γ + +abbrev add (Γ Δ : SequentPart) : SequentPart := ⟨Γ.fmls + Δ.fmls, Γ.rels + Δ.rels⟩ +instance : Add SequentPart := ⟨add⟩ + end SequentPart @@ -59,8 +63,8 @@ end Sequent inductive Derivation : Sequent → Type _ -| axA {Γ Δ : SequentPart} {x} {a} : Derivation (⟨(x ∶ atom a) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ Δ.fmls, Δ.rels⟩) -| axBot {Γ Δ : SequentPart} {x} : Derivation (⟨(x ∶ ⊥) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ) +| initAtom {Γ Δ : SequentPart} {x} {a} : Derivation (⟨(x ∶ atom a) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ Δ.fmls, Δ.rels⟩) +| initBot {Γ Δ : SequentPart} {x} : Derivation (⟨(x ∶ ⊥) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ) | impL {Γ Δ : SequentPart} {x} {φ ψ} : Derivation (Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) → Derivation (⟨(x ∶ ψ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ) → @@ -77,17 +81,17 @@ inductive Derivation : Sequent → Type _ Derivation (Γ ⟹ ⟨(x ∶ □φ) ::ₘ Δ.fmls, Δ.rels⟩) prefix:40 "⊢ᵍ " => Derivation -export Derivation (axA axBot impL impR boxL boxR) +export Derivation (initAtom initBot impL impR boxL boxR) abbrev Derivable (S : Sequent) : Prop := Nonempty (⊢ᵍ S) prefix:40 "⊢ᵍ! " => Derivable -section height +section Height def Derivation.height {S : Sequent} : ⊢ᵍ S → ℕ - | axA => 1 - | axBot => 1 + | initAtom => 1 + | initBot => 1 | impL d₁ d₂ => max d₁.height d₂.height + 1 | impR d => d.height + 1 | boxL d => d.height + 1 @@ -103,15 +107,21 @@ def DerivationWithHeight.ofDerivation (d : ⊢ᵍ S) : ⊢ᵍ[d.height] S := ⟨ abbrev DerivableWithHeight (S : Sequent) (h : ℕ) : Prop := Nonempty (⊢ᵍ[h] S) notation:40 "⊢ᵍ[ " h " ]! " S => DerivableWithHeight S h -end height +end Height + + +variable {Γ Γ₁ Γ₂ Δ Δ₁ Δ₂ : SequentPart} -variable {Γ Δ : SequentPart} +section -def axF : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) := by +end + + +def initFml : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) := by induction φ using Formula.rec' generalizing Γ Δ x with - | hatom a => exact axA - | hfalsum => exact axBot + | hatom a => exact initAtom + | hfalsum => exact initBot | himp φ ψ ihφ ihψ => apply impR; simpa [Multiset.cons_swap] using impL ihφ ihψ; @@ -121,68 +131,68 @@ def axF : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ φ) :: apply boxL; simpa [Multiset.cons_swap] using ih (Γ := ⟨(x ∶ □φ) ::ₘ Γ.fmls, _ ::ₘ Γ.rels⟩); +def initFml' (x φ) (hΓ : (x ∶ φ) ∈ Γ.fmls) (hΔ : (x ∶ φ) ∈ Δ.fmls) : ⊢ᵍ Γ ⟹ Δ := by + suffices ⊢ᵍ (⟨Γ.fmls, Γ.rels⟩ ⟹ ⟨Δ.fmls, Δ.rels⟩) by simpa; + have eΓ := Multiset.cons_erase hΓ; + have eΔ := Multiset.cons_erase hΔ; + rw [←eΓ, ←eΔ]; + simpa using initFml (Γ := ⟨Γ.fmls.erase (x ∶ φ), _⟩) (Δ := ⟨Δ.fmls.erase (x ∶ φ), _⟩); -def axiomK : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ □(φ ➝ ψ) ➝ □φ ➝ □ψ}, ∅⟩⟩ := by - letI y : Label := x + 1; - apply impR (Δ := ⟨_, _⟩); - apply impR; - apply boxR (y := y) (by simp [y]) (by simp) (by simp); - suffices ⊢ᵍ (⟨(x ∶ □φ) ::ₘ {x ∶ □(φ ➝ ψ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by simpa; - apply boxL (Γ := ⟨_, _⟩); - suffices ⊢ᵍ (⟨(x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ) ::ₘ {(x ∶ □φ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by - have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (x ∶ □φ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □(φ ➝ ψ)} := by sorry; - simpa [e]; - apply boxL (x := x) (φ := φ ➝ ψ) (Γ := ⟨{y ∶ φ, x ∶ □φ}, _⟩); - suffices ⊢ᵍ (⟨(y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by - have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ ➝ ψ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)} := by sorry; - simpa [e]; - apply impL (Γ := ⟨_, _⟩); - . simpa using axF (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); - . simpa using axF (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); - -section replaceLabel +section ReplaceLabel -def replaceLabel (d : ⊢ᵍ[h] Γ ⟹ Δ) (σ : Label → Label) : ⊢ᵍ[h] Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := by sorry; +def replaceLabelₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) (σ : Label → Label) : ⊢ᵍ[h] Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := by sorry; -def replaceLabel' (d : ⊢ᵍ Γ ⟹ Δ) (σ : Label → Label) : ⊢ᵍ Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := replaceLabel (.ofDerivation d) σ |>.drv +def replaceLabel (d : ⊢ᵍ Γ ⟹ Δ) (σ : Label → Label) : ⊢ᵍ Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := replaceLabelₕ (.ofDerivation d) σ |>.drv -end replaceLabel +end ReplaceLabel section Weakening -def wkFmlL (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := by sorry +def wkFmlLₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := by sorry -def wkFmlL' (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := wkFmlL (d := .ofDerivation d) |>.drv +def wkFmlL (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := wkFmlLₕ (d := .ofDerivation d) |>.drv -def wkRelL (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] ⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ := by sorry +def wkRelLₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] ⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ := by sorry -def wkRelL' (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ ⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ := wkRelL (d := .ofDerivation d) |>.drv +def wkRelL (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ ⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ := wkRelLₕ (d := .ofDerivation d) |>.drv -def wkFmlR (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩ := by sorry +def wkFmlRₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩ := by sorry -def wkFmlR' (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩ := wkFmlR (d := .ofDerivation d) |>.drv +def wkFmlR (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩ := wkFmlRₕ (d := .ofDerivation d) |>.drv -def wkRelR (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] Γ ⟹ ⟨Δ.fmls, (x, y) ::ₘ Δ.rels⟩ := by sorry +def wkRelRₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] Γ ⟹ ⟨Δ.fmls, (x, y) ::ₘ Δ.rels⟩ := by sorry -def wkRelR' (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ Γ ⟹ ⟨Δ.fmls, (x, y) ::ₘ Δ.rels⟩ := wkRelR (d := .ofDerivation d) |>.drv +def wkRelR (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ Γ ⟹ ⟨Δ.fmls, (x, y) ::ₘ Δ.rels⟩ := wkRelRₕ (d := .ofDerivation d) |>.drv end Weakening -def necessitation (d : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ φ}, ∅⟩⟩) : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ □φ}, ∅⟩⟩ := by - letI y : Label := x + 1; - apply boxR (Δ := ⟨∅, ∅⟩) (y := y) (by simp [y]) (by simp) (by simp); - apply wkRelL'; - simpa [SequentPart.replaceLabel, LabelledFormula.labelReplace, LabelReplace.specific] using replaceLabel' d (x ⧸ y); +section Inv -end Gentzen +def implyRInvₕ (d : ⊢ᵍ[h] (Γ ⟹ ⟨(x ∶ φ ➝ ψ) ::ₘ Δ.fmls, Δ.rels⟩)) : ⊢ᵍ[h] (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ Δ.fmls, Δ.rels⟩) := by sorry + +def implyRInv (d : ⊢ᵍ (Γ ⟹ ⟨(x ∶ φ ➝ ψ) ::ₘ Δ.fmls, Δ.rels⟩)) : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ Δ.fmls, Δ.rels⟩) := implyRInvₕ (d := .ofDerivation d) |>.drv + +end Inv +section Cut + +def cutRel (d₁ : ⊢ᵍ Γ₁ ⟹ ⟨Δ₁.fmls, (x, y) ::ₘ Δ₁.rels⟩) (d₂ : ⊢ᵍ ⟨Γ₂.fmls, (x, y) ::ₘ Γ₂.rels⟩ ⟹ Δ₂) : ⊢ᵍ (Γ₁ + Γ₂) ⟹ (Δ₁ + Δ₂) := by + sorry + +def cutFml (d₁ : ⊢ᵍ Γ₁ ⟹ ⟨(x ∶ φ) ::ₘ Δ₁.fmls, Δ₁.rels⟩) (d₂ : ⊢ᵍ ⟨(x ∶ φ) ::ₘ Γ₂.fmls, Γ₂.rels⟩ ⟹ Δ₂) : ⊢ᵍ (Γ₁ + Γ₂) ⟹ (Δ₁ + Δ₂) := by + sorry + +end Cut + + +end Gentzen end Labelled diff --git a/LabelledSystem/Gentzen/Hilbert.lean b/LabelledSystem/Gentzen/Hilbert.lean new file mode 100644 index 0000000..3228f71 --- /dev/null +++ b/LabelledSystem/Gentzen/Hilbert.lean @@ -0,0 +1,71 @@ +import LabelledSystem.Gentzen.Basic + +namespace LO.Modal.Labelled.Gentzen + +-- def Sequent.ofFormula (φ : Formula ℕ) : Sequent := ⟨∅, ∅⟩ ⟹ ⟨{0 ∶ φ}, ∅⟩ + +variable {x : Label} {φ ψ χ : Formula ℕ} + +def imply₁ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ ➝ ψ ➝ φ}, ∅⟩ := by + apply impR (Δ := ⟨_, _⟩); + apply impR (Δ := ⟨_, _⟩); + have e : (x ∶ ψ) ::ₘ {x ∶ φ} = (x ∶ φ) ::ₘ {x ∶ ψ} := by sorry; + exact initFml' x φ (by simp) (by simp); + +def imply₂ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ}, ∅⟩ := by + apply impR (Δ := ⟨_, _⟩); + apply impR (Δ := ⟨_, _⟩); + apply impR (Δ := ⟨_, _⟩); + rw [Multiset.cons_swap]; + apply impL (Γ := ⟨{x ∶ φ, x ∶ φ ➝ ψ ➝ χ}, _⟩); + . exact initFml' x φ (by simp) (by simp); + . suffices ⊢ᵍ ⟨(x ∶ φ ➝ ψ ➝ χ) ::ₘ {x ∶ ψ, x ∶ φ}, ∅⟩ ⟹ ⟨{x ∶ χ}, ∅⟩ by + have e : (x ∶ ψ) ::ₘ (x ∶ φ) ::ₘ {x ∶ φ ➝ ψ ➝ χ} = (x ∶ φ ➝ ψ ➝ χ) ::ₘ {x ∶ ψ, x ∶ φ} := by sorry; + simpa [e]; + apply impL (Γ := ⟨_, _⟩); + . exact initFml' x φ (by simp) (by simp); + . apply impL (Γ := ⟨_, _⟩); + . exact initFml' x ψ (by simp) (by simp); + . exact initFml' x χ (by simp) (by simp); + +def elimContra : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ (∼ψ ➝ ∼φ) ➝ (φ ➝ ψ)}, ∅⟩ := by + apply impR (Δ := ⟨_, _⟩); + apply impR (Δ := ⟨_, _⟩); + rw [Multiset.cons_swap]; + apply impL (Γ := ⟨{x ∶ φ}, _⟩); + . -- TODO: `⊢ᵍ Γ ⟹ ⟨(x ∶ ∼ψ) ::ₘ {x ∶ ψ}, Δ.rels⟩` + apply impR (Δ := ⟨_, _⟩); + exact initFml' x ψ (by simp) (by simp); + . -- TODO: `⊢ᵍ ⟨(x ∶ ∼φ) ::ₘ {x ∶ φ} :: Γ.fmls, ∅⟩ ⟹ Δ` + apply impL (Γ := ⟨{x ∶ φ}, _⟩); + . exact initFml' x φ (by simp) (by simp); + . exact initBot; + +def axiomK : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ □(φ ➝ ψ) ➝ □φ ➝ □ψ}, ∅⟩ := by + letI y : Label := x + 1; + apply impR (Δ := ⟨_, _⟩); + apply impR; + apply boxR (y := y) (by simp [y]) (by simp) (by simp); + suffices ⊢ᵍ (⟨(x ∶ □φ) ::ₘ {x ∶ □(φ ➝ ψ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by simpa; + apply boxL (Γ := ⟨_, _⟩); + suffices ⊢ᵍ (⟨(x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ) ::ₘ {(x ∶ □φ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by + have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (x ∶ □φ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □(φ ➝ ψ)} := by sorry; + simpa [e]; + apply boxL (Γ := ⟨{y ∶ φ, x ∶ □φ}, _⟩); + suffices ⊢ᵍ (⟨(y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by + have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ ➝ ψ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)} := by sorry; + simpa [e]; + apply impL (Γ := ⟨_, _⟩); + . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); + . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); + +def mdp (d₁ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ ➝ ψ}, ∅⟩) (d₂ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ}, ∅⟩) : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ ψ}, ∅⟩ := by + simpa using cutFml (Δ₁ := ⟨∅, ∅⟩) (Δ₂ := ⟨{x ∶ ψ}, ∅⟩) d₂ $ implyRInv (Δ := ⟨∅, ∅⟩) d₁; + +def necessitation (d : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ}, ∅⟩) : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ □φ}, ∅⟩ := by + letI y : Label := x + 1; + apply boxR (Δ := ⟨∅, ∅⟩) (y := y) (by simp [y]) (by simp) (by simp); + apply wkRelL; + simpa [SequentPart.replaceLabel, LabelledFormula.labelReplace, LabelReplace.specific] using replaceLabel d (x ⧸ y); + +end LO.Modal.Labelled.Gentzen