# Theory HOML

section‹Higher-Order Modal Logic in HOL (cf.~\cite{J23} and Fig.~1 in \cite{C85}).›

theory HOML imports Main
begin
nitpick_params[user_axioms,expect=genuine]

text‹Type i is associated with possible worlds and type e with entities:›
typedecl i ―‹Possible worlds›
typedecl e ―‹Individuals›
type_synonym σ = "i⇒bool" ―‹World-lifted propositions›
type_synonym γ = "e⇒σ" ―‹Lifted predicates›
type_synonym μ = "σ⇒σ" ―‹Unary modal connectives›
type_synonym ν = "σ⇒σ⇒σ" ―‹Binary modal connectives›

text‹Logical connectives (operating on truth-sets):›
abbreviation c1::σ ("❙⊥") where "❙⊥ ≡ λw. False"
abbreviation c2::σ ("❙⊤") where "❙⊤ ≡ λw. True"
abbreviation c3::μ ("❙¬_"[52]53) where "❙¬φ ≡ λw.¬(φ w)"
abbreviation c4::ν (infix"❙∧"50) where "φ❙∧ψ ≡ λw.(φ w)∧(ψ w)"
abbreviation c5::ν (infix"❙∨"49) where "φ❙∨ψ ≡ λw.(φ w)∨(ψ w)"
abbreviation c6::ν (infix"❙→"48) where "φ❙→ψ ≡ λw.(φ w)⟶(ψ w)"
abbreviation c7::ν (infix"❙↔"47) where "φ❙↔ψ ≡ λw.(φ w)⟷(ψ w)"
consts R::"i⇒i⇒bool" ("_❙r_")  ―‹Accessibility relation›
abbreviation c8::μ ("❙□_"[54]55) where "❙□φ ≡ λw.∀v.(w❙rv)⟶(φ v)"
abbreviation c9::μ ("❙◇_"[54]55) where "❙◇φ ≡ λw.∃v.(w❙rv)∧(φ v)"
abbreviation c10::"γ⇒γ" ("❙¬_"[52]53) where "❙¬Φ ≡ λx.λw.¬(Φ x w)"
abbreviation c11::"γ⇒γ" ("❙⇁_") where "❙⇁Φ ≡ λx.λw.¬(Φ x w)"
abbreviation c12::"e⇒e⇒σ" ("_❙=_") where "x❙=y ≡ λw.(x=y)"
abbreviation c13::"e⇒e⇒σ" ("_❙≠_") where "x❙≠y ≡ λw.(x≠y)"

text‹Polymorphic possibilist quantification:›
abbreviation q1::"('a⇒σ)⇒σ" ("❙∀") where "❙∀Φ ≡ λw.∀x.(Φ x w)"
abbreviation q2 (binder"❙∀"[10]11) where "❙∀x. φ(x) ≡ ❙∀φ"
abbreviation q3::"('a⇒σ)⇒σ" ("❙∃") where "❙∃Φ ≡ λw.∃x.(Φ x w)"
abbreviation q4 (binder"❙∃"[10]11) where "❙∃x. φ(x) ≡ ❙∃φ"

text‹Actualist quantification for individuals/entities:›
consts existsAt::γ ("_❙@_")
abbreviation q5::"γ⇒σ" ("❙∀⇧E") where "❙∀⇧EΦ ≡ λw.∀x.(x❙@w)⟶(Φ x w)"
abbreviation q6 (binder"❙∀⇧E"[8]9) where "❙∀⇧Ex. φ(x) ≡ ❙∀⇧Eφ"
abbreviation q7::"γ⇒σ" ("❙∃⇧E") where "❙∃⇧EΦ ≡ λw.∃x.(x❙@w)∧(Φ x w)"
abbreviation q8 (binder"❙∃⇧E"[8]9) where "❙∃⇧Ex. φ(x) ≡ ❙∃⇧Eφ"

text‹Meta-logical predicate for global validity:›
abbreviation g1::"σ⇒bool" ("⌊_⌋") where "⌊ψ⌋ ≡  ∀w. ψ w"

text‹Barcan and converse Barcan formula:›
lemma True nitpick[satisfy] oops  ―‹Model found by Nitpick›
lemma "⌊(❙∀⇧Ex.❙□(φ x)) ❙→ ❙□(❙∀⇧Ex.(φ x))⌋" nitpick oops ―‹Ctm›
lemma "⌊❙□(❙∀⇧Ex.(φ x)) ❙→ (❙∀⇧Ex.❙□(φ x))⌋" nitpick oops ―‹Ctm›
lemma "⌊(❙∀x.❙□(φ x)) ❙→ ❙□(❙∀x. φ x)⌋" by simp
lemma "⌊❙□(❙∀x.(φ x)) ❙→ (❙∀x.❙□(φ x))⌋" by simp
end


