Theory KanckosLethenNo2Possibilist

subsection‹Formal Study of Version No.2 of Gödel's Argument as 
  Reported by Kanckos and Lethen, 2019 \<^cite>‹"KanckosLethen19"› (Fig.~11 in \<^cite>‹"C85"›)›

theory KanckosLethenNo2Possibilist imports
  HOML 
  MFilter 
  BaseDefs
begin  
text‹Axioms of Version No. 2 \<^cite>‹"KanckosLethen19"›.›
abbreviation delta ("Δ") where "Δ A ≡ λx.(❙∀ψ. ((A ψ) ❙→ (ψ x)))"
abbreviation N ("𝒩") where "𝒩 φ ≡ λx.(❙□(φ x))"

axiomatization where 
  Axiom1: "⌊❙∀φ ψ.(((𝒫 φ) ❙∧ (❙□(❙∀x. ((φ x) ❙→ (ψ x))))) ❙→ (𝒫 ψ))⌋" and ―‹The ‹❙□› can be omitted here; the proofs still work.› 
  Axiom2: "⌊❙∀A .(❙□((❙∀φ.((A φ) ❙→  (𝒫 φ))) ❙→ (𝒫 (Δ A))))⌋" and  ―‹The ‹❙□› can be omitted here; the proofs still work.› 
  Axiom3: "⌊❙∀φ.((𝒫 φ) ❙→ (𝒫 (𝒩 φ)))⌋" and
  Axiom4: "⌊❙∀φ.((𝒫 φ) ❙→ (❙¬(𝒫(❙⇁φ))))⌋" and
  ―‹Logic S5› 
  axB:  "⌊❙∀φ.(φ ❙→ ❙□❙◇φ)⌋" and axM: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋" and ax4:  "⌊❙∀φ.((❙□φ) ❙→ (❙□❙□φ))⌋"

text‹Sahlqvist correspondences: they are better suited for proof automation.›
lemma axB': "∀x y. ¬(x❙ry) ∨ (y❙rx)" using axB by fastforce
lemma axM': "∀x. (x❙rx)" using axM by blast
lemma ax4': "∀x y z. (((x❙ry) ∧ (y❙rz)) ⟶ (x❙rz))" using ax4 by auto 

