change: System, Deduction

Logic.lean

@@ -5,7 +5,6 @@ import Logic.Vorspiel.Meta
 import Logic.Logic.LogicSymbol
 import Logic.Logic.Semantics
 import Logic.Logic.System
-import Logic.Logic.HilbertStyle
 
 -- AutoProver
 

Logic/AutoProver/Prover.lean

@@ -232,7 +232,7 @@ section
 
 open Litform.Meta Denotation
 
-variable {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instSys : Q(System $F))
+variable {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instSys : Q(System.{u,u} $F))
   (instGz : Q(Gentzen $F)) (instLTS : Q(LawfulTwoSided $F))
 
 
@@ -292,7 +292,7 @@ elab "tautology" n:(num)? : tactic => do
   let ⟨u, F, T, p⟩ ← isExprProvable? ty
   let .some instLS ← trySynthInstanceQ (q(LogicalConnective.{u} $F) : Q(Type u))
     | throwError m! "error: failed to find instance LogicalConnective {F}"
-  let .some instSys ← trySynthInstanceQ q(System $F)
+  let .some instSys ← trySynthInstanceQ q(System.{u,u} $F)
     | throwError m! "error: failed to find instance System {F}"
   let .some instGz ← trySynthInstanceQ q(Gentzen $F)
     | throwError m! "error: failed to find instance Gentzen {F}"
@@ -312,7 +312,7 @@ elab "prover" n:(num)? seq:(termSeq)? : tactic => do
   let ⟨u, F, T, p⟩ ← isExprProvable? ty
   let .some instLS ← trySynthInstanceQ (q(LogicalConnective.{u} $F) : Q(Type u))
     | throwError m! "error: failed to find instance LogicalConnective {F}"
-  let .some instSys ← trySynthInstanceQ q(System $F)
+  let .some instSys ← trySynthInstanceQ q(System.{u,u} $F)
     | throwError m! "error: failed to find instance System {F}"
   let .some instGz ← trySynthInstanceQ q(Gentzen $F)
     | throwError m! "error: failed to find instance Gentzen {F}"

Logic/FirstOrder/Arith/Basic.lean

@@ -87,7 +87,7 @@ section
 variable {L : Language} [Structure L ℕ] (T : Theory L) (F : Set (Sentence L))
 
 lemma consistent_of_sound [SoundOn T F] (hF : F ⊥) : System.Consistent T :=
-  ⟨fun b => by simpa using SoundOn.sound hF ⟨b⟩⟩
+  fun b => by simpa using SoundOn.sound hF b
 
 end
 

Logic/FirstOrder/Basic/Calculus.lean

@@ -511,7 +511,7 @@ def lMap {σ : Sentence L₁} (b : T ⊢ σ) :
     (by simp; intro σ hσ; exact Set.mem_image_of_mem _ (b.antecedent_ss σ hσ) )
 
 lemma inconsistent_lMap : ¬System.Consistent T → ¬System.Consistent (T.lMap Φ) := by
-  simp[System.Consistent]; intro b; exact ⟨by simpa using lMap Φ b⟩
+  simp [System.inconsistent_iff_provable_falsum]; intro ⟨b⟩; exact ⟨by simpa using lMap Φ b⟩
 
 end System
 

Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean

