iff_context

Author: iehality

Foundation/FirstOrder/Basic/Calculus.lean

@@ -27,6 +27,9 @@ def newVar (Γ : Sequent L) : ℕ := (Γ.map Semiformula.fvSup).foldr max 0
 lemma not_fvar?_newVar {φ : Proposition L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬FVar? φ Γ.newVar :=
   not_fvar?_of_lt_fvSup φ (by simpa [newVar] using List.le_max_of_le (List.mem_map_of_mem h) (by simp))
 
+@[simp] lemma rew_neg_comm {Γ : Sequent L} (ω : Rew L ℕ 0 ℕ 0) :
+    (∼Γ).map (ω ▹ ·) = ∼Γ.map (ω ▹ ·) := by simp [List.tilde_def]
+
 end Sequent
 
 /-! ## Derivation for one-sided $\mathbf{LK}$ -/
@@ -48,8 +51,6 @@ namespace Derivation
 
 open Rewriting LawfulSyntacticRewriting
 
-
-
 def height {Δ : Sequent L} : ⊢ᴷ Δ → ℕ
   |   .id _ _ => 0
   | cut dp dn => (max (height dp) (height dn)).succ
@@ -262,10 +263,6 @@ def equiv (𝓢 : Schema L) (φ) :
   toFun b := ⟨⟨b.axioms, b.axioms_mem⟩, b.derivation⟩
   invFun := fun ⟨⟨Γ, hΓ⟩, d⟩ ↦ ⟨Γ, hΓ, d⟩
 
-lemma provable_iff :
-    𝓢 ⊢ φ ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ φ :: ∼Γ) := by
-  simpa using (equiv 𝓢 φ).nonempty_congr
-
 instance : Entailment.Compact (Schema L) where
   core b := ⟨fun φ ↦ φ ∈ b.axioms⟩
   corePrf b := ⟨b.axioms, by simp, b.derivation⟩
@@ -284,29 +281,96 @@ instance (𝓢 𝓤 : Schema L) : 𝓢 ⪯ 𝓢 ⊔ 𝓤 := weakerThan_of_le (by
 instance (𝓢 𝓤 : Schema L) : 𝓤 ⪯ 𝓢 ⊔ 𝓤 := weakerThan_of_le (by simp)
 
 lemma inconsistent_iff :
-    Entailment.Inconsistent 𝓢 ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ ∼Γ) := calc
-  _ ↔ 𝓢 ⊢ ⊥ := Entailment.inconsistent_iff_provable_bot
-  _ ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ ⊥ :: ∼Γ) := by simp [provable_iff]
-  _ ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ ∼Γ) := by
-    constructor
-    · rintro ⟨Γ, hΓ, ⟨d⟩⟩
-      have : ⊢ᴷ [(∼⊥ : Proposition L)] := Derivation.verum.cast
-      exact ⟨Γ, hΓ, ⟨(Derivation.cut d this).cast⟩⟩
-    · rintro ⟨Γ, hΓ, ⟨d⟩⟩
-      exact ⟨Γ, hΓ, ⟨d.weakening⟩⟩
+    Entailment.Inconsistent 𝓢 ↔ ∃ Γ : Sequent L, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (⊢ᴷ ∼Γ) :=
+  OneSidedLK.inconsistent_iff
+
+def rewrite [𝓢.IsClosed] (b : 𝓢 ⊢! φ) (f : ℕ → SyntacticTerm L) :
+    𝓢 ⊢! Rew.rewrite f ▹ φ where
+  axioms := b.axioms.map (Rew.rewrite f ▹ ·)
+  axioms_mem := by
+    suffices ∀ ψ ∈ b.axioms, Rew.rewrite f ▹ ψ ∈ 𝓢 by simpa
+    intro ψ hψ
+    exact Schema.IsClosed.closed (Rew.rewrite f) _ (b.axioms_mem ψ hψ)
+  derivation := b.derivation.rewrite f |>.cast
 
 end Schema.Proof
 
