Skip to content

Commit 5baf6f0

Browse files
iehalityiehality
committed
add
1 parent f21f1d8 commit 5baf6f0

2 files changed

Lines changed: 128 additions & 21 deletions

File tree

‎Foundation/FirstOrder/Basic/Calculus.lean‎

Lines changed: 30 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,16 @@ abbrev Proof (φ : Proposition L) := ⊢ᴷ [φ]
242242
instance : Entailment (Proof.Symbol L) (Proposition L) where
243243
Prf _ := Proof
244244

245-
lemma Proof.def (φ : Proposition L) : (𝐋𝐊¹ ⊢! φ) = (⊢ᴷ [φ]) := rfl
245+
namespace Proof
246+
247+
lemma def_eq (φ : Proposition L) : (𝐋𝐊¹ ⊢! φ) = (⊢ᴷ [φ]) := rfl
248+
249+
instance : OneSidedLK.EmptyEntailment (Derivation (L := L)) (𝐋𝐊¹ : Proof.Symbol L) where
250+
equiv := Equiv.refl _
251+
252+
instance classical : Entailment.Cl (𝐋𝐊¹ : Proof.Symbol L) := inferInstance
253+
254+
end Proof
246255

247256
structure Schema.Proof (𝓢 : Schema L) (φ : Proposition L) where
248257
axioms : List (Proposition L)
@@ -282,7 +291,7 @@ instance (𝓢 𝓤 : Schema L) : 𝓤 ⪯ 𝓢 ⊔ 𝓤 := weakerThan_of_le (by
282291

283292
lemma inconsistent_iff :
284293
Entailment.Inconsistent 𝓢 ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ ∼Γ) :=
285-
OneSidedLK.inconsistent_iff
294+
OneSidedLK.Entailment.inconsistent_iff
286295

287296
def rewrite [𝓢.IsClosed] (b : 𝓢 ⊢! φ) (f : ℕ → SyntacticTerm L) :
288297
𝓢 ⊢! Rew.rewrite f ▹ φ where
@@ -293,6 +302,10 @@ def rewrite [𝓢.IsClosed] (b : 𝓢 ⊢! φ) (f : ℕ → SyntacticTerm L) :
293302
exact Schema.IsClosed.closed (Rew.rewrite f) _ (b.axioms_mem ψ hψ)
294303
derivation := b.derivation.rewrite f |>.cast
295304

305+
@[simp] lemma empty_provable_iff_eprovable :
306+
(⊥ : Schema L) ⊢ φ ↔ 𝐋𝐊¹ ⊢ φ :=
307+
OneSidedLK.Entailment.empty_provable_iff_eprovable 𝐋𝐊¹
308+
296309
end Schema.Proof
297310

298311
namespace Derivation
@@ -303,7 +316,7 @@ variable {Γ Δ : Sequent L}
303316

304317
def eCut (d₁ : ⊢ᴷ φ :: Γ) (d₂ : ⊢ᴷ ψ :: Δ) (e : ∼φ = ψ := by simp) : ⊢ᴷ Γ ++ Δ := cut d₁ (d₂.cast (by simp [e]))
305318

306-
def disj₂ {Γ Δ : Sequent L} : ⊢ᴷ (Γ ++ Δ) → ⊢ᴷ ⋁Γ :: Δ := fun d ↦
319+
def disj₂ {Γ Δ : Sequent L} : ⊢ᴷ Γ ++ Δ → ⊢ᴷ ⋁Γ :: Δ := fun d ↦
307320
match Γ with
308321
| [] => d.weakening
309322
| [φ] => d
@@ -344,11 +357,9 @@ end Derivation
344357

345358
namespace Schema.Proof
346359

347-
variable {𝓢 : Schema L}
348-
349-
open Derivation
360+
open Entailment Derivation
350361

351-
lemma iff_context : 𝓢 ⊢ φ ↔ 𝓢 *⊢[𝐋𝐊¹] φ := by
362+
lemma iff_context {𝓢 : Schema L} : 𝓢 ⊢ φ ↔ 𝓢 *⊢[𝐋𝐊¹] φ := by
352363
constructor
353364
· rintro ⟨d⟩
354365
have : 𝐋𝐊¹ ⊢! ⋀d.axioms ➝ φ :=
@@ -362,10 +373,21 @@ lemma iff_context : 𝓢 ⊢ φ ↔ 𝓢 *⊢[𝐋𝐊¹] φ := by
362373
this.tensor (identity φ).rotate |>.weakening
363374
refine ⟨⟨Γ, h, (d.eCut this).cast⟩⟩
364375