# Theory DisableKodkodScala

theory DisableKodkodScala
imports Main
begin

text ‹Some of the nitpick invocation within this AFP entry do not work,
if "Kodkod Scala" is enabled, i.e., if the box under
Plugin Options — Isabelle — General — Miscelleaneous Tools — Kodkod Scala
is activated. Therefore, in this theory we explicitly disable this configuration option.›

ML ‹
Options.default_put_bool \<^system_option>‹kodkod_scala› false
›

end

# Theory SimplifiedOntologicalArgument

section ‹Selected Simplified Ontological Argument \label{sec:selected}›

theory SimplifiedOntologicalArgument imports
HOML
DisableKodkodScala
begin
text ‹Positive properties:›
consts posProp::"γ⇒σ" ("𝒫")

text ‹An entity x is God-like if it possesses all positive properties.›
definition G ("𝒢") where "𝒢(x) ≡ ❙∀Φ.(𝒫(Φ) ❙→ Φ(x))"

text ‹The axiom's of the simplified variant are presented next; these axioms are further motivated in \cite{C85,J52}).›
text ‹Self-difference is not a positive property (possible alternative:
the empty property is not a positive property).›
axiomatization where CORO1: "⌊❙¬(𝒫(λx.(x❙≠x)))⌋"
text ‹A property entailed by a positive property is positive.›
axiomatization where CORO2: "⌊❙∀Φ Ψ. 𝒫(Φ) ❙∧ (❙∀x. Φ(x) ❙→ Ψ(x)) ❙→ 𝒫(Ψ)⌋"
text ‹Being Godlike is a positive property.›
axiomatization where AXIOM3: "⌊𝒫 𝒢⌋"

subsection‹Verifying the Selected Simplified Ontological Argument (version 1)›

text ‹The existence of a non-exemplified positive property implies that self-difference
(or, alternatively, the empty property) is a positive property.›
lemma LEMMA1: "⌊(❙∃Φ.(𝒫(Φ) ❙∧ ❙¬(❙∃x. Φ(x)))) ❙→ 𝒫(λx.(x❙≠x))⌋"
using CORO2 by meson
text ‹A non-exemplified positive property does not exist.›
lemma LEMMA2: "⌊❙¬(❙∃Φ.(𝒫(Φ) ❙∧ ❙¬(❙∃x. Φ(x))))⌋"
using CORO1 LEMMA1 by blast
text ‹Positive properties are exemplified.›
lemma LEMMA3: "⌊❙∀Φ.(𝒫(Φ) ❙→ (❙∃x. Φ(x)))⌋"
using LEMMA2 by blast
text ‹There exists a God-like entity.›
theorem THEOREM3': "⌊❙∃x. 𝒢(x)⌋"
using AXIOM3 LEMMA3 by auto
text ‹Necessarily, there exists a God-like entity.›
theorem THEOREM3: "⌊❙□(❙∃x. 𝒢(x))⌋"
using THEOREM3' by simp
text ‹However, the possible existence of Godlike entity is not implied.›
theorem CORO: "⌊❙◇(❙∃x. 𝒢(x))⌋"
nitpick oops (*Countermodel*)

subsection‹Verifying the Selected Simplified Ontological Argument (version 2)›

text ‹We switch to logic T.›
axiomatization where T: "⌊❙∀φ. ❙□φ ❙→ φ⌋"
lemma T': "⌊❙∀φ. φ ❙→ ❙◇φ⌋" using T by metis
text ‹Positive properties are possibly exemplified.›
theorem THEOREM1: "⌊❙∀Φ. 𝒫(Φ) ❙→ ❙◇(❙∃x. Φ(x))⌋"
using CORO1 CORO2 T' by metis
text ‹Possibly there exists a God-like entity.›
theorem CORO: "⌊❙◇(❙∃x. 𝒢(x))⌋"
using AXIOM3 THEOREM1 by auto
text ‹The possible existence of a God-like entity impplies the necessary  existence of a God-like entity.›
theorem THEOREM2: "⌊❙◇(❙∃x. 𝒢(x)) ❙→ ❙□(❙∃x. 𝒢(x))⌋"
using AXIOM3 CORO1 CORO2 by metis
text ‹Necessarily, there exists a God-like entity.›
theorem THEO3: "⌊❙□(❙∃x. 𝒢(x))⌋"
using CORO THEOREM2 by blast
text ‹There exists a God-like entity.›
theorem THEO3': "⌊❙∃x. 𝒢(x)⌋"
using T THEO3 by metis