+namespace Derivation
+
+open Entailment
+
+variable {Γ Δ : Sequent L}
+
+def eCut (d₁ : ⊢ᴷ φ :: Γ) (d₂ : ⊢ᴷ ψ :: Δ) (e : ∼φ = ψ := by simp) : ⊢ᴷ Γ ++ Δ := cut d₁ (d₂.cast (by simp [e]))
+
+def disj₂ {Γ Δ : Sequent L} : ⊢ᴷ (Γ ++ Δ) → ⊢ᴷ ⋁Γ :: Δ := fun d ↦
+  match Γ with
+  |               [] => d.weakening
+  |              [φ] => d
+  |           [φ, ψ] => d.or
+  | φ :: ψ :: χ :: Γ =>
+    let Φ := ⋁(χ :: Γ)
+    have : ⊢ᴷ (φ ⋎ ψ :: χ :: Γ) ++ Δ := d.or
+    have d₁ : ⊢ᴷ (φ ⋎ ψ) ⋎ Φ :: Δ := this.disj₂
+    have d₂ : ⊢ᴷ [(∼φ ⋏ ∼ψ) ⋏ ∼Φ, φ ⋎ ψ ⋎ Φ] :=
+      have : ⊢ᴷ [φ, ψ ⋎ Φ, (∼φ ⋏ ∼ψ) ⋏ ∼Φ] :=
+        ((identity φ).rotate.tensor (identity ψ).rotate).tensor
+          (identity Φ).rotate |>.rotate.rotate.or.weakening
+      this.or.rotate
+    d₂.eCut d₁
+  termination_by _ => Γ.length
+
+def conj₂ {Γ Δ : Sequent L} (d : (φ : Proposition L) → φ ∈ Γ → ⊢ᴷ φ :: Δ) : ⊢ᴷ ⋀Γ :: Δ :=
+  match Γ with
+  |          [] => verum.weakening
+  |         [φ] => d φ (by simp)
+  | φ :: ψ :: Γ =>
+    have : ⊢ᴷ ⋀(ψ :: Γ) :: Δ := conj₂ (Γ := ψ :: Γ) (fun χ h ↦ d χ (by simp_all))
+    (d φ (by simp)).and this
+
+def disjClosure : ⊢ᴷ Γ → 𝐋𝐊¹ ⊢! ⋁Γ := fun d ↦
+  have : ⊢ᴷ Γ ++ [] := d.cast
+  this.disj₂
+
+def disjClosureInv : 𝐋𝐊¹ ⊢! ⋁Γ → ⊢ᴷ Γ := fun d ↦
+  have d₁ : ⊢ᴷ [⋁Γ] := d
+  have d₂ : ⊢ᴷ ⋀(∼Γ) :: Γ := conj₂ fun φ h ↦ close φ (by simp) (by simp_all)
+  d₁.eCut d₂
+
+lemma nonempty_iff_provable_disj : Nonempty (⊢ᴷ Γ) ↔ 𝐋𝐊¹ ⊢ ⋁Γ :=
+  ⟨by rintro ⟨d⟩; exact ⟨d.disjClosure⟩, by rintro ⟨d⟩; exact ⟨d.disjClosureInv⟩⟩
+
+end Derivation
+
+namespace Schema.Proof
+
+variable {𝓢 : Schema L}
+
+open Derivation
+
+lemma iff_context : 𝓢 ⊢ φ ↔ 𝓢 *⊢[𝐋𝐊¹] φ := by
+  constructor
+  · rintro ⟨d⟩
+    have : 𝐋𝐊¹ ⊢! ⋀d.axioms ➝ φ :=
+      have : ⊢ᴷ ∼d.axioms ++ [φ] := d.derivation.weakening
+      this.disj₂.or.cast <| by simp [Semiformula.imp_eq]
+    refine ⟨⟨d.axioms, by simpa using d.axioms_mem, this⟩⟩
+  · rintro ⟨Γ, h, d⟩
+    have d : ⊢ᴷ [⋁(∼Γ) ⋎ φ] := d.cast (by simp [Semiformula.imp_eq])
+    have : ⊢ᴷ ⋀Γ ⋏ ∼φ :: φ :: ∼Γ :=
+      have : ⊢ᴷ ⋀Γ :: ∼Γ := Derivation.conj₂ fun φ h ↦ close φ (by simp) (by simp [h])
+      this.tensor (identity φ).rotate |>.weakening
+    refine ⟨⟨Γ, h, (d.eCut this).cast⟩⟩
+
+end Schema.Proof
 
 /-!
   ### Theory of schemata
 -/
 
-abbrev Theory (L : Language) := Set (Sentence L)
-
 def Schema.theory (𝓢 : Schema L) : Theory L := {σ | 𝓢 ⊢ ↑σ}
 
-@[simp] lemma Schema.mem_theory {𝓢 : Schema L} {σ : Sentence L} :
+@[simp] lemma Schema.mem_theory {𝓢 : Schema L} :
     σ ∈ 𝓢.theory ↔ 𝓢 ⊢ ↑σ := by simp [Schema.theory]
 
 namespace Theory

Foundation/FirstOrder/Basic/Syntax/Schema.lean

@@ -16,6 +16,7 @@ namespace LO.FirstOrder
 structure Schema (L : Language) where
   Mem : Proposition L → Prop
 
+abbrev Theory (L : Language) := Set (Sentence L)
 namespace Schema
 
 variable {L : Language}
@@ -119,6 +120,13 @@ instance sentence (σ : Sentence L) : IsClosed (σ : Schema L) where
 
 end IsClosed
 
+def uniClosure (𝓢 : Schema L) : Theory L := Set.image Semiformula.univCl {φ | φ ∈ 𝓢}
+
+variable {𝓢 : Schema L}
+
+@[simp] lemma mem_uniClosure :
+    σ ∈ 𝓢.uniClosure ↔ ∃ φ ∈ 𝓢, Semiformula.univCl φ = σ := by simp [uniClosure]
+
 end Schema
 
 end LO.FirstOrder

Foundation/Logic/Calculus.lean

@@ -60,6 +60,11 @@ open Entailment
 
 variable {S : Type*} [Entailment S F] [AdjunctiveSet F S] [OneSidedLK.Entailment 𝔇 S]
 
