@@ -7,158 +7,92 @@ public import Foundation.Logic.Calculus
77
88namespace LO.Propositional
99
10- variable {α : Type *}
11-
1210abbrev Sequent (α : Type *) := List (NNFormula α)
1311
14- inductive Derivation (T : Theory α) : Sequent α → Type _
15- | axL (Δ a) : Derivation T (NNFormula.atom a :: NNFormula.natom a :: Δ)
16- | verum (Δ) : Derivation T (⊤ :: Δ)
17- | or {Δ φ ψ} : Derivation T (φ :: ψ :: Δ) → Derivation T (φ ⋎ ψ :: Δ)
18- | and {Δ φ ψ} : Derivation T (φ :: Δ) → Derivation T (ψ :: Δ) → Derivation T (φ ⋏ ψ :: Δ)
19- | wk {Δ Γ} : Derivation T Δ → Δ ⊆ Γ → Derivation T Γ
20- | cut {Δ φ} : Derivation T (φ :: Δ) → Derivation T (∼φ :: Δ) → Derivation T Δ
21- | axm {φ} : φ ∈ T → Derivation T [φ]
12+ inductive Derivation : Sequent α → Type _
13+ | identity (a : α) : Derivation [NNFormula.atom a, NNFormula.natom a]
14+ | cut : Derivation (φ :: Γ) → Derivation (∼φ :: Δ) → Derivation (Γ ++ Δ)
15+ | wk : Derivation Δ → Δ ⊆ Γ → Derivation Γ
16+ | verum : Derivation [⊤]
17+ | or : Derivation (φ :: ψ :: Γ) → Derivation (φ ⋎ ψ :: Γ)
18+ | and : Derivation (φ :: Γ) → Derivation (ψ :: Γ) → Derivation (φ ⋏ ψ :: Γ)
2219
23- instance : OneSided (Theory α) (NNFormula α) := ⟨ Derivation⟩
20+ scoped prefix : 45 "⊢ᴷ " => Derivation
2421
2522namespace Derivation
2623
2724variable {T U : Theory α} {Δ Δ₁ Δ₂ Γ : Sequent α}
2825
29- def length {Δ : Sequent α} : T ⟹ Δ → ℕ
30- | axL _ _ => 0
31- | verum _ => 0
32- | or d => d.length.succ
33- | and dp dq => (max (length dp) (length dq)).succ
34- | wk d _ => d.length.succ
35- | cut dp dn => (max (length dp) (length dn)).succ
36- | axm _ => 0
26+ def height {Δ : Sequent α} : ⊢ᴷ Δ → ℕ
27+ |identity _ => 0
28+ | cut dp dn => max dp.height dn.height + 1
29+ | wk d _ => d.height + 1
30+ | verum => 0
31+ | or d => d.height + 1
32+ | and dp dq => max (height dp) (height dq) + 1
3733
38- protected def cast (d : T ⟹ Δ) (e : Δ = Γ) : T ⟹ Γ := cast (by simp [e]) d
34+ protected def cast (d : ⊢ᴷ Δ) (e : Δ = Γ) : ⊢ᴷ Γ := cast (by simp [e]) d
3935
40- @[simp] lemma length_cast (d : T ⟹ Δ) (e : Δ = Γ) : length (Derivation.cast d e) = length d := by
36+ @[simp] lemma height_cast (d : ⊢ᴷ Δ) (e : Δ = Γ) : height (Derivation.cast d e) = height d := by
4137 rcases e with rfl; simp [Derivation.cast]
4238
43- def verum' (h : ⊤ ∈ Δ) : T ⟹ Δ := (verum Δ).wk (by simp [h])
44-
45- def axL' (a : α)
46- (h : NNFormula.atom a ∈ Δ) (hn : NNFormula.natom a ∈ Δ) : T ⟹ Δ := (axL Δ a).wk (by simp [h, hn])
47-
48- def em {φ : NNFormula α} {Δ : Sequent α} (hpos : φ ∈ Δ) (hneg : ∼φ ∈ Δ) : T ⟹ Δ := by
49- induction φ using NNFormula.rec' generalizing Δ <;> simp at hneg
50- case hverum => exact verum' hpos
51- case hfalsum => exact verum' hneg
52- case hatom a => exact axL' a hpos hneg
53- case hnatom a => exact axL' a hneg hpos
54- case hand φ ψ ihp ihq =>
55- have ihp : T ⟹ φ :: ∼φ :: ∼ψ :: Δ := ihp (by simp) (by simp)
56- have ihq : T ⟹ ψ :: ∼φ :: ∼ψ :: Δ := ihq (by simp) (by simp)
57- have : T ⟹ ∼φ :: ∼ψ :: Δ := (ihp.and ihq).wk (by simp [hpos])
58- exact this.or.wk (by simp [hneg])
59- case hor φ ψ ihp ihq =>
60- have ihp : T ⟹ ∼φ :: φ :: ψ :: Δ := ihp (by simp) (by simp)
61- have ihq : T ⟹ ∼ψ :: φ :: ψ :: Δ := ihq (by simp) (by simp)
62- have : T ⟹ φ :: ψ :: Δ := (ihp.and ihq).wk (by simp [hneg])
63- exact this.or.wk (by simp [hpos])
64-
65- instance : Tait (NNFormula α) (Theory α) where
66- verum := fun _ Δ => Derivation.verum Δ
67- and := fun dp dq => Derivation.cast (dp.and dq) (by simp)
68- or := fun d => Derivation.cast d.or (by simp)
69- wk := fun d ss => d.wk ss
70- em := fun hp hn => Derivation.em hp hn
71-
72- instance : Tait.Cut (NNFormula α) (Theory α) := ⟨Derivation.cut⟩
73-
74- def trans (F : U ⊢!* T) {Γ : Sequent α} : T ⟹ Γ → U ⟹ Γ
75- | axL Γ φ => axL Γ φ
76- | verum Γ => verum Γ
77- | and d₁ d₂ => and (trans F d₁) (trans F d₂)
78- | or d => or (trans F d)
79- | wk d ss => wk (trans F d) ss
80- | cut d₁ d₂ => cut (trans F d₁) (trans F d₂)
81- | axm h => F h
82-
83- instance : Tait.Axiomatized (NNFormula α) (Theory α) where
84- axm {_ _ h} := axm h
85- trans {_ _ _ F d} := trans (fun h ↦ F _ h) d
86-
87- variable [DecidableEq α]
88-
89- def compact {Γ : Sequent α} : T ⟹ Γ → (s : { s : Finset (NNFormula α) // ↑s ⊆ T}) × (s : Theory α) ⟹ Γ
90- | axL Γ φ => ⟨⟨∅, by simp⟩, axL Γ φ⟩
91- | verum Γ => ⟨⟨∅, by simp⟩, verum Γ⟩
92- | and d₁ d₂ =>
93- let ⟨s₁, d₁⟩ := compact d₁
94- let ⟨s₂, d₂⟩ := compact d₂
95- ⟨⟨(s₁ ∪ s₂ : Finset (NNFormula α)), by simp [s₁.prop, s₂.prop]⟩,
96- and (Tait.ofAxiomSubset (by simp) d₁) (Tait.ofAxiomSubset (by simp) d₂)⟩
97- | or d =>
98- let ⟨s, d⟩ := compact d
99- ⟨s, or d⟩
100- | wk d ss =>
101- let ⟨s, d⟩ := compact d
102- ⟨s, wk d ss⟩
103- | cut d₁ d₂ =>
104- let ⟨s₁, d₁⟩ := compact d₁
105- let ⟨s₂, d₂⟩ := compact d₂
106- ⟨⟨(s₁ ∪ s₂ : Finset (NNFormula α)), by simp [s₁.prop, s₂.prop]⟩,
107- cut (Tait.ofAxiomSubset (by simp) d₁) (Tait.ofAxiomSubset (by simp) d₂)⟩
108- | axm (φ := φ) h =>
109- ⟨⟨{φ}, by simp [h]⟩, axm (by simp)⟩
110-
111- instance : Entailment.Compact (Theory α) where
112- Γ b := (compact b).1
113- ΓPrf b := (compact b).2
114- Γ_subset b := by simpa using (compact b).1 .prop
115- Γ_finite b := by simp
116-
117- def deductionAux {Γ : Sequent α} {φ} : T ⟹ Γ → T \ {φ} ⟹ ∼φ :: Γ
118- | axL Γ φ => wk (axL Γ φ) (by simp)
119- | verum Γ => wk (verum Γ) (by simp)
120- | and d₁ d₂ =>
121- Tait.rotate₁ <| and (Tait.rotate₁ <| deductionAux d₁) (Tait.rotate₁ <| deductionAux d₂)
122- | or d => Tait.rotate₁ <| Tait.or <| Tait.wk (deductionAux d) (by intro x; simp; tauto)
123- | wk d ss => wk (deductionAux d) <| List.cons_subset_cons (∼φ) ss
124- | cut d₁ d₂ => cut (Tait.rotate₁ <| deductionAux d₁) (Tait.rotate₁ <| deductionAux d₂)
125- | axm (φ := ψ) h =>
126- if hq : φ = ψ then em (φ := φ) (by simp [hq]) (by simp) else
127- Tait.wk (show T \ {φ} ⟹ [ψ] from Tait.axm (by simp [h, Ne.symm hq])) (by simp)
128-
129- def deduction {Γ : Sequent α} {φ} (d : insert φ T ⟹ Γ) : T ⟹ ∼φ :: Γ := Tait.ofAxiomSubset (by simp) (deductionAux d)
130-
131- lemma inconsistent_iff_provable :
132- Entailment.Inconsistent (insert φ T) ↔ T ⊢ ∼φ := by
133- constructor
134- · intro h; exact ⟨deduction (Tait.inconsistent_iff_provable.mp h).get⟩
135- · rintro b
136- exact Entailment.inconsistent_of_provable_of_unprovable (φ := φ) (Entailment.by_axm _ <| by simp) (Entailment.wk! (by simp) b)
137-
138- lemma consistent_iff_unprovable :
139- Entailment.Consistent (insert φ T) ↔ T ⊬ ∼φ := by simp [←Entailment.not_inconsistent_iff_consistent, inconsistent_iff_provable]
140-
141- omit [DecidableEq α]
142- @[simp] lemma inconsistent_theory_iff :
143- Entailment.Inconsistent (Entailment.theory T) ↔ Entailment.Inconsistent T := by
144- constructor
145- · intro h
146- exact Entailment.inconsistent_iff_provable_bot.mpr
147- <| Entailment.StrongCut.cut! (by simp) <| Entailment.inconsistent_iff_provable_bot.mp h
148- · intro h; exact h.of_supset (by simpa using Entailment.Axiomatized.axm_subset T)
149-
150- @[simp] lemma consistent_theory_iff :
151- Entailment.Consistent (Entailment.theory T) ↔ Entailment.Consistent T := by simp [←Entailment.not_inconsistent_iff_consistent, inconsistent_theory_iff]
39+ def weakening (d : ⊢ᴷ Δ) (h : Δ ⊆ Γ := by simp) : ⊢ᴷ Γ := wk d h
40+
41+ def top (h : ⊤ ∈ Δ := by simp) : ⊢ᴷ Δ := verum.wk (by simp [h])
42+
43+ def identity' (a : α) (hpos : .atom a ∈ Δ := by simp) (hneg : .natom a ∈ Δ := by simp) : ⊢ᴷ Δ :=
44+ (identity a).wk (by simp [hpos, hneg])
45+
46+ def tensor {φ ψ} (dφ : ⊢ᴷ φ :: Γ) (dψ : ⊢ᴷ ψ :: Δ) : ⊢ᴷ φ ⋏ ψ :: (Γ ++ Δ) := and dφ.weakening dψ.weakening
47+
48+ def rotate (d : ⊢ᴷ φ :: Γ) : ⊢ᴷ Γ ++ [φ] := d.weakening
49+
50+ def eta : (φ : NNFormula α) → ⊢ᴷ [φ, ∼φ]
51+ | .atom a | .natom a => identity' a
52+ | ⊤ | ⊥ => top
53+ | φ ⋏ ψ => ((eta φ).tensor (eta ψ)).rotate.or.rotate
54+ | φ ⋎ ψ => ((eta φ).rotate.tensor (eta ψ).rotate).rotate.or
55+
56+ def close (φ : NNFormula α) (hp : φ ∈ Δ := by simp) (hn : ∼φ ∈ Δ := by simp) : ⊢ᴷ Δ :=
57+ eta φ |>.weakening (by simp [hp, hn])
58+
59+ instance : OneSidedLK (Derivation (α := α)) where
60+ verum := verum
61+ and d₁ d₂ := d₁.and d₂
62+ or d := d.or
63+ wk d ss := d.wk ss
64+ identity φ := eta φ
65+
66+ instance : OneSidedLK.Cut (Derivation (α := α)) where
67+ cut dp dn := cut dp dn
15268
15369end Derivation
15470
155- abbrev Sequent.Tautology (Γ : Sequent α) := (∅ : Theory α) ⟹ Γ
71+ /-! ## Classical proof system -/
15672
157- abbrev Sequent.IsTautology (Γ : Sequent α) := (∅ : Theory α) ⟹! Γ
73+ inductive Proof.Symbol (α : Type *) : Type
74+ | symbol
15875
159- abbrev NNFormula.Tautology (φ : NNFormula α) := Sequent.Tautology [φ]
76+ notation "𝐋𝐊⁰" => Proof.Symbol.symbol
16077
161- abbrev NNFormula.IsTautology (φ : NNFormula α) := Sequent.IsTautology [φ]
78+ abbrev Proof (φ : NNFormula α) := ⊢ᴷ [φ]
79+
80+ instance : Entailment (Proof.Symbol α) (NNFormula α) where
81+ Prf _ := Proof
82+
83+ namespace Proof
84+
85+ lemma def_eq (φ : NNFormula α) : (𝐋𝐊⁰ ⊢! φ) = (⊢ᴷ [φ]) := rfl
86+
87+ instance : OneSidedLK.EmptyEntailment (Derivation (α := α)) (𝐋𝐊⁰ : Proof.Symbol α) where
88+ equiv := Equiv.refl _
89+
90+ instance classical : Entailment.Cl (𝐋𝐊⁰ : Proof.Symbol α) := inferInstance
91+
92+ end Proof
93+
94+ abbrev NNFormula.IsTautology (φ : NNFormula α) : Prop := 𝐋𝐊⁰ ⊢ φ
16295
16396end LO.Propositional
97+
16498end
0 commit comments