text ‹Modal collapse is not implied; nitpick reports a countermodel.›

lemma MC: "⌊❙∀Φ. Φ ❙→ ❙□Φ⌋" nitpick oops

text ‹Consistency of the theory; nitpick reports a model.›
lemma True nitpick[satisfy] oops (*Model found*)
end



# Theory MFilter

section‹Presentation of All Variants as Studied in \cite{C85} \label{sec:all}›

subsection‹Preliminaries: Modal Ultrafilter (Fig.~2 in \cite{C85})›

theory MFilter imports HOML
begin
text‹Some abbreviations for auxiliary operations.›
abbreviation a::"γ⇒(γ⇒σ)⇒σ" ("_❙∈_") where "x❙∈S ≡ S x"
abbreviation b::γ ("❙∅") where "❙∅ ≡ λx. ❙⊥"
abbreviation c::γ ("❙U") where "❙U ≡ λx. ❙⊤"
abbreviation d::"γ⇒γ⇒σ" ("_❙⊆_") where "φ❙⊆ψ ≡ ❙∀x.((φ x) ❙→ (ψ x))"
abbreviation e::"γ⇒γ⇒γ" ("_❙⊓_") where "φ❙⊓ψ ≡ λx.((φ x) ❙∧ (ψ x))"
abbreviation f::"γ⇒γ" ("¯_") where "¯ψ ≡ λx. ❙¬(ψ x)"

text‹Definition of modal filter.›
abbreviation g::"(γ⇒σ)⇒σ" ("Filter")
where "Filter Φ ≡ (((❙U❙∈Φ) ❙∧ ❙¬(❙∅❙∈Φ))
❙∧ (❙∀φ ψ. (((φ❙∈Φ) ❙∧ (φ❙⊆ψ)) ❙→ (ψ❙∈Φ))))
❙∧ (❙∀φ ψ. (((φ❙∈Φ) ❙∧ (ψ❙∈Φ)) ❙→ ((φ❙⊓ψ)❙∈Φ)))"

text‹Definition of modal ultrafilter .›
abbreviation h::"(γ⇒σ)⇒σ" ("UFilter") where
"UFilter Φ ≡ (Filter Φ)❙∧(❙∀φ.((φ❙∈Φ) ❙∨ ((¯φ)❙∈Φ)))"

text‹Modal filter and modal ultrafilter are consistent.›
lemma "⌊❙∀Φ φ.((UFilter Φ) ❙→ ❙¬((φ❙∈Φ) ❙∧ ((¯φ)❙∈Φ)))⌋" by force
end



# Theory BaseDefs

subsection‹Preliminaries: Further Basic Notions (Fig.~3 in \cite{C85})›

theory BaseDefs imports HOML
begin
text‹Positive properties.›
consts posProp::"γ⇒σ" ("𝒫")

text‹Basic definitions for modal ontological argument.›
abbreviation a ("_❙⊑_") where "X❙⊑Y ≡ ❙∀⇧Ez.((X z) ❙→ (Y z))"
abbreviation b ("_⇛_") where "X⇛Y ≡ ❙□(X❙⊑Y)"
abbreviation c ("𝒫𝗈𝗌") where "𝒫𝗈𝗌 Z ≡ ❙∀X.((Z X) ❙→ (𝒫 X))"
abbreviation d ("_⨅_") where "X⨅𝒵 ≡ ❙□(❙∀⇧Eu.((X u) ❙↔ (❙∀Y.((𝒵 Y) ❙→ (Y u)))))"

text‹Definition of Godlike.›
definition G ("𝒢") where "𝒢 x ≡ ❙∀Y.((𝒫 Y) ❙→ (Y x))"

text‹Definitions of Essence and Necessary Existence.›
definition E ("ℰ") where "ℰ Y x ≡ (Y x) ❙∧ (❙∀Z.((Z x) ❙→ (Y⇛Z)))"
definition NE ("𝒩ℰ") where "𝒩ℰ x ≡ ❙∀Y.((ℰ Y x) ❙→ ❙□(❙∃⇧E Y))"
end



# Theory ScottVariant

