refactor: fix Kreisel spelling throughout codebase

Foundation.lean

@@ -441,7 +441,7 @@ public import Foundation.Propositional.Entailment.Corsi.WF
 public import Foundation.Propositional.Entailment.Int.Basic
 public import Foundation.Propositional.Entailment.Int.DNE_of_LEM
 public import Foundation.Propositional.Entailment.KC
-public import Foundation.Propositional.Entailment.KrieselPutnam
+public import Foundation.Propositional.Entailment.KreiselPutnam
 public import Foundation.Propositional.Entailment.LC
 public import Foundation.Propositional.Entailment.Minimal.Basic
 public import Foundation.Propositional.Entailment.Scott
@@ -471,7 +471,7 @@ public import Foundation.Propositional.Hilbert.WF
 public import Foundation.Propositional.Hilbert.WF.Basic
 public import Foundation.Propositional.Hilbert.WF_VF
 public import Foundation.Propositional.Kripke.AxiomDummett
-public import Foundation.Propositional.Kripke.AxiomKrieselPutnam
+public import Foundation.Propositional.Kripke.AxiomKreiselPutnam
 public import Foundation.Propositional.Kripke.AxiomLEM
 public import Foundation.Propositional.Kripke.AxiomWLEM
 public import Foundation.Propositional.Kripke.Basic
@@ -481,7 +481,7 @@ public import Foundation.Propositional.Kripke.Hilbert
 public import Foundation.Propositional.Kripke.Logic.Cl
 public import Foundation.Propositional.Kripke.Logic.Int
 public import Foundation.Propositional.Kripke.Logic.KC
-public import Foundation.Propositional.Kripke.Logic.KrieselPutnam
+public import Foundation.Propositional.Kripke.Logic.KreiselPutnam
 public import Foundation.Propositional.Kripke.Logic.LC
 public import Foundation.Propositional.Kripke.Preservation
 public import Foundation.Propositional.Kripke.Rooted

Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean

@@ -366,7 +366,7 @@ theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T)
 
 omit [Diagonalization T₀] [Consistent T] in
 /-- If `𝔅` satisfies Rosser provability condition, then `𝔅.con` is provable from `T`. -/
-theorem kriesel_remark [𝔅.Rosser] : T ⊢ 𝔅.con := by
+theorem kreisel_remark [𝔅.Rosser] : T ⊢ 𝔅.con := by
   have : T₀ ⊢ ∼𝔅 ⊥ := Ros (N!_iff_CO!.mpr (by simp));
   exact WeakerThan.pbl $ this;
 

Foundation/Propositional/Entailment/KreiselPutnam.lean

@@ -0,0 +1,62 @@
+module
+public import Foundation.Propositional.Entailment.Int.Basic
+
+@[expose] public section
+
+namespace LO.Axioms
+
+variable {F : Type*} [LogicalConnective F]
+variable (φ ψ χ : F)
+
+protected abbrev KreiselPutnam :=  (∼φ ➝ ψ ⋎ χ) ➝ (∼φ ➝ ψ) ⋎ (∼φ ➝ χ)
+
+end LO.Axioms
+
+
+namespace LO.Entailment
+
+variable {S F : Type*} [LogicalConnective F] [Entailment S F]
+variable {𝓢 : S} {φ ψ χ : F}
+
+class HasAxiomKreiselPutnam (𝓢 : S)  where
+  kreiselputnam {φ ψ χ : F} : 𝓢 ⊢! Axioms.KreiselPutnam φ ψ χ
+export HasAxiomKreiselPutnam (kreiselputnam)
+
+@[simp] lemma kreiselputnam! [HasAxiomKreiselPutnam 𝓢] : 𝓢 ⊢ Axioms.KreiselPutnam φ ψ χ := ⟨kreiselputnam⟩
+
+section
+
+variable [ModusPonens 𝓢] [HasAxiomKreiselPutnam 𝓢]
+
+def kreiselputnam' (h : 𝓢 ⊢! (∼φ ➝ ψ ⋎ χ)) : 𝓢 ⊢! (∼φ ➝ ψ) ⋎ (∼φ ➝ χ) := kreiselputnam ⨀ h
+lemma kreiselputnam'! (h : 𝓢 ⊢ (∼φ ➝ ψ ⋎ χ)) : 𝓢 ⊢ (∼φ ➝ ψ) ⋎ (∼φ ➝ χ) := ⟨kreiselputnam' h.some⟩
+
+end
+
+
+section
+
+variable [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢]
+
+namespace FiniteContext
+
+instance [Entailment.HasAxiomKreiselPutnam 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomKreiselPutnam Γ := ⟨of kreiselputnam⟩
+
+end FiniteContext
+
+
+namespace Context
+
+instance [Entailment.HasAxiomKreiselPutnam 𝓢] (Γ : Context F 𝓢) : HasAxiomKreiselPutnam Γ := ⟨of kreiselputnam⟩
+
+end Context
+
+end
+
+
+protected class KreiselPutnam (𝓢 : S) extends Entailment.Int 𝓢, HasAxiomKreiselPutnam 𝓢
+
+
+end LO.Entailment
+
+end

Foundation/Propositional/Hilbert/Axiom.lean

@@ -1,7 +1,7 @@
 module
 
 public import Foundation.Propositional.Formula.Basic
-public import Foundation.Propositional.Entailment.KrieselPutnam
+public import Foundation.Propositional.Entailment.KreiselPutnam
 public import Foundation.Propositional.Entailment.Scott
 public import Foundation.Propositional.Entailment.Corsi
 
@@ -41,14 +41,14 @@ class HasPeirce (Ax : Axiom α) where
   ne_pq : p ≠ q := by trivial;
   mem_peirce : Axioms.Peirce (.atom p) (.atom q) ∈ Ax := by tauto;
 
-class HasKrieselPutnam (Ax : Axiom α) where
+class HasKreiselPutnam (Ax : Axiom α) where
   p : α
   q : α
   r : α
   ne_pq : p ≠ q := by trivial;
   ne_qr : q ≠ r := by trivial;
   ne_rp : r ≠ p := by trivial;
-  mem_kriesel_putnam : Axioms.KrieselPutnam (.atom p) (.atom q) (.atom r) ∈ Ax := by tauto;
+  mem_kreisel_putnam : Axioms.KreiselPutnam (.atom p) (.atom q) (.atom r) ∈ Ax := by tauto;
 
 class HasScott (Ax : Axiom α) where
   p : α

Foundation/Propositional/Hilbert/Standard/Basic.lean

@@ -183,17 +183,17 @@ instance [Ax.HasPeirce] : Entailment.HasAxiomPeirce (Hilbert.Standard Ax) where
         else (.atom b))
       $ (HasPeirce.mem_peirce);
 