@@ -26,7 +26,7 @@ variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T] [DecidableP
 variable (T)
 
 /-- Set $D \coloneqq \{\sigma\ |\ T \vdash \lnot\sigma(\ulcorner \sigma \urcorner)\}$ is r.e. -/
-private lemma diagRefutation_re : RePred (fun σ ↦ T ⊢! ~σ/[⸢σ⸣]) := by
+lemma diagRefutation_re : RePred (fun σ ↦ T ⊢! ~σ/[⸢σ⸣]) := by
   have : Partrec fun σ : Semisentence ℒₒᵣ 1 ↦ (provableFn T (~σ/[⸢σ⸣])).map (fun _ ↦ ()) :=
     Partrec.map
       ((provableFn_partrec T).comp <| Primrec.to_comp

Logic/Logic/Calculus.lean

@@ -279,7 +279,7 @@ end Disjconseq
 variable (F)
 
 instance : System F where
-  Bew := fun T p => T ⊢' [p]
+  turnstile := fun T p => T ⊢' [p]
   axm := fun {T p} h =>
     ⟨[p], by simpa,
       em (List.mem_singleton.mpr rfl) (List.mem_singleton.mpr rfl)⟩
@@ -311,42 +311,42 @@ lemma provable_iff {p : F} :
 theorem compact :
     System.Consistent T ↔ ∀ T' : Finset F, ↑T' ⊆ T → System.Consistent (T' : Set F) :=
   ⟨fun c u hu => c.of_subset hu,
-   fun h => ⟨by
+   fun h => by
     letI := Classical.typeDecidableEq F
     rintro ⟨Δ, hΔ, d⟩
     exact (System.unprovable_iff_not_provable.mp $
       System.consistent_iff_unprovable.mp $ h Δ.toFinset (by intro p; simpa using hΔ p))
-      (provable_iff.mpr $ ⟨Δ, by simp, ⟨d⟩⟩)⟩⟩
+      (provable_iff.mpr $ ⟨Δ, by simp, ⟨d⟩⟩)⟩
 
 theorem compact_inconsistent (h : ¬System.Consistent T) :
     ∃ s : Finset F, ↑s ⊆ T ∧ ¬System.Consistent (s : Set F) := by
   simpa using (not_iff_not.mpr compact).mp h
 
 lemma consistent_iff_empty_sequent :
     System.Consistent T ↔ IsEmpty (T ⊢' []) :=
-  ⟨by contrapose; simp[System.Consistent]; intro b; exact ⟨b.wk (by simp)⟩,
-   by contrapose; simp[System.Consistent]
+  ⟨by contrapose; simp[System.Consistent, Deduction.Consistent, Deduction.Undeducible]; intro b; exact ⟨b.wk (by simp)⟩,
+   by contrapose; simp[System.Consistent, Deduction.Consistent, Deduction.Undeducible]
       rintro ⟨Δ, h, d⟩
       have : Δ ⊢² [] := Cut.cut d (falsum _ _)
       exact ⟨toDisjconseq this h⟩⟩
 
 lemma provable_iff_inconsistent {p} :
     T ⊢! p ↔ ¬System.Consistent (insert (~p) T) :=
   ⟨by rintro ⟨⟨Δ, h, d⟩⟩
-      simp[consistent_iff_empty_sequent]
+      simp [consistent_iff_empty_sequent]
       exact ⟨⟨~p :: Δ, by simp; intro q hq; right; exact h q hq, negLeft d⟩⟩,
    by letI := Classical.typeDecidableEq F
-      simp[consistent_iff_empty_sequent]
+      simp [consistent_iff_empty_sequent]
       intro b
       exact ⟨b.deductionNeg⟩⟩
 
 lemma refutable_iff_inconsistent {p} :
     T ⊢! ~p ↔ ¬System.Consistent (insert p T) :=
   ⟨by rintro ⟨⟨Δ, h, d⟩⟩
-      simp[consistent_iff_empty_sequent]
+      simp [consistent_iff_empty_sequent]
       exact ⟨⟨p :: Δ, by simp; intro q hq; right; exact h q hq, ofNegRight d⟩⟩,
    by letI := Classical.typeDecidableEq F
-      simp[consistent_iff_empty_sequent]
+      simp [consistent_iff_empty_sequent]
       intro b
       exact ⟨b.deduction⟩⟩
 
@@ -366,10 +366,11 @@ lemma inconsistent_of_provable_and_refutable' {p}
 
 @[simp] lemma consistent_theory_iff_consistent :
     System.Consistent (System.theory T) ↔ System.Consistent T :=
-  ⟨fun h ↦ h.of_subset (by intro _; simp[System.theory]; exact fun h ↦ ⟨System.axm h⟩),
-   fun consis ↦ ⟨fun b ↦ by
+  ⟨fun h ↦ h.of_subset (by intro _; simp[System.theory]; exact fun h ↦ ⟨Deduction.axm h⟩),
+   fun consis ↦ fun b ↦ by
+      rcases b with ⟨b⟩
       have : ¬System.Consistent T := System.inconsistent_of_proof (proofCut System.provableTheory_theory b)
-      contradiction ⟩⟩
+      contradiction⟩
 
 end Gentzen
 

Logic/Logic/Deduction.lean

@@ -6,6 +6,26 @@ class Deduction {F : Type*} (Bew : Set F → F → Type*) where
   axm : ∀ {f}, f ∈ Γ → Bew Γ f
   weakening' : ∀ {T U f}, T ⊆ U → Bew T f → Bew U f
 
+namespace Deduction
+
+variable {F : Type*} [LogicalConnective F] (Bew : Set F → F → Type*) [Deduction Bew]
+
+variable (Γ : Set F) (p : F)
+
+def Deducible := Nonempty (Bew Γ p)
+
+def Undeducible := ¬Deducible Bew Γ p
+
+def Inconsistent := Deducible Bew Γ ⊥
+
+def Consistent := Undeducible Bew Γ ⊥
+
+variable {Bew Γ p}
+
+lemma not_consistent : ¬Consistent Bew Γ ↔ Deducible Bew Γ ⊥ := by simp [Consistent, Undeducible]
+
+end Deduction
+
 namespace Hilbert
 
 variable {F : Type*} [LogicalConnective F] [DecidableEq F] [NegDefinition F]
@@ -281,9 +301,6 @@ local infix:20 " ⊢ " => Bew
 
 variable (Γ : Set F) (p : F)
 
-abbrev Deducible := Nonempty (Bew Γ p)
-abbrev Undeducible := ¬(Deducible Bew Γ p)
-
 section Deducible
 
 variable {Bew : Set F → F → Type u} [Deduction Bew]
@@ -360,14 +377,14 @@ lemma contra₀'! {Γ : Set F} {p q : F} (d : Γ ⊢! (p ⟶ q)) : Γ ⊢! (~q 
 lemma dtr! {Γ : Set F} {p q : F} (d : (insert p Γ) ⊢! q) : Γ ⊢! (p ⟶ q) := ⟨dtr d.some⟩
 lemma dtr_not! {Γ : Set F} {p q : F} : (Γ ⊬! (p ⟶ q)) → ((insert p Γ) ⊬! q) := by
   contrapose;
-  simp;
+  simp [Undeducible, Deducible];
   intro d;
   exact ⟨dtr d⟩
 
 lemma dtl! {Γ : Set F} {p q : F} (d : Γ ⊢! (p ⟶ q)) : (insert p Γ) ⊢! q := ⟨dtl d.some⟩
 lemma dtl_not! {Γ : Set F} {p q : F} : ((insert p Γ) ⊬! q) → (Γ ⊬! (p ⟶ q)) := by
   contrapose;
-  simp;
+  simp [Undeducible, Deducible];
   intro d;
   exact ⟨dtl d⟩
 
@@ -378,9 +395,6 @@ section Consistency
 local infix:20 "⊢!" => Deducible Bew
 local infix:20 "⊬!" => Undeducible Bew
 
-abbrev Inconsistent := Γ ⊢! ⊥
-abbrev Consistent := Γ ⊬! ⊥
-
 lemma consistent_iff_undeducible_falsum : Consistent Bew Γ ↔ (Γ ⊬! ⊥) := Iff.rfl
 
 lemma consistent_no_falsum {Γ} (h : Consistent Bew Γ) : ⊥ ∉ Γ := fun hC ↦ h ⟨hd.axm hC⟩
@@ -398,7 +412,7 @@ lemma consistent_subset_undeducible_falsum {Γ Δ} (hConsis : Consistent Bew Γ)
   exact hConsis.false $ hd.weakening' hΔ hC.some;
 
 lemma consistent_neither_undeducible {Γ : Set F} (hConsis : Consistent Bew Γ) (p) : (Γ ⊬! p) ∨ (Γ ⊬! ~p) := by
-  by_contra hC; simp only [not_or] at hC;
+  by_contra hC; simp only [Undeducible, not_or] at hC;
   have h₁ : Γ ⊢! p  := by simpa using hC.1;
   have h₂ : Γ ⊢! p ⟶ ⊥ := by simpa using hC.2;
   exact hConsis $ modus_ponens'! h₂ h₁;
@@ -430,7 +444,7 @@ lemma inconsistent_iff_insert_neg {Γ p} : Inconsistent Bew (insert (~p) Γ) ↔
 lemma consistent_iff_insert_neg {Γ p} : Consistent Bew (insert (~p) Γ) ↔ (Γ ⊬! p) := (inconsistent_iff_insert_neg Bew).not
 
 lemma consistent_either {Γ : Set F} (hConsis : Consistent Bew Γ) (p) : (Consistent Bew (insert p Γ)) ∨ (Consistent Bew (insert (~p) Γ)) := by
-  by_contra hC; simp [not_or, Consistent] at hC;
+  by_contra hC; simp [Undeducible, not_or, Consistent] at hC;
   have ⟨Δ₁, hΔ₁, ⟨dΔ₁⟩⟩ := inconsistent_insert Bew hC.1;
   have ⟨Δ₂, hΔ₂, ⟨dΔ₂⟩⟩ := inconsistent_insert Bew hC.2;
   exact consistent_subset_undeducible_falsum _ hConsis (by aesop) ⟨(dtr dΔ₂) ⨀ (dtr dΔ₁)⟩;

Logic/Logic/System.lean

@@ -28,17 +28,22 @@ variable [𝓑 : System F]
 
 open Deduction
 
-abbrev Provable (T : Set F) (f : F) : Prop := Nonempty (T ⊢ f)
+abbrev Provable (T : Set F) (f : F) : Prop := Deduction.Deducible (· ⊢ ·) T f
 
 infix:45 " ⊢! " => System.Provable
 
+open Deduction
+
+
 noncomputable def Provable.toProof {T : Set F} {f : F} (h : T ⊢! f) : T ⊢ f := Classical.choice h
 
-abbrev Unprovable (T : Set F) (f : F) : Prop := IsEmpty (T ⊢ f)
+abbrev Unprovable (T : Set F) (f : F) : Prop := Deduction.Undeducible (· ⊢ ·) T f
 
 infix:45 " ⊬ " => System.Unprovable
 
-lemma unprovable_iff_not_provable {T : Set F} {f : F} : T ⊬ f ↔ ¬T ⊢! f := by simp[System.Unprovable]
+lemma unprovable_iff_not_provable {T : Set F} {f : F} : T ⊬ f ↔ ¬T ⊢! f := by simp [System.Unprovable, Undeducible]
+
+lemma not_unprovable_iff_provable {T : Set F} {f : F} : ¬T ⊬ f ↔ T ⊢! f := by simp [System.Unprovable, Undeducible]
 
 def BewTheory (T U : Set F) : Type _ := {f : F} → f ∈ U → T ⊢ f
 
@@ -54,24 +59,33 @@ def BewTheory.ofSubset {T U : Set F} (h : U ⊆ T) : T ⊢* U := fun hf => axm (
 
 def BewTheory.refl (T : Set F) : T ⊢* T := axm
 
-def Consistent (T : Set F) : Prop := IsEmpty (T ⊢ ⊥)
+abbrev Consistent (T : Set F) : Prop := Deduction.Consistent (· ⊢ ·) T
 
 def weakening {T U : Set F} {f : F} (b : T ⊢ f) (ss : T ⊆ U) : U ⊢ f := weakening' ss b
 
-lemma Consistent.of_subset {T U : Set F} (h : Consistent U) (ss : T ⊆ U) : Consistent T := ⟨fun b => h.false (weakening b ss)⟩
+lemma weakening! {T U : Set F} {f : F} (b : T ⊢! f) (ss : T ⊆ U) : U ⊢! f := by
+  rcases b with ⟨b⟩; exact ⟨weakening b ss⟩
 
-lemma inconsistent_of_proof {T : Set F} (b : T ⊢ ⊥) : ¬Consistent T := by simp[Consistent]; exact ⟨b⟩
+lemma Consistent.of_subset {T U : Set F} (h : Consistent U) (ss : T ⊆ U) : Consistent T := fun b ↦ h (weakening! b ss)
 
-lemma inconsistent_of_provable {T : Set F} (b : T ⊢! ⊥) : ¬Consistent T := by simp[Consistent]
+lemma inconsistent_of_proof {T : Set F} (b : T ⊢ ⊥) : ¬Consistent T := by simp [Consistent, Deduction.Consistent, Deduction.Undeducible]; exact ⟨b⟩
+
+lemma inconsistent_of_provable {T : Set F} (b : T ⊢! ⊥) : ¬Consistent T := by simpa [Consistent, Deduction.Consistent, Deduction.Undeducible] using b
 
 lemma consistent_iff_unprovable {T : Set F} : Consistent T ↔ T ⊬ ⊥ := by rfl
 
+lemma inconsistent_iff_provable_falsum {T : Set F} : ¬Consistent T ↔ T ⊢! ⊥ := by
+  simp [Consistent, Deduction.Consistent, Deduction.Undeducible]
+
+lemma Consistent.falsum_not_mem {T : Set F} (h : Consistent T) : ⊥ ∉ T := fun b ↦
+    System.unprovable_iff_not_provable.mp (System.consistent_iff_unprovable.mp h) ⟨LO.Deduction.axm b⟩
+
 protected def Complete (T : Set F) : Prop := ∀ f, (T ⊢! f) ∨ (T ⊢! ~f)
 
 def Independent (T : Set F) (f : F) : Prop := T ⊬ f ∧ T ⊬ ~f
 
 lemma incomplete_iff_exists_independent {T : Set F} :
-    ¬System.Complete T ↔ ∃ f, Independent T f := by simp[System.Complete, not_or, Independent]
+    ¬System.Complete T ↔ ∃ f, Independent T f := by simp [System.Complete, not_or, Independent, Unprovable, Undeducible]
 
 def theory (T : Set F) : Set F := {p | T ⊢! p}
 
@@ -147,8 +161,7 @@ variable {a : α}
 lemma sound! {T : Set F} {f : F} : T ⊢! f → T ⊨ f := by rintro ⟨b⟩; exact sound b
 
 lemma not_provable_of_countermodel {T : Set F} {p : F}
-  (hT : a ⊧* T) (hp : ¬a ⊧ p) : IsEmpty (T ⊢ p) :=
-  ⟨fun b => by have : a ⊧ p := Sound.sound b hT; contradiction⟩
+  (hT : a ⊧* T) (hp : ¬a ⊧ p) : T ⊬ p := fun b ↦ hp (Sound.sound! b hT)
 
 lemma consistent_of_model {T : Set F}
   (hT : a ⊧* T) : System.Consistent T :=
@@ -183,7 +196,7 @@ lemma satisfiableTheory_iff_consistent {T : Set F} : Semantics.SatisfiableTheory
       exact System.inconsistent_of_proof this⟩
 
 lemma not_satisfiable_iff_inconsistent {T : Set F} : ¬Semantics.SatisfiableTheory T ↔ T ⊢! ⊥ := by
-  simp[satisfiableTheory_iff_consistent, System.Consistent]
+  simp [satisfiableTheory_iff_consistent, System.Consistent, Deduction.Consistent, Deduction.Undeducible]
 
 lemma consequence_iff_provable {T : Set F} {f : F} : T ⊨ f ↔ T ⊢! f :=
 ⟨fun h => ⟨complete h⟩, by rintro ⟨b⟩; exact Sound.sound b⟩

Logic/Modal/Normal.lean

@@ -1,4 +1,4 @@
-import Logic.Modal.Normal.LogicalConnective
+import Logic.Modal.Normal.LogicSymbol
 import Logic.Modal.Normal.Formula
 import Logic.Modal.Normal.Axioms
 import Logic.Modal.Normal.HilbertStyle