subsection‹Ultrafilter Analysis of Scott's Variant (Fig.~3 in \cite{C85}))›

theory ScottVariant imports
HOML
MFilter
BaseDefs
begin
text‹Axioms of Scott's variant.›
axiomatization where
A1: "⌊❙∀X.((❙¬(𝒫 X)) ❙↔ (𝒫(❙⇁X)))⌋" and
A2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X⇛Y)) ❙→ (𝒫 Y))⌋" and
A3: "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋" and
A4: "⌊❙∀X.((𝒫 X) ❙→ ❙□(𝒫 X))⌋" and
A5: "⌊𝒫 𝒩ℰ⌋" and
B:  "⌊❙∀φ.(φ ❙→ ❙□❙◇φ)⌋" ―‹Logic KB›

lemma B': "∀x y. ¬(x❙ry) ∨ (y❙rx)" using B by fastforce

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋"
proof -
have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" using A1 A2 by blast
have T2: "⌊𝒫 𝒢⌋" by (metis A3 G_def)
have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
have T4: "⌊❙∀⇧Ex.((𝒢 x)❙→(ℰ 𝒢 x))⌋" unfolding G_def E_def using A1 A4 by metis
have T5: "⌊(❙◇(❙∃⇧E𝒢))❙→ ❙□(❙∃⇧E𝒢)⌋" by (smt A5 G_def B' NE_def T4)
thus ?thesis using T3 by blast qed

text‹Existence of a Godlike entity.›
lemma "⌊❙∃⇧E 𝒢⌋" using A1 A2 B' T6 by blast

text‹Consistency›
lemma True nitpick[satisfy] oops ―‹Model found.›

text‹Modal collapse: holds.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋"
proof - {
fix w fix Q
have 1: "∀x.((𝒢 x w) ⟶ (❙∀Z.((Z x) ❙→ ❙□(❙∀⇧Ez.((𝒢 z) ❙→ (Z z))))) w)"
by (metis A1 A4 G_def)
have 2: "(∃x. 𝒢 x w)⟶((Q ❙→ ❙□(❙∀⇧Ez.((𝒢 z) ❙→ Q))) w)"
using 1 by force
have 3: "(Q ❙→ ❙□Q) w" using B' T6 2 by blast}
thus ?thesis by auto qed

text‹Analysis of positive properties using ultrafilters.›
theorem U1: "⌊UFilter 𝒫⌋"  ―‹Proof found by sledgehammer›
proof -
have 1: "⌊(❙U❙∈𝒫) ❙∧ ❙¬(❙∅❙∈𝒫)⌋"  using A1 A2 by blast
have 2: "⌊❙∀φ ψ.(((φ❙∈𝒫)❙∧(φ❙⊆ψ))❙→(ψ❙∈𝒫))⌋"  by (smt A2 B' MC)
have 3: "⌊❙∀φ ψ.(((φ❙∈𝒫)❙∧(ψ❙∈𝒫))❙→((φ❙⊓ψ)❙∈𝒫))⌋" by (metis A1 A2 G_def B' T6)
have 4: "⌊❙∀φ.((φ❙∈𝒫) ❙∨ ((¯φ)❙∈𝒫))⌋"  using A1 by blast
thus ?thesis using 1 2 3 4 by simp qed

lemma L1: "⌊❙∀X Y.((X⇛Y) ❙→ (X❙⊑Y))⌋" by (metis A1 A2 MC)
lemma L2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑Y)) ❙→ (𝒫 Y))⌋" by (smt A2 B' MC)

text‹Set of supersets of X, we call this HF X.›
abbreviation HF where "HF X ≡ λY.(X❙⊑Y)"

text‹‹HF 𝒢› is a filter; hence, ‹HF 𝒢› is Hauptfilter of ‹𝒢›.›
lemma F1: "⌊Filter (HF 𝒢)⌋" by (metis A2 B' T6 U1)
lemma F2: "⌊UFilter (HF 𝒢)⌋" by (smt A1 F1 G_def)

text‹T6 follows directly from F1.›
theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋" using F1 by simp
end

# Theory UFilterVariant

subsection‹Ultrafilter Variant (Fig.~5 in \cite{C85})›

theory UFilterVariant imports
HOML
MFilter
BaseDefs
DisableKodkodScala
begin
text‹Axiom's of ultrafilter variant.›
axiomatization where
U1: "⌊UFilter 𝒫⌋" and
A2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X⇛Y)) ❙→ (𝒫 Y))⌋" and
A3: "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋"

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" ―‹Proof also found by sledgehammer›
proof -
have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" by (metis A2 U1)
have T2: "⌊𝒫 𝒢⌋" by (metis A3 G_def)
have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A2 G_def T2 U1)
thus ?thesis using T3 by blast qed

