Theory GoedelVariantHOML1poss

section‹Appendix›
subsection‹GoedelVariantHOML1poss.thy (Figure 16 of \cite{J75})›
text‹Gödel's axioms and definitions, as presented in the 1970 manuscript, are inconsistent. 
In contrast to Figure 6 we here use only possibilist quantifiers and still derive falsity.›
theory GoedelVariantHOML1poss imports HOMLinHOL
begin 

consts PositiveProperty::"(e⇒σ)⇒σ" ("P") 

axiomatization where Ax1: "⌊P φ ❙∧ P ψ ❙⊃ P (φ ❙. ψ)⌋"

axiomatization where Ax2a: "⌊P φ ❙∨⇧e P ❙~φ⌋" 

definition God ("G") where "G x ≡ ❙∀φ. P φ ❙⊃ φ x"

abbreviation PropertyInclusion ("_❙⊃⇩N_") where "φ ❙⊃⇩N ψ ≡ ❙□(❙∀y::e. φ y ❙⊃ ψ y)"

definition Essence ("_Ess._") where "φ Ess. x ≡ ❙∀ψ. ψ x ❙⊃ (φ ❙⊃⇩N ψ)"

axiomatization where Ax2b: "⌊P φ ❙⊃ ❙□ P φ⌋"

lemma Ax2b': "⌊❙¬P φ ❙⊃ ❙□(❙¬P φ)⌋" using Ax2a Ax2b by blast

theorem Th1: "⌊G x ❙⊃ G Ess. x⌋" using Ax2a Ax2b Essence_def God_def by (smt (verit))

definition NecExist ("E") where "E x ≡ ❙∀φ. φ Ess. x ❙⊃ ❙□(❙∃x. φ x)"

axiomatization where Ax3: "⌊P E⌋"

theorem Th2: "⌊G x ❙⊃ ❙□(❙∃y. G y)⌋" using Ax3 Th1 God_def NecExist_def by smt

theorem Th3: "⌊❙◇(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" 
  ―‹sledgehammer(Th2 Rsymm)› ―‹Proof found›
  proof -
    have 1: "⌊(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" using Th2 by blast
    have 2: "⌊❙◇(❙∃x. G x) ❙⊃ ❙◇❙□(❙∃y. G y)⌋" using 1 by blast
    have 3: "⌊❙◇(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" using 2 Rsymm by blast
    thus ?thesis by blast
  qed

axiomatization where Ax4: "⌊P φ ❙∧ (φ ❙⊃⇩N ψ) ❙⊃ P ψ⌋"

lemma True nitpick[satisfy,expect=unknown] oops ―‹No model found›

lemma EmptyEssL: "⌊(λy.❙⊥) Ess. x⌋" using Essence_def by metis

theorem Inconsistency: False 
  ―‹sledgehammer(Ax2a Ax3 Ax4 EmptyEssL NecExist\_def)› ―‹Proof found›
  proof -
    have 1: "⌊❙¬(P (λx.❙⊥))⌋" using Ax2a Ax4 by blast
    have 2: "⌊P (λx.(λy.❙⊥) Ess. x ❙⊃ ❙□(❙∃z::e.(λy.❙⊥)z))⌋" using Ax3 Ax4 NecExist_def by smt
    have 3: "⌊P (λx.❙□(❙∃z. (λx.❙⊥) z))⌋" using 2 EmptyEssL Ax4 by smt
    have 4: "⌊P (λx.❙□❙⊥)⌋" using 3 by auto
    have 5: "⌊P (λx.❙⊥)⌋" using 4 Ax2a Ax4 by smt
    have 6: "⌊❙⊥⌋" using 1 5 by blast
    thus ?thesis by blast
  qed

end