-instance [Ax.HasKrieselPutnam] : Entailment.HasAxiomKrieselPutnam (Hilbert.Standard Ax) where
-  krieselputnam {φ ψ χ} := by
+instance [Ax.HasKreiselPutnam] : Entailment.HasAxiomKreiselPutnam (Hilbert.Standard Ax) where
+  kreiselputnam {φ ψ χ} := by
     constructor;
-    simpa [HasKrieselPutnam.ne_pq, HasKrieselPutnam.ne_qr, HasKrieselPutnam.ne_rp.symm] using axm
-      (φ := Axioms.KrieselPutnam (.atom (HasKrieselPutnam.p Ax)) (.atom (HasKrieselPutnam.q Ax)) (.atom (HasKrieselPutnam.r Ax)))
+    simpa [HasKreiselPutnam.ne_pq, HasKreiselPutnam.ne_qr, HasKreiselPutnam.ne_rp.symm] using axm
+      (φ := Axioms.KreiselPutnam (.atom (HasKreiselPutnam.p Ax)) (.atom (HasKreiselPutnam.q Ax)) (.atom (HasKreiselPutnam.r Ax)))
       (s := λ b =>
-        if (HasKrieselPutnam.p Ax) = b then φ
-        else if (HasKrieselPutnam.q Ax) = b then ψ
-        else if (HasKrieselPutnam.r Ax) = b then χ
+        if (HasKreiselPutnam.p Ax) = b then φ
+        else if (HasKreiselPutnam.q Ax) = b then ψ
+        else if (HasKreiselPutnam.r Ax) = b then χ
         else (.atom b))
-      $ (HasKrieselPutnam.mem_kriesel_putnam);
+      $ (HasKreiselPutnam.mem_kreisel_putnam);
 
 end
 
@@ -236,13 +236,13 @@ protected abbrev LC := Hilbert.Standard LC.axioms
 instance : Entailment.LC Propositional.LC where
 
 
-protected abbrev KrieselPutnam.axioms : Axiom ℕ := {Axioms.EFQ (.atom 0), Axioms.KrieselPutnam (.atom 0) (.atom 1) (.atom 2)}
-namespace KrieselPutnam.axioms
-instance : KrieselPutnam.axioms.HasEFQ where p := 0;
-instance : KrieselPutnam.axioms.HasKrieselPutnam where p := 0; q := 1; r := 2;
-end KrieselPutnam.axioms
-protected abbrev KrieselPutnam := Hilbert.Standard KrieselPutnam.axioms
-instance : Entailment.KrieselPutnam Propositional.KrieselPutnam where
+protected abbrev KreiselPutnam.axioms : Axiom ℕ := {Axioms.EFQ (.atom 0), Axioms.KreiselPutnam (.atom 0) (.atom 1) (.atom 2)}
+namespace KreiselPutnam.axioms
+instance : KreiselPutnam.axioms.HasEFQ where p := 0;
+instance : KreiselPutnam.axioms.HasKreiselPutnam where p := 0; q := 1; r := 2;
+end KreiselPutnam.axioms
+protected abbrev KreiselPutnam := Hilbert.Standard KreiselPutnam.axioms
+instance : Entailment.KreiselPutnam Propositional.KreiselPutnam where
 
 
 end LO.Propositional