text‹Checking for consistency.›
lemma True nitpick[satisfy] oops  ―‹Model found›

text‹Checking for modal collapse.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops ―‹Countermodel›
end

(*
definition ess ("ℰ") where "ℰ Y x ≡ Y x ❙∧ (❙∀Z.(Z x ❙→ (Y⇛Z)))"
definition NE ("NE") where "NE x ≡ λw.((❙∀Y.(ℰ Y x ❙→ ❙□❙∃⇧E Y)) w)"
consts Godlike::γ UltraFilter::"(γ⇒σ)⇒σ" NeEx::γ
axiomatization where
1: "Godlike = G" and
2: "UltraFilter = Ultrafilter" and
3: "NeEx = NE"
lemma True nitpick[satisfy] oops
lemma MC: "⌊❙∀Φ. Φ ❙→ ❙□Φ⌋" nitpick[format=8] oops (*Countermodel*)
lemma A1: "⌊❙∀X. ❙¬(𝒫 X) ❙↔ 𝒫(❙⇁X)⌋" using U1 by fastforce
lemma A4: "⌊(𝒫 X ❙→ ❙□(𝒫 X))⌋" nitpick [format=4] oops (*Countermodel*)
lemma A5: "⌊𝒫 NE⌋" nitpick oops (*Countermodel*)
*)

# Theory SimpleVariant

subsection‹Simplified Variant (Fig.~6 in \cite{C85})›

theory SimpleVariant imports
HOML
MFilter
BaseDefs
DisableKodkodScala
begin
text‹Axiom's of new, simplified variant.›
axiomatization where
A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
A2': "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑Y) ❙∨ (X⇛Y))) ❙→ (𝒫 Y))⌋" and
A3:  "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋"

lemma T2: "⌊𝒫 𝒢⌋" by (metis A3 G_def) ―‹From A3›
lemma L1: "⌊𝒫(λx.(x❙=x))⌋" by (metis A2' A3)

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋"  ―‹Proof found by sledgehammer›
proof -
have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" by (metis A1' A2')
have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A1' A2' T2)
thus ?thesis using T3 by blast qed

lemma True nitpick[satisfy] oops ―‹Consistency: model found›

text‹Modal collapse and monotheism: not implied.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops ―‹Countermodel›
lemma MT: "⌊❙∀x y.(((𝒢 x) ❙∧ (𝒢 y)) ❙→ (x❙=y))⌋"
nitpick oops ―‹Countermodel.›

text‹Gödel's A1, A4, A5: not implied anymore.›
lemma A1: "⌊❙∀X.((❙¬(𝒫 X))❙↔(𝒫(❙⇁X)))⌋" nitpick oops ―‹Countermodel›
lemma A4: "⌊❙∀X.((𝒫 X) ❙→ ❙□(𝒫 X))⌋" nitpick oops ―‹Countermodel›
lemma A5: "⌊𝒫 𝒩ℰ⌋" nitpick oops ―‹Countermodel›

text‹Checking filter and ultrafilter properties.›
theorem F1: "⌊Filter 𝒫⌋" oops ―‹Proof found by sledgehammer, but reconstruction timeout›
theorem U1: "⌊UFilter 𝒫⌋" nitpick oops  ―‹Countermodel›
end



# Theory SimpleVariantPG

subsection‹Simplified Variant with Axiom T2 (Fig.~7 in \cite{C85})›

theory SimpleVariantPG imports
HOML
MFilter
BaseDefs
DisableKodkodScala
begin
text‹Axiom's of simplified variant with A3 replaced.›
axiomatization where
A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
A2': "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑Y)❙∨(X⇛Y))) ❙→ (𝒫 Y))⌋" and
T2:  "⌊𝒫 𝒢⌋"

text‹Necessary existence of a Godlike entity.›
theorem T6:  "⌊❙□(❙∃⇧E 𝒢)⌋"  ―‹Proof found by sledgehammer›
proof -
have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" by (metis A1' A2')
have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A1' A2' T2)
thus ?thesis using T3 by blast qed

lemma True nitpick[satisfy] oops  ―‹Consistency: model found›