+omit [DeMorgan F] [NegInvolutive F] [OneSidedLK 𝔇] in
+lemma provable_iff {𝓢 : S} :
+    𝓢 ⊢ φ ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (φ :: ∼Γ)) := by
+  simpa using OneSidedLK.Entailment.equiv.nonempty_congr
+
 def toProof (𝓢 : S) (d : 𝔇 [φ]) : 𝓢 ⊢! φ := OneSidedLK.Entailment.equiv.symm ⟨⟨[], by simp⟩, d⟩
 
 def ofAxiom {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ :=
@@ -74,7 +79,7 @@ instance : Entailment.Axiomatized S where
   prfAxm h := ofAxiom h
   weakening h d := ofAxiomSubset d h
 
-variable [OneSidedLK.Cut 𝔇] [OneSidedLK.Entailment 𝔇 S]
+variable [OneSidedLK.Cut 𝔇]
 
 instance (𝓢 : S) : Entailment.ModusPonens 𝓢 where
   mdp {φ ψ} b₁ b₂ :=
@@ -107,6 +112,18 @@ instance : Entailment.DeductiveExplosion S where
       have : 𝔇 [∼⊥] := cast verum (by simp)
       wk (cut b this) (by simp) ⟩
 
+lemma inconsistent_iff {𝓢 : S} :
+    Entailment.Inconsistent 𝓢 ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (∼Γ)) := calc
+  _ ↔ 𝓢 ⊢ ⊥ := Entailment.inconsistent_iff_provable_bot
+  _ ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (⊥ :: ∼Γ)) := by simp [provable_iff]
+  _ ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (∼Γ)) := by
+    constructor
+    · rintro ⟨Γ, hΓ, ⟨d⟩⟩
+      have : 𝔇 [(∼⊥ : F)] := cast verum
+      exact ⟨Γ, hΓ, ⟨cast (cut d this)⟩⟩
+    · rintro ⟨Γ, hΓ, ⟨d⟩⟩
+      exact ⟨Γ, hΓ, ⟨wk d (by simp)⟩⟩
+
 instance (𝓢 : S) : Entailment.Cl 𝓢 where
   negEquiv {φ} := Entailment.cast
     (show 𝓢 ⊢! (φ ⋎ ∼φ ⋎ ⊥) ⋏ (φ ⋏ ⊤ ⋎ ∼φ) from

Foundation/Logic/LogicSymbol.lean

@@ -344,15 +344,32 @@ variable [Tilde α]
 
 instance : Tilde (List α) := ⟨fun l ↦ l.map (∼·)⟩
 
+lemma tilde_def (l : List α) : ∼l = l.map (∼·) := rfl
+
 @[simp] lemma tilde_nil : ∼([] : List α) = [] := rfl
 
 @[simp] lemma tilde_cons (a : α) (l : List α) : ∼(a :: l) = ∼a :: ∼l := rfl
 
 @[simp] lemma tilde_append (l k : List α) : ∼(l ++ k) = ∼l ++ ∼k := by
   induction l with
-  | nil => simp [*]
+  |          nil => simp [*]
   | cons a as ih => simp [*, List.cons_append]
 
+@[simp] lemma mem_tilde_iff [NegInvolutive α] {a : α} {l : List α} : a ∈ ∼l ↔ ∼a ∈ l := by
+  induction l with
+  |          nil => simp [*]
+  | cons b bs ih =>
+    suffices a = ∼b ↔ ∼a = b by
+      simp [ih, this]
+    constructor <;> {rintro rfl; simp}
+
+instance [NegInvolutive α] : NegInvolutive (List α) where
+  neg_involutive l := by
+    induction l with
+    |          nil => simp [*]
+    | cons a as ih =>
+      simp [ih, NegInvolutive.neg_involutive a]
+
 end tilde
 
 section conjunction
@@ -437,6 +454,34 @@ def disj' (f : ι → α) (l : List ι) : α := (l.map f).disj₂
 
 end disjunction
 
+section tilde
+
+variable [LogicalConnective α] [DeMorgan α]
+
+@[simp] lemma tilde_conj (l : List α) : ∼l.disj = (∼l).conj := by
+  match l with
+  |     [] => simp
+  | a :: l => simp [tilde_conj l]
+
+@[simp] lemma tilde_disj (l : List α) : ∼l.conj = (∼l).disj := by
+  match l with
+  |     [] => simp
+  | a :: l => simp [tilde_disj l]
+
+@[simp] lemma tilde_conj₂ (l : List α) : ∼⋁l = ⋀(∼l) := by
+  match l with
+  |          [] => simp
+  |         [a] => simp
+  | a :: b :: l => simp [tilde_conj₂ (b :: l)]
+
+@[simp] lemma tilde_disj₂ (l : List α) : ∼⋀l = ⋁(∼l) := by
+  match l with
+  |          [] => simp
+  |         [a] => simp
+  | a :: b :: l => simp [tilde_disj₂ (b :: l)]
+
+end tilde
+
 section
 
 variable [LogicalConnective α] [LogicalConnective β] [FunLike G α β] [LogicalConnective.HomClass G α β]