Foundation/Propositional/Kripke/AxiomKrieselPutnam.lean → Foundation/Propositional/Kripke/AxiomKreiselPutnam.lean

@@ -1,7 +1,7 @@
 module
 
 public import Foundation.Propositional.Kripke.Completeness
-public import Foundation.Propositional.Entailment.KrieselPutnam
+public import Foundation.Propositional.Entailment.KreiselPutnam
 
 @[expose] public section
 
@@ -12,19 +12,19 @@ open Formula.Kripke
 
 namespace Kripke
 
-protected class Frame.SatisfiesKriselPutnamCondition (F : Frame) where
-  kriesel_putnam :
+protected class Frame.SatisfiesKreiselPutnamCondition (F : Frame) where
+  kreisel_putnam :
     ∀ x y z : F,
     (x ≺ y ∧ x ≺ z ∧ ¬y ≺ z ∧ ¬z ≺ y) →
     (∃ u, x ≺ u ∧ u ≺ y ∧ u ≺ z ∧ (∀ v, u ≺ v → ∃ w, v ≺ w ∧ (y ≺ w ∨ z ≺ w)))
 
-lemma Frame.kriesel_putnam {F : Frame} [F.SatisfiesKriselPutnamCondition] :
+lemma Frame.kreisel_putnam {F : Frame} [F.SatisfiesKreiselPutnamCondition] :
   ∀ x y z : F,
   (x ≺ y ∧ x ≺ z ∧ ¬y ≺ z ∧ ¬z ≺ y) →
   (∃ u, x ≺ u ∧ u ≺ y ∧ u ≺ z ∧ (∀ v, u ≺ v → ∃ w, v ≺ w ∧ (y ≺ w ∨ z ≺ w))) :=
-  SatisfiesKriselPutnamCondition.kriesel_putnam
+  SatisfiesKreiselPutnamCondition.kreisel_putnam
 
-instance : whitepoint.SatisfiesKriselPutnamCondition := ⟨by simp⟩
+instance : whitepoint.SatisfiesKreiselPutnamCondition := ⟨by simp⟩
 
 
 section definability
@@ -33,7 +33,7 @@ variable {F : Kripke.Frame}
 
 open Formula (atom)
 
-lemma validate_axiomKrieselPutnam_of_satisfiesKrieselPutnamCondition [F.SatisfiesKriselPutnamCondition ] : F ⊧ (Axioms.KrieselPutnam (.atom 0) (.atom 1) (.atom 2)) := by
+lemma validate_axiomKreiselPutnam_of_satisfiesKreiselPutnamCondition [F.SatisfiesKreiselPutnamCondition ] : F ⊧ (Axioms.KreiselPutnam (.atom 0) (.atom 1) (.atom 2)) := by
   intro V x y Rxy h₁;
   by_contra hC;
   replace hC := Satisfies.or_def.not.mp hC;
@@ -48,7 +48,7 @@ lemma validate_axiomKrieselPutnam_of_satisfiesKrieselPutnamCondition [F.Satisfie
   push_neg at h₃;
   obtain ⟨z₂, Ryz₂, ⟨hz₂₁, hz₂₂⟩⟩ := h₃;
 
-  obtain ⟨u, Ryu, ⟨Ruz₁, Ruz₂, h⟩⟩ := F.kriesel_putnam y z₁ z₂ ⟨
+  obtain ⟨u, Ryu, ⟨Ruz₁, Ruz₂, h⟩⟩ := F.kreisel_putnam y z₁ z₂ ⟨
     Ryz₁, Ryz₂,
     by
       rcases Satisfies.or_def.mp $ h₁ Ryz₁ hz₁₁ with (h | h);
@@ -91,7 +91,7 @@ open Classical
 
 namespace Canonical
 
-instance [Entailment.HasAxiomKrieselPutnam 𝓢] : (canonicalFrame 𝓢).SatisfiesKriselPutnamCondition := ⟨by
+instance [Entailment.HasAxiomKreiselPutnam 𝓢] : (canonicalFrame 𝓢).SatisfiesKreiselPutnamCondition := ⟨by
   rintro x y z ⟨Rxy, Rxz, nRyz, nRzy⟩;
   let ΓNyz := { φ | ∼φ ∈ (y.1.1 ∩ z.1.1)}.image (∼·);
   obtain ⟨u, hu₁, hu₂⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := ⟨x.1.1 ∪ ΓNyz, y.1.2 ∪ z.1.2⟩) $ by