text‹Proofs for all theorems for No.2 from \<^cite>‹"KanckosLethen19"›.›
theorem Theorem0: "⌊❙∀φ ψ.((❙∀Q. ((Q φ)  ❙→ (Q ψ))) ❙→  ((𝒫 φ) ❙→ (𝒫  φ)))⌋" by auto ―‹not needed›
theorem Theorem1: "⌊𝒫 𝒢⌋"  unfolding G_def  using Axiom2 axM by blast
theorem Theorem2: "⌊❙∀x. ((𝒢 x)❙→(❙∃y. 𝒢 y))⌋" by blast  ―‹not needed›
theorem Theorem3a: "⌊𝒫 (λx. (❙∃y. 𝒢 y))⌋"  by (metis (no_types, lifting) Axiom1 Theorem1) 
theorem Theorem3b: "⌊❙□(𝒫 (λx.(❙□(❙∃y. 𝒢 y))))⌋" by (smt Axiom1 G_def Theorem3a  Axiom3 Theorem1 axB') 
theorem Theorem4: "⌊❙∀x. ❙□((𝒢 x) ❙→ ((𝒫 (λx.(❙□(❙∃y. 𝒢 y)))) ❙→  (❙□(❙∃y. 𝒢 y))))⌋" using G_def by fastforce ―‹not needed›
theorem Theorem5: "⌊❙∀x. ❙□((𝒢 x) ❙→ (❙□(❙∃y. 𝒢 y)))⌋" by (smt (verit) G_def Theorem3a Theorem3b)  ―‹not needed›
theorem Theorem6: "⌊❙□((❙∃y. 𝒢 y) ❙→ (❙□(❙∃y. 𝒢 y)))⌋" by (smt G_def Theorem3a Theorem3b) 
theorem Theorem7: "⌊❙□((❙◇(❙∃y. 𝒢 y)) ❙→ (❙□(❙∃y. 𝒢 y)))⌋" using Theorem6 axB' by blast
theorem Theorem8: "⌊❙□(❙∃y. 𝒢 y)⌋" by (metis Axiom1 Axiom4 Theorem1 Theorem7 axB')
theorem Theorem9: "⌊❙∀φ. ((𝒫 φ) ❙→ ❙◇(❙∃x. φ x))⌋" using Axiom1 Axiom4 axM' by metis

text‹Short proof of Theorem8; analogous to the one presented in Sec. 7 of Benzmüller 2020.›
theorem "⌊❙□(❙∃y. 𝒢 y)⌋" ―‹Note: this version of the proof uses only ‹axB'› and ‹axM'›.›
proof -
  have L1: "⌊(❙∃X.((𝒫 X)❙∧❙¬(❙∃X)))❙→(𝒫(λx.(x❙≠x)))⌋"  using Axiom1 Axiom3 axB' by blast  ―‹Use metis here if ‹❙□› is omitted in Axiom1 and Axiom 2›  
  have L2:  "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" using Axiom1 Axiom4 by metis
  have L3: "⌊❙¬(❙∃X.((𝒫 X) ❙∧ ❙¬(❙∃ X)))⌋" using L1 L2 by blast 
  have T2: "⌊𝒫 𝒢⌋" by (smt Axiom1 Axiom2 G_def axM')
  have T3: "⌊❙∃y. 𝒢 y⌋" using L3 T2 by blast
  have T6: "⌊❙□(❙∃y. 𝒢 y)⌋" by (simp add: T3)
  thus ?thesis by blast qed

theorem T5: "⌊(❙◇(❙∃y. 𝒢 y)) ❙→ ❙□(❙∃y. 𝒢 y)⌋" ―‹Obvious: If we can prove Theorem8, then we also have T5.›
proof -
  have L1: "⌊(❙∃X.((𝒫 X)❙∧❙¬(❙∃X)))❙→(𝒫(λx.(x❙≠x)))⌋"  using Axiom1 Axiom3 axB' by blast  ―‹Use metis here if ‹❙□› is omitted in Axiom1 and Axiom 2›  
  have L2:  "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" using Axiom1 Axiom4 by metis
  have L3: "⌊❙¬(❙∃X.((𝒫 X) ❙∧ ❙¬(❙∃ X)))⌋" using L1 L2 by blast 
  have T2: "⌊𝒫 𝒢⌋" by (smt Axiom1 Axiom2 G_def axM')
  have T3: "⌊❙∃y. 𝒢 y⌋" using L3 T2 by blast
  have T6: "⌊❙□(❙∃y. 𝒢 y)⌋" by (simp add: T3)
  thus ?thesis by blast qed

text‹Another short proof of Theorem8.›
theorem "⌊❙□(❙∃y. 𝒢 y)⌋"  ―‹Note: fewer assumptions used in some cases than in \cite{KanckosLethen19}.›
proof -
  have T1: "⌊𝒫 𝒢⌋"  unfolding G_def  using Axiom2 axM by blast
  have T3a: "⌊𝒫 (λx. (❙∃y. 𝒢 y))⌋" by (metis (no_types, lifting) Axiom1 T1)
  have T3b: "⌊❙□(𝒫 (λx.(❙□(❙∃y. 𝒢 y))))⌋" by (smt Axiom1 G_def T3a  Axiom3 T1 axB') 
  have T6: "⌊❙□((❙∃y. 𝒢 y) ❙→ (❙□(❙∃y. 𝒢 y)))⌋" by (smt G_def T3a T3b) 
  have T7: "⌊❙□((❙◇(❙∃y. 𝒢 y)) ❙→ (❙□(❙∃y. 𝒢 y)))⌋" using T6 axB' by blast
  thus ?thesis  by (smt Axiom1 Axiom4 T3b axB') qed

text‹Are the axioms of the simplified versions implied?›
text‹Actualist version of the axioms.›
lemma A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" using Theorem9 by blast
lemma A2': "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑Y)❙∨(X⇛Y))) ❙→ (𝒫 Y))⌋" nitpick oops  ―‹Countermodel›
lemma A3:  "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋" nitpick oops  ―‹Countermodel›

text‹Possibilist version of the axioms.›
abbreviation a ("_❙⊑⇧p_") where "X❙⊑⇧pY ≡ ❙∀z.((X z) ❙→ (Y z))"
abbreviation b ("_⇛⇧p_") where "X⇛⇧pY ≡ ❙□(X❙⊑⇧pY)"
abbreviation d ("_⨅⇧p_") where "X⨅⇧p𝒵 ≡ ❙□(❙∀u.((X u) ❙↔ (❙∀Y.((𝒵 Y) ❙→ (Y u)))))"

lemma A1'P: "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" using Theorem9 by blast
lemma A2'P: "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑⇧pY)❙∨(X⇛⇧pY))) ❙→ (𝒫 Y))⌋" oops ―‹no answer, yet by sledgehammer and nitpick›
lemma A2'aP: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X⇛⇧pY)) ❙→ (𝒫 Y))⌋" using Axiom1 axM' by metis
lemma A2'bP: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑⇧pY)) ❙→ (𝒫 Y))⌋" oops ―‹no answer, yet by sledgehammer and nitpick›
lemma A3P:  "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅⇧p𝒵) ❙→ (𝒫 X))))⌋" 
  by (smt (verit, del_insts) Axiom1 Axiom2 axM') ―‹proof found›

text‹Are Axiom2 and A3 equivalent? Only when assuming Axiom1 and axiom M.›
lemma  "⌊❙∀A .(❙□((❙∀φ.((A φ) ❙→  (𝒫 φ))) ❙→ (𝒫 (Δ A))))⌋ ≡ ⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅⇧p𝒵) ❙→ (𝒫 X))))⌋"
  by (smt (verit, ccfv_threshold) Axiom1 axM') ―‹proof found›
end