text‹Modal collapse and Monotheism: not implied.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops  ―‹Countermodel›
lemma MT: "⌊❙∀x y.(((𝒢 x)❙∧(𝒢 y))❙→(x❙=y))⌋" nitpick oops  ―‹Countermodel›
end


# Theory SimpleVariantSE

subsection‹Simplified Variant with Simple Entailment in Logic K (Fig.~8 in \cite{C85})›

theory SimpleVariantSE imports
HOML
MFilter
BaseDefs
begin
text‹Axiom's of new variant based on ultrafilters.›
axiomatization where
A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
A2'': "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑Y)) ❙→ (𝒫 Y))⌋" and
T2:  "⌊𝒫 𝒢⌋"

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" using A1' A2'' T2 by blast
theorem T7: "⌊❙∃⇧E 𝒢⌋" using A1' A2'' T2 by blast

text‹Possible existence of a Godlike: has counterodel.›
lemma T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" nitpick oops ―‹Countermodel›

lemma T3': assumes T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋"
shows "⌊❙◇(❙∃⇧E 𝒢)⌋"
using A1' A2'' T2 T by metis
end


# Theory SimpleVariantSEinT

subsection‹Simplified Variant with Simple Entailment in Logic T (Fig.~9 in \cite{C85})›

theory SimpleVariantSEinT imports
HOML
MFilter
BaseDefs
begin
text‹Axiom's of new variant based on ultrafilters.›
axiomatization where
A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
A2'': "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑Y)) ❙→ (𝒫 Y))⌋" and
T2:   "⌊𝒫 𝒢⌋"

text‹Modal Logic T.›
axiomatization where T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋"
lemma T': "⌊❙∀φ.(φ ❙→ (❙◇φ))⌋" by (metis T)

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋"  ―‹Proof found by sledgehammer›
proof -
have T1: "⌊❙∀X.((𝒫 X)❙→(❙◇(❙∃⇧E X)))⌋" by (metis A1' A2'' T')
have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" by (metis T1 T2)
have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A1' A2'' T2)
thus ?thesis using T3 by simp qed

text‹T6 again, with an alternative, simpler proof.›
theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋"
proof -
have L1: "⌊(❙∃X.((𝒫 X)❙∧❙¬(❙∃⇧EX)))❙→(𝒫(λx.(x❙≠x)))⌋"
by (smt A2'')
have L2: "⌊❙¬(❙∃X.((𝒫 X) ❙∧ ❙¬(❙∃⇧E X)))⌋" by (metis L1 A1')
have T1': "⌊❙∀X.((𝒫 X) ❙→ (❙∃⇧E X))⌋" by (metis L2)
have T3': "⌊❙∃⇧E 𝒢⌋" by (metis T1' T2)
have L3: "⌊❙◇(❙∃⇧E 𝒢)⌋" by (metis T3' T') ―‹not needed›
thus ?thesis using T3' by simp qed
end



# Theory SimpleVariantHF

subsection‹Hauptfiltervariant (Fig.~10 in \cite{C85})›

theory SimpleVariantHF imports
HOML
MFilter
BaseDefs
DisableKodkodScala
begin
text‹Definition: Set of supersets of ‹X›, we call this ‹ℋℱ X›.›
abbreviation HF::"γ⇒(γ⇒σ)"  where "HF X ≡ λY.(X❙⊑Y)"

text‹Postulate: ‹ℋℱ 𝒢› is a filter; i.e., Hauptfilter of ‹𝒢›.›
axiomatization where F1: "⌊Filter (HF 𝒢)⌋"

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" using F1 by auto ―‹Proof found›

theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋"
proof -
have T3': "⌊❙∃⇧E 𝒢⌋" using F1 by auto
have T6:  "⌊❙□(❙∃⇧E 𝒢)⌋" using T3' by blast
thus ?thesis by simp qed

text‹Possible existence of Godlike entity not implied.›
lemma T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" nitpick oops  ―‹Countermodel›

text‹Axiom T enforces possible existence of Godlike entity.›
axiomatization
lemma T3: assumes T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋"
shows "⌊❙◇(❙∃⇧E 𝒢)⌋" using F1 T by auto

lemma True nitpick[satisfy] oops ―‹Consistency: model found›

text‹Modal collapse: not implied anymore.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops  ―‹Countermodel›
lemma MT: "⌊❙∀x y.(((𝒢 x) ❙∧ (𝒢 y)) ❙→ (x❙=y))⌋"
nitpick oops ―‹Countermodel›
end



# 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