wip

Author: SnO2WMaN

Foundation/Propositional/ConsistentTableau.lean

@@ -124,7 +124,6 @@ lemma ruleC_fconj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢
   simpa;
 
 
-
 lemma mem_lconj₂ {Γ : List F} (h : φ ∈ Γ) : 𝓢 ⊢ ⋀Γ 🡒 φ := by
   induction Γ using List.induction_with_singleton with
   | hcons ψ Δ he ih =>
@@ -191,6 +190,10 @@ lemma mem_ldisj₂ {Γ : List F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj₂ :
       exact orIntroR;
   | _ => simp_all;
 
+lemma mem_fdisj {Γ : Finset F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj := by
+  apply mem_ldisj₂;
+  simpa using h;
+
 lemma mem_fdisj' {Γ : Finset ι} (Φ : ι → F) (hΦ : ∃ i ∈ Γ, Φ i = ψ) : 𝓢 ⊢ ψ 🡒 ⩖ i ∈ Γ, Φ i := by
   apply mem_ldisj₂;
   simpa;
@@ -212,6 +215,26 @@ lemma ruleD_fdisj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢
   simpa;
 
 
+lemma CLDisj₂Disj₂_of_provable {Γ : List F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ γ 🡒 δ) : 𝓢 ⊢ Γ.disj₂ 🡒 δ := by
+  induction Γ using List.induction_with_singleton with
+  | hnil => simp only [List.disj₂_nil, Entailment.efq!];
+  | hsingle φ => apply h; simp;
+  | hcons ψ Δ he ih =>
+    simp only [List.disj₂_cons_nonempty he];
+    simp only [List.mem_cons, forall_eq_or_imp] at h;
+    apply ruleD;
+    . apply h.1;
+    . apply ih h.2;
+
+lemma CLDisj₂Disj₂_of_subset {Γ Δ : List F} (h : ∀ φ, φ ∈ Γ → φ ∈ Δ) : 𝓢 ⊢ Γ.disj₂ 🡒 Δ.disj₂ := by
+  apply CLDisj₂Disj₂_of_provable;
+  intro γ hγ;
+  apply mem_ldisj₂ $ h _ hγ;
+
+lemma CFDisjFDisj_of_subset {Γ Δ : Finset F} (h : Γ ⊆ Δ) : 𝓢 ⊢ Γ.disj 🡒 Δ.disj := by
+  apply CLDisj₂Disj₂_of_subset;
+  simpa;
+
 
 variable [Entailment.Disjunctive 𝓢] [Entailment.Consistent 𝓢]
 

Foundation/Propositional/Entailment/Corsi/VF.lean

@@ -86,7 +86,7 @@ instance [Entailment.HasAxiomDummett 𝓢] : IsPiecewiseStronglyConnected (canon
   by_contra!;
   obtain ⟨φ, hφy, hφz⟩ := Set.not_subset.mp this.1;
   obtain ⟨ψ, hψz, hψy⟩ := Set.not_subset.mp this.2;
-  rcases (show φ ➝ ψ ∈ x.1.1 ∨ ψ ➝ φ ∈ x.1.1 by exact iff_mem₁_or.mp $ mem₁_of_provable dummett!) with (hφψx | hψφx);
+  rcases (show φ 🡒 ψ ∈ x.1.1 ∨ ψ 🡒 φ ∈ x.1.1 by exact iff_mem₁_or.mp $ mem₁_of_provable dummett!) with (hφψx | hψφx);
   . exact hψy $ mdp₁_mem hφy (Rxy hφψx);
   . exact hφz $ mdp₁_mem hψz (Rxz hψφx);
 

Foundation/Propositional/Kripke3/Axiom/Dummett.lean

@@ -92,14 +92,14 @@ instance [Entailment.HasAxiomKreiselPutnam 𝓢] : (canonicalKripkeModel 𝓢).K
     let Γ₂ := Γ₁.preimage (∼·) $ by simp [Set.InjOn];
     let Δy := { φ ∈ Δ | φ ∈ y.1.2};
     let Δz := { φ ∈ Δ | φ ∈ z.1.2};
-    replace hC : 𝓢 ⊢ (Γx ∪ Γ₁).conj ➝ (Δy ∪ Δz).disj := C!_replace ?_ ?_ hC;
-    . replace hC : 𝓢 ⊢ Γx.conj ⋏ Γ₁.conj ➝ Δy.disj ⋎ Δz.disj := C!_replace CKFconjFconjUnion! CFdisjUnionAFdisj hC;
+    replace hC : 𝓢 ⊢ (Γx ∪ Γ₁).conj 🡒 (Δy ∪ Δz).disj := C!_replace ?_ ?_ hC;
+    . replace hC : 𝓢 ⊢ Γx.conj ⋏ Γ₁.conj 🡒 Δy.disj ⋎ Δz.disj := C!_replace CKFconjFconjUnion! CFdisjUnionAFdisj hC;
       generalize eδy : Δy.disj = δy at hC;
       generalize eδz : Δz.disj = δz at hC;
-      replace hC : ↑Γx *⊢[𝓢] ∼(Γ₂.disj) ➝ δy ⋎ δz := C!_trans ?_ $ FConj_DT.mp $ CK!_iff_CC!.mp 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) := kreiselputnam'! hC;
-        replace hC : ∼γ ➝ δy ∈ x.1.1 ∨ ∼γ ➝ δz ∈ x.1.1 := iff_mem₁_or.mp $ iff_provable_include₁.mp hC x ?_;
+        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) ?_
             . subst eδy;

Foundation/Propositional/Kripke3/Axiom/KreiselPutnam.lean

@@ -85,7 +85,7 @@ instance [Entailment.HasAxiomWLEM 𝓢] : IsPiecewiseStronglyConvergent (canonic
     let Θz := { φ ∈ Γ | φ ∈ z.1.1 ∧ φ ∉ x.1.1 };
 
     simp only [Finset.disj_empty] at h;
-    replace : [Θx.conj] ⊢[𝓢] ∼∼Θz.conj ➝ ∼Θy.conj := contra! $ FiniteContext.deductInv'! $ by
+    replace : [Θx.conj] ⊢[𝓢] ∼∼Θz.conj 🡒 ∼Θy.conj := contra! $ FiniteContext.deductInv'! $ by
       apply FConj_DT.mpr;
       apply FConj_DT'.mpr;
       apply FConj_DT'.mpr;

Foundation/Propositional/Kripke3/Axiom/WLEM.lean

@@ -44,7 +44,7 @@ def Forces (M : KripkeModel κ α) (x : M.world) : Formula α → Prop
   | ⊥      => False
   | φ ⋏ ψ  => Forces M x φ ∧ Forces M x ψ
   | φ ⋎ ψ  => Forces M x φ ∨ Forces M x ψ
-  | φ ➝ ψ => ∀ y : M.world, x ≺ y → (Forces M y φ → Forces M y ψ)
+  | φ 🡒 ψ => ∀ y : M.world, x ≺ y → (Forces M y φ → Forces M y ψ)
 
 instance : ForcingRelation M.world (Formula α) where
   Forces := Forces M
@@ -54,7 +54,7 @@ instance : ForcingRelation M.world (Formula α) where
 @[simp, grind .] lemma forces_verum : x ⊩ ⊤ := by tauto;
 @[grind =] lemma forces_and : x ⊩ φ ⋏ ψ ↔ x ⊩ φ ∧ x ⊩ ψ := by rfl;
 @[grind =] lemma forces_or : x ⊩ φ ⋎ ψ ↔ x ⊩ φ ∨ x ⊩ ψ := by rfl;
-@[grind =] lemma forces_imp : x ⊩ φ ➝ ψ ↔ ∀ y : M.world, x ≺ y → (y ⊩ φ → y ⊩ ψ) := by rfl;
+@[grind =] lemma forces_imp : x ⊩ φ 🡒 ψ ↔ ∀ y : M.world, x ≺ y → (y ⊩ φ → y ⊩ ψ) := by rfl;
 
 @[grind =]
 lemma forces_neg : x ⊩ ∼φ ↔ ∀ y, x ≺ y → (y ⊮ φ) := by
@@ -187,7 +187,7 @@ attribute [grind .]
 lemma validates_ruleC (hφ : M ⊧ φ) (hψ : M ⊧ ψ) : M ⊧ φ ⋏ ψ := fun x ↦ ⟨hφ x, hψ x⟩
 
 @[grind <=]
-lemma validates_afortiori (h : M ⊧ φ) : M ⊧ ψ ➝ φ := fun _ y _ _ ↦ h y
+lemma validates_afortiori (h : M ⊧ φ) : M ⊧ ψ 🡒 φ := fun _ y _ _ ↦ h y
 
 end Models
 
@@ -208,7 +208,7 @@ lemma formula_persistency [Persistent M] [IsTrans _ M.rel] {x y : M.world} {φ :
   | _ => grind;
 
 @[grind .]
-lemma validates_implyK [Persistent M] [IsTrans _ M.rel] : M ⊧ φ ➝ ψ ➝ φ := by
+lemma validates_implyK [Persistent M] [IsTrans _ M.rel] : M ⊧ φ 🡒 ψ 🡒 φ := by
   intro x y Rxy hφ z Ryz hψ;
   apply formula_persistency hφ Ryz;
 
@@ -219,7 +219,7 @@ lemma validates_implyS [IsTrans _ M.rel] [Std.Refl M.rel] : M ⊧ Axioms.ImplyS
   have Rww : w ≺ w := Std.Refl.refl _;
   exact hφψχ _ Ryw hφ _ Rww (hφψ _ Rzw hφ);
 
-lemma validates_mdp_of_reflexive [Std.Refl M.rel] (hφψ : M ⊧ φ ➝ ψ) (hφ : M ⊧ φ) : M ⊧ ψ := by
+lemma validates_mdp_of_reflexive [Std.Refl M.rel] (hφψ : M ⊧ φ 🡒 ψ) (hφ : M ⊧ φ) : M ⊧ ψ := by
   intro x;
   apply hφψ x;
   . apply Std.Refl.refl;
@@ -229,9 +229,6 @@ class Intuitionistic (M : KripkeModel κ α) extends Std.Refl M.rel, IsTrans _ M
 
 end
 
-
-def logic (M : KripkeModel κ α) : Logic α := { φ | M ⊧ φ }
-
 end KripkeModel
 
 

Foundation/Propositional/Kripke3/Basic.lean

@@ -60,7 +60,7 @@ lemma truthlemma : t ⊩ φ ↔ φ ∈ t.1.1 := by
       obtain ⟨t', ⟨h, _⟩⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := (insert φ t.1.1, {ψ})) $ by
         intro Γ Δ hΓ hΔ;
         by_contra hC;
-        apply t.consistent (Γ := Γ.erase φ) (Δ := {φ ➝ ψ}) ?_ ?_;
+        apply t.consistent (Γ := Γ.erase φ) (Δ := {φ 🡒 ψ}) ?_ ?_;
         . simp only [Finset.disj_singleton];
           apply FConj_DT.mpr;
           apply Context.deduct!
@@ -91,11 +91,11 @@ lemma truthlemma : t ⊩ φ ↔ φ ∈ t.1.1 := by
       have hpq := htt' h;
       apply ihq.mpr;
       apply iff_not_mem₂_mem₁.mp;
-      apply not_mem₂ (Γ := {φ, φ ➝ ψ});
+      apply not_mem₂ (Γ := {φ, φ 🡒 ψ});
       . simp only [Finset.coe_insert, Finset.coe_singleton];
         apply Set.doubleton_subset.mpr;
         tauto;
-      . suffices 𝓢 ⊢ Finset.conj {φ, φ ➝ ψ} ➝ Finset.disj {ψ} by simpa;
+      . suffices 𝓢 ⊢ Finset.conj {φ, φ 🡒 ψ} 🡒 Finset.disj {ψ} by simpa;
         apply Entailment.CFConj_CDisj!_of_innerMDP (φ := φ) (ψ := ψ) <;> simp;
 
 lemma iff_validates_provable : (canonicalKripkeModel 𝓢) ⊧ φ ↔ 𝓢 ⊢ φ := by