Theory SimplifiedOntologicalArgument
section ‹Selected Simplified Ontological Argument \label{sec:selected}›
theory SimplifiedOntologicalArgument imports
HOML
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" and "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
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
end