@@ -108,7 +108,7 @@ instance [Entailment.HasAxiomKrieselPutnam 𝓢] : (canonicalFrame 𝓢).Satisfi
       generalize eδz : Δz.disj = δz at hC;
       replace hC : ↑Γx *⊢[𝓢] ∼(Γ₂.disj) ➝ δy ⋎ δz := C!_trans ?_ $ FConj_DT.mp $ CK!_iff_CC!.mp hC;
       . generalize eγ : Γ₂.disj = γ at hC;
-        replace hC : ↑Γx *⊢[𝓢] (∼γ ➝ δy) ⋎ (∼γ ➝ δz) := krieselputnam'! hC;
+        replace hC : ↑Γx *⊢[𝓢] (∼γ ➝ δy) ⋎ (∼γ ➝ δz) := kreiselputnam'! hC;
         replace hC : ∼γ ➝ δy ∈ x.1.1 ∨ ∼γ ➝ δz ∈ x.1.1 := iff_mem₁_or.mp $ iff_provable_include₁.mp hC x ?_;
         . rcases hC with h | h;
           . apply iff_not_mem₂_mem₁.mpr $ of_mem₁_imp' (Rxy h) ?_

Foundation/Propositional/Kripke/Logic/Cl.lean

@@ -24,7 +24,7 @@ instance : whitepoint.IsEuclidean := ⟨by tauto⟩
 protected abbrev FrameClass.Cl : FrameClass := { F | F.IsCl }
 protected abbrev FrameClass.finite_Cl : FrameClass := { F | F.IsFiniteCl }
 
-instance [F.IsCl] : F.IsKrieselPutnam := ⟨by
+instance [F.IsCl] : F.IsKreiselPutnam := ⟨by
   rintro x y z ⟨Rxy, Rxz, Ryz, _⟩;
   exfalso;
   apply Ryz;

Foundation/Propositional/Kripke/Logic/KC.lean

@@ -2,7 +2,7 @@ module
 
 public import Foundation.Propositional.Kripke.AxiomWLEM
 public import Foundation.Propositional.Kripke.Rooted
-public import Foundation.Propositional.Kripke.Logic.KrieselPutnam
+public import Foundation.Propositional.Kripke.Logic.KreiselPutnam
 
 
 @[expose] public section
@@ -24,7 +24,7 @@ protected class Frame.IsFiniteKC (F : Frame) extends F.IsFinite, F.IsKC
 protected abbrev FrameClass.KC : FrameClass := { F | F.IsPiecewiseStronglyConvergent }
 protected abbrev FrameClass.finite_KC : FrameClass := { F | F.IsFiniteKC }
 
-instance [F.IsKC] : F.IsKrieselPutnam := ⟨by
+instance [F.IsKC] : F.IsKreiselPutnam := ⟨by
   rintro x y z ⟨Rxy, Rxz, nRyz, nRzy⟩;
   use x;
   refine ⟨F.refl, Rxy, Rxz, ?_⟩;
@@ -136,17 +136,17 @@ end FFP
 end KC
 
 
-instance : Propositional.KrieselPutnam ⪱ Propositional.KC := by
+instance : Propositional.KreiselPutnam ⪱ Propositional.KC := by
   constructor;
-  . apply weakerThan_of_subset_frameClass FrameClass.KrieselPutnam FrameClass.KC;
+  . apply weakerThan_of_subset_frameClass FrameClass.KreiselPutnam FrameClass.KC;
     intro F hF;
     simp_all only [Set.mem_setOf_eq];
     infer_instance
   . apply Entailment.not_weakerThan_iff.mpr;
     use Axioms.WLEM (.atom 0);
     constructor;
     . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.KrieselPutnam)
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.KreiselPutnam)
       apply not_validOnFrameClass_of_exists_frame;
       let F : Frame := {
         World := Fin 3,
@@ -160,7 +160,7 @@ instance : Propositional.KrieselPutnam ⪱ Propositional.KC := by
       use F;
       constructor;
       . refine {
-          kriesel_putnam := by
+          kreisel_putnam := by
             rintro x y z ⟨Rxy, Rxz, nRyz, nRzy⟩;
             match x, y, z with
             | 0, 1, 2
@@ -187,7 +187,7 @@ instance : Propositional.KrieselPutnam ⪱ Propositional.KC := by
         omega;
 
 instance : Propositional.Int ⪱ Propositional.KC := calc
-  Propositional.Int ⪱ Propositional.KrieselPutnam := inferInstance
+  Propositional.Int ⪱ Propositional.KreiselPutnam := inferInstance
   _   ⪱ Propositional.KC := inferInstance
 
 end LO.Propositional