376+
open Classical in
377+
378+
noncomputable instance : Entailment.Deduction (Schema L) where
379+
ofInsert {φ ψ 𝓢 b} :=
380+
have : insert φ ↑𝓢 *⊢[𝐋𝐊¹] ψ := iff_context.mp ⟨b⟩
381+
have : ↑𝓢 *⊢[𝐋𝐊¹] φ ➝ ψ := Context.deduct! this
382+
(iff_context.mpr this).get
383+
inv {φ ψ 𝓢 b} :=
384+
have : ↑(adjoin φ 𝓢) *⊢[𝐋𝐊¹] ψ := Context.deductInv! (iff_context.mp ⟨b⟩)
385+
(iff_context.mpr this).get
386+
365387
end Schema.Proof
366388

367389
/-!
368-
### Theory of schemata
390+
### Theory
369391
-/
370392

371393
def Schema.theory (𝓢 : Schema L) : Theory L := {σ | 𝓢 ⊢ ↑σ}

‎Foundation/Logic/Calculus.lean‎

Lines changed: 98 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -53,26 +53,93 @@ def rotate₃ (d : 𝔇 (φ₄ :: φ₁ :: φ₂ :: φ₃ :: Γ)) : 𝔇 (φ₁
5353

5454
alias cut := OneSidedLK.Cut.cut
5555

56+
open Entailment
57+
58+
class EmptyEntailment (𝔇 : outParam (List F → Type*)) {E : Type*} [Entailment E F] (𝓔 : E) where
59+
equiv {φ} : 𝓔 ⊢! φ ≃ 𝔇 [φ]
60+
61+
namespace EmptyEntailment
62+
63+
variable {E : Type*} [Entailment E F] (𝓔 : E) [EmptyEntailment 𝔇 𝓔]
64+
65+
omit [LogicalConnective F] [DeMorgan F] [NegInvolutive F] [OneSidedLK 𝔇] in
66+
lemma provable_iff :
67+
𝓔 ⊢ φ ↔ Nonempty (𝔇 [φ]) := by
68+
simpa using OneSidedLK.EmptyEntailment.equiv.nonempty_congr
69+
70+
variable [OneSidedLK.Cut 𝔇]
71+
72+
instance : Entailment.ModusPonens 𝓔 where
73+
mdp {φ ψ} b₁ b₂ :=
74+
let b₁ := equiv b₁
75+
let b₂ := equiv b₂
76+
have : 𝔇 [∼(φ ➝ ψ), ∼φ, ψ] := cast (tensor (𝔇 := 𝔇) (identity φ) (identity (∼ψ))) (by simp [DeMorgan.imply])
77+
have : 𝔇 [∼φ, ψ] := wk (cut b₁ this) (by simp)
78+
have : 𝔇 [ψ] := wk (cut b₂ this) (by simp)
79+
equiv.symm <| cast this
80+
81+
instance : Entailment.Cl 𝓔 where
82+
negEquiv {φ} := Entailment.cast
83+
(show 𝓔 ⊢! (φ ⋎ ∼φ ⋎ ⊥) ⋏ (φ ⋏ ⊤ ⋎ ∼φ) from
84+
equiv.symm <| and (or <| rotate₁ <| or <| close φ) (or <| and (identity φ) verum'))
85+
(by simp [Axioms.NegEquiv, DeMorgan.imply, LogicalConnective.iff])
86+
verum := equiv.symm <| verum
87+
implyK {φ ψ} :=
88+
have : 𝓔 ⊢! ∼φ ⋎ ∼ψ ⋎ φ := equiv.symm <| or <| rotate₁ <| or <| close φ
89+
Entailment.cast this (by simp [DeMorgan.imply])
90+
implyS {φ ψ χ} :=
91+
have : 𝓔 ⊢! φ ⋏ ψ ⋏ ∼χ ⋎ φ ⋏ ∼ψ ⋎ ∼φ ⋎ χ :=
92+
equiv.symm <| or <| rotate₁ <| or <| rotate₁ <| or <| rotate₃ <| and
93+
(close φ)
94+
(and (rotate₃ <| and (close φ) (close ψ)) (close χ))
95+
Entailment.cast this (by simp [DeMorgan.imply])
96+
and₁ {φ ψ} :=
97+
have : 𝓔 ⊢! (∼φ ⋎ ∼ψ) ⋎ φ := equiv.symm <|or <| or <| close φ
98+
Entailment.cast this (by simp [DeMorgan.imply])
99+
and₂ {φ ψ} :=
100+
have : 𝓔 ⊢! (∼φ ⋎ ∼ψ) ⋎ ψ := equiv.symm <| or <| or <| close ψ
101+
Entailment.cast this (by simp [DeMorgan.imply])
102+
and₃ {φ ψ} :=
103+
have : 𝓔 ⊢! ∼φ ⋎ ∼ψ ⋎ φ ⋏ ψ := equiv.symm <| or <| rotate₁ <| or <| rotate₁ <| and (close φ) (close ψ)
104+
Entailment.cast this (by simp [DeMorgan.imply])
105+
or₁ {φ ψ} :=
106+
have : 𝓔 ⊢! ∼φ ⋎ φ ⋎ ψ := equiv.symm <| or <| rotate₁ <| or <| close φ
107+
Entailment.cast this (by simp [DeMorgan.imply])
108+
or₂ {φ ψ} :=
109+
have : 𝓔 ⊢! ∼ψ ⋎ φ ⋎ ψ := equiv.symm <| or <| rotate₁ <| or <| close ψ
110+
Entailment.cast this (by simp [DeMorgan.imply])
111+
or₃ {φ ψ χ} :=
112+
have : 𝓔 ⊢! φ ⋏ ∼χ ⋎ ψ ⋏ ∼ χ ⋎ ∼φ ⋏ ∼ψ ⋎ χ :=
113+
equiv.symm <| or <| rotate₁ <| or <| rotate₁ <| or <| and
114+
(rotate₃ <| and (close φ) (close χ))
115+
(rotate₂ <| and (close ψ) (close χ))
116+
Entailment.cast this (by simp [DeMorgan.imply])
117+
dne {φ} :=
118+
have : 𝓔 ⊢! ∼φ ⋎ φ := equiv.symm <| or <| close φ
119+
Entailment.cast this (by simp [DeMorgan.imply])
120+
121+
end EmptyEntailment
122+
56123
protected class Entailment (𝔇 : outParam (List F → Type*)) (S : Type*) [Entailment S F] [AdjunctiveSet F S] where
57124
equiv {𝓢 : S} {φ} : 𝓢 ⊢! φ ≃ (l : {l : List F // ∀ φ ∈ l, φ ∈ 𝓢}) × 𝔇 (φ :: ∼l)
58125

59-
open Entailment
126+
namespace Entailment
60127

61128
variable {S : Type*} [Entailment S F] [AdjunctiveSet F S] [OneSidedLK.Entailment 𝔇 S]
62129

63130
omit [DeMorgan F] [NegInvolutive F] [OneSidedLK 𝔇] in
64131
lemma provable_iff {𝓢 : S} :
65132
𝓢 ⊢ φ ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (φ :: ∼Γ)) := by
66-
simpa using OneSidedLK.Entailment.equiv.nonempty_congr
133+
simpa using equiv.nonempty_congr
67134

68-
def toProof (𝓢 : S) (d : 𝔇 [φ]) : 𝓢 ⊢! φ := OneSidedLK.Entailment.equiv.symm ⟨⟨[], by simp⟩, d⟩
135+
def toProof (𝓢 : S) (d : 𝔇 [φ]) : 𝓢 ⊢! φ := equiv.symm ⟨⟨[], by simp⟩, d⟩
69136

70137
def ofAxiom {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ :=
71-
OneSidedLK.Entailment.equiv.symm ⟨⟨[φ], by simp_all⟩, identity φ⟩
138+
equiv.symm ⟨⟨[φ], by simp_all⟩, identity φ⟩
72139

73140
def ofAxiomSubset {𝓢 𝓤 : S} : 𝓢 ⊢! φ → 𝓢 ⊆ 𝓤 → 𝓤 ⊢! φ := fun b h ↦
74-
have ⟨l, d⟩ := OneSidedLK.Entailment.equiv b
75-
OneSidedLK.Entailment.equiv.symm
141+
have ⟨l, d⟩ := equiv b
142+
equiv.symm
76143
⟨⟨l, fun φ hφ ↦ AdjunctiveSet.subset_iff.mp h _ (l.prop φ hφ)⟩, d⟩
77144

78145
instance : Entailment.Axiomatized S where
@@ -83,31 +150,31 @@ variable [OneSidedLK.Cut 𝔇]
83150

84151
instance (𝓢 : S) : Entailment.ModusPonens 𝓢 where
85152
mdp {φ ψ} b₁ b₂ :=
86-
let ⟨Γ₁, b₁⟩ := OneSidedLK.Entailment.equiv b₁
87-
let ⟨Γ₂, b₂⟩ := OneSidedLK.Entailment.equiv b₂
153+
let ⟨Γ₁, b₁⟩ := equiv b₁
154+
let ⟨Γ₂, b₂⟩ := equiv b₂
88155
have : 𝔇 [∼(φ ➝ ψ), ∼φ, ψ] := cast (tensor (𝔇 := 𝔇) (identity φ) (identity (∼ψ))) (by simp [DeMorgan.imply])
89156
have : 𝔇 (∼φ :: ψ :: ∼↑Γ₁) := wk (cut b₁ this) (by simp)
90157
have : 𝔇 (ψ :: ∼↑Γ₁ ++ ∼↑Γ₂) := wk (cut b₂ this) (by simp)
91-
OneSidedLK.Entailment.equiv.symm ⟨⟨Γ₁ ++ Γ₂, by simp; grind⟩, cast this⟩
158+
equiv.symm ⟨⟨Γ₁ ++ Γ₂, by simp; grind⟩, cast this⟩
92159

93160
instance : Entailment.StrongCut S S where
94161
cut {T U φ bs b} :=
95162
let rec bl (l : List F) (hl : ∀ ψ ∈ l, ψ ∈ U) (χ) (d : 𝔇 (χ :: ∼l)) : T ⊢! χ :=
96163
match l with
97-
| [] => OneSidedLK.Entailment.equiv.symm ⟨⟨[], by simp⟩, d⟩
164+
| [] => equiv.symm ⟨⟨[], by simp⟩, d⟩
98165
| ψ :: l =>
99166
have bχ : T ⊢! ψ ➝ χ :=
100167
Entailment.cast (bl l (by simp at hl; grind) (∼ψ ⋎ χ) (OneSidedLK.or <| OneSidedLK.rotate₁ d))
101168
(by simp [DeMorgan.imply])
102169
have bψ : T ⊢! ψ := bs (show ψ ∈ U by simp at hl; grind)
103170
Entailment.mdp bχ bψ
104-
have ⟨l, hl⟩ := OneSidedLK.Entailment.equiv b
171+
have ⟨l, hl⟩ := equiv b
105172
bl l l.prop φ hl
106173

107174
instance : Entailment.DeductiveExplosion S where
108175
dexp b φ :=
109-
have ⟨Γ, b⟩ := OneSidedLK.Entailment.equiv b
110-
OneSidedLK.Entailment.equiv.symm
176+
have ⟨Γ, b⟩ := equiv b
177+
equiv.symm
111178
⟨ Γ,
112179
have : 𝔇 [∼⊥] := cast verum (by simp)
113180
wk (cut b this) (by simp) ⟩
@@ -164,6 +231,24 @@ instance (𝓢 : S) : Entailment.Cl 𝓢 where
164231
have : 𝓢 ⊢! ∼φ ⋎ φ := toProof _ <| or <| close φ
165232
Entailment.cast this (by simp [DeMorgan.imply])
166233

234+
variable {E : Type*} [Entailment E F]
235+
236+
omit [DeMorgan F] [OneSidedLK 𝔇] [Cut 𝔇] in
237+
lemma empty_provable_iff_eprovable (𝓔 : E) [EmptyEntailment 𝔇 𝓔] :
238+
(∅ : S) ⊢ φ ↔ 𝓔 ⊢ φ := by
239+
constructor
240+
· rintro ⟨d⟩
241+
let ⟨l, d⟩ := equiv d
242+
have : 𝓔 ⊢! φ := EmptyEntailment.equiv.symm <| cast d <| by
243+
have : ∀ φ, φ ∉ (l : List F) := by simpa using l.prop
244+
simp [List.eq_nil_iff_forall_not_mem]; grind
245+
exact ⟨this⟩
246+
· rintro ⟨b⟩
247+
have : 𝔇 [φ] := EmptyEntailment.equiv b
248+
exact ⟨equiv.symm ⟨⟨[], by simp⟩, this⟩⟩
249+
250+
end Entailment
251+
167252
end OneSidedLK
168253

169254
end LO

0 commit comments

Comments
 (0)