# Theory Relations

theory Relations
imports Main
begin

type_synonym 'a Rel = "'a ⇒ 'a ⇒ bool"

abbreviation symmetric :: "'a Rel ⇒ bool" where
"symmetric  A ≡ ∀ x.  ∀ y. (A x y) ⟶ (A y x)"

abbreviation asymmetric :: "'a Rel ⇒ bool" where
" asymmetric A ≡ ∀ x. ∀ y. (A x y) ⟶ ¬(A y x)"

abbreviation antisymmetric :: "'a Rel ⇒ bool" where
" antisymmetric A ≡ ∀ x. ∀ y. (A x y ∧ A y x) ⟶ x = y"

abbreviation reflexive :: "'a Rel ⇒ bool" where
"reflexive  A ≡ ∀ x. A x x"

abbreviation irreflexive :: "'a Rel ⇒ bool" where
"irreflexive  A ≡ ∀ x. ¬(A x x)"

abbreviation transitive :: "'a Rel ⇒ bool" where
"transitive  A ≡ ∀ x. ∀ y. ∀ z. (A x y) ∧ (A y z) ⟶ (A x z)"

abbreviation total :: "'a Rel ⇒ bool" where
"total  A ≡ ∀ x. ∀ y. A x y ∨ A y x"

abbreviation universal :: "'a Rel ⇒ bool" where
"universal  A ≡ ∀ x. ∀ y. A x y"

abbreviation serial :: "'a Rel ⇒ bool" where
"serial  A ≡ ∀ x. ∃ y. A x y"

abbreviation euclidean :: "'a Rel ⇒ bool" where
"euclidean  A ≡ ∀x y z. (A x y ∧ A x z) ⟶ A y z"

abbreviation preorder :: "'a Rel ⇒ bool" where
"preorder A ≡ reflexive A ∧ transitive A"

abbreviation equivalence :: "'a Rel ⇒ bool" where
"equivalence A ≡ preorder A ∧ symmetric A"

abbreviation partial_order :: "'a Rel ⇒ bool" where
"partial_order A ≡  preorder A ∧ antisymmetric A"

abbreviation strict_partial_order :: "'a Rel ⇒ bool" where
"strict_partial_order A ≡  irreflexive A ∧ asymmetric A ∧ transitive A" (* asymmetry is redundant *)

end


# Theory QML

(*<*)
theory QML
imports Relations
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d]
(*>*)

section ‹Embedding of Quantified Modal Logic›
text‹\noindent{As is well known, the Isabelle proof assistant @{cite "Isabelle"} does not natively support modal logics, so
we have used a technique known as \emph{shallow semantic embedding}, which allows us
to take advantage of the expressive power of higher-order logic in order to embed the semantics
of an object language. We draw on previous work on the embedding of multimodal logics in HOL @{cite "J23"},
which has successfully been applied to the analysis and verification of ontological arguments
(e.g. @{cite C55 and J32 and J35}).}›

subsection ‹Type Declarations›

typedecl e                        ― ‹Type for entities›
typedecl w                        ― ‹Type for worlds›
type_synonym wo = "w⇒bool" ― ‹Type for world-dependent formulas›

subsection ‹Logical Constants as Truth-Sets›
text‹\noindent{Using the technique of \emph{shallow semantic embedding} each operator gets defined as a function
on world-dependent formulas or \emph{truth sets}.}›

abbreviation mand::"wo⇒wo⇒wo" (infixr "❙∧"(*<*)51(*>*))
where "φ❙∧ψ ≡ λw. (φ w)∧(ψ w)"
abbreviation mor::"wo⇒wo⇒wo" (infixr "❙∨"(*<*)50(*>*))
where "φ❙∨ψ ≡ λw. (φ w)∨(ψ w)"
abbreviation mimp::"wo⇒wo⇒wo" (infixr "❙→"(*<*)49(*>*))
where "φ❙→ψ ≡ λw. (φ w)⟶(ψ w)"
abbreviation mequ::"wo⇒wo⇒wo" (infix "❙↔"(*<*)48(*>*))
where "φ❙↔ψ ≡ λw. (φ w)⟷(ψ w)"
abbreviation mnot::"wo⇒wo" ("❙¬_"(*<*)[52]53(*>*))
where "❙¬φ ≡ λw. ¬(φ w)"
(*<*)
abbreviation xor:: "bool⇒bool⇒bool" (infix"⊕"50) where "φ⊕ψ ≡  (φ∨ψ) ∧ ¬(φ∧ψ)"
abbreviation mxor::"wo⇒wo⇒wo" (infix"❙⊕"50) where "φ❙⊕ψ ≡ λw. (φ w)⊕(ψ w)"
(*>*)

text‹\noindent{We embed a modal logic \emph{K} by defining the box and diamond operators using restricted quantification
over the set of accessible' worlds (using an \emph{accessibility} relation \emph{R} as a guard).}›

consts R::"w⇒w⇒bool" (infix "r"(*<*)70(*>*)) ― ‹Accessibility relation›
abbreviation mbox :: "wo⇒wo" ("❙□_"(*<*)[52]53(*>*))
where "❙□φ ≡ λw.∀v. (w r v)⟶(φ v)"
abbreviation mdia :: "wo⇒wo" ("❙◇_"(*<*)[52]53(*>*))
where "❙◇φ ≡ λw.∃v. (w r v)∧(φ v)"

subsection ‹Quantification›
text‹\noindent{Quantifiers are defined analogously.}›

abbreviation mforall::"('t⇒wo)⇒wo" ("❙∀")
where "❙∀Φ ≡ λw.∀x. (Φ x w)"
abbreviation mexists::"('t⇒wo)⇒wo" ("❙∃")
where "❙∃Φ ≡ λw.∃x. (Φ x w)"
abbreviation mforallB  :: "('t⇒wo)⇒wo" (binder "❙∀"(*<*)[8]9(*>*))
where "❙∀x. (φ x) ≡ ❙∀φ"
abbreviation mexistsB  :: "('t⇒wo)⇒wo" (binder "❙∃"(*<*)[8]9(*>*))
where "❙∃x. (φ x) ≡ ❙∃φ"

subsection ‹Equality›
text‹\noindent{Two different definitions of equality are given. The first one is an extension of standard
equality for use in world-dependent formulas. The second is the well-known Leibniz equality.}›
abbreviation meq:: "'t⇒'t⇒wo" (infix "❙≈"(*<*)60(*>*))
where "x ❙≈ y ≡ λw. x = y"
abbreviation meqL:: "e⇒e⇒wo" (infix "❙≈⇧L"(*<*)52(*>*))
where "x ❙≈⇧L y ≡ λw. ∀φ. (φ x w)⟶(φ y w)"

subsection ‹Validity›
text‹\noindent{Validity is defined as truth in \emph{all} worlds and represented by wrapping the formula
in special brackets (‹⌊-⌋›).}›
abbreviation valid::"wo⇒bool" ("⌊_⌋") where "⌊ψ⌋ ≡  ∀w.(ψ w)"

subsection ‹Verifying the Embedding›
text‹\noindent{The above definitions introduce modal logic \emph{K} with quantification,
as evidenced by the following tests.}›

lemma K: "⌊(❙□(φ ❙→ ψ)) ❙→ (❙□φ ❙→ ❙□ψ)⌋" by simp ― ‹Verifying \emph{K} principle›
lemma NEC: "⌊φ⌋ ⟹ ⌊❙□φ⌋" by simp        ― ‹Verifying \emph{necessitation} rule›

text‹\noindent{Local consequence implies global consequence (not the other way round).}›
lemma localImpGlobalCons: "⌊φ ❙→ ξ⌋ ⟹ ⌊φ⌋ ⟶ ⌊ξ⌋" by simp
lemma "⌊φ⌋ ⟶ ⌊ξ⌋ ⟹ ⌊φ ❙→ ξ⌋" nitpick oops ― ‹Countersatisfiable›

text‹\noindent{(Converse-)Barcan formulas are validated in this embedding.}›
lemma "⌊(❙∀x.❙□(φ x)) ❙→ ❙□(❙∀x.(φ x))⌋" by simp
lemma "⌊❙□(❙∀x.(φ x)) ❙→ (❙∀x.❙□(φ x))⌋" by simp

text‹\noindent{‹β›-redex is valid.}›
lemma "⌊(λα. φ α) (τ::w⇒e) ❙↔ (φ  τ)⌋" by simp
lemma "⌊(λα. φ α) (τ::e) ❙↔ (φ  τ)⌋" by simp
lemma "⌊(λα. ❙□φ α) (τ::w⇒e) ❙↔ (❙□φ τ)⌋" by simp
lemma "⌊(λα. ❙□φ α) (τ::e) ❙↔ (❙□φ τ)⌋" by simp

text‹\noindent{Modal collapse is countersatisfiable, as shown by Nitpick @{cite "Nitpick"}.}›
lemma "⌊φ ❙→ ❙□φ⌋" nitpick oops

subsection ‹Axiomatization of Further Logics›

text‹\noindent{The best-known normal logics (\emph{K4, K5, KB, K45, KB5, D, D4, D5, ...}) can be obtained by
combinations of the following axioms.}›
abbreviation T  where "T ≡ ❙∀φ. ❙□φ ❙→ φ"
abbreviation B  where "B ≡ ❙∀φ. φ ❙→  ❙□❙◇φ"
abbreviation D  where "D ≡ ❙∀φ. ❙□φ ❙→ ❙◇φ"
abbreviation IV where "IV ≡ ❙∀φ. ❙□φ ❙→  ❙□❙□φ"
abbreviation V  where "V ≡ ❙∀φ. ❙◇φ ❙→ ❙□❙◇φ"

text‹\noindent{Instead of postulating combinations of the above  axioms we make use of
the well-known \emph{Sahlqvist correspondence}, which links axioms to constraints on a model's accessibility
relation (cf. @{cite "J23"} for further details).
We show  that  reflexivity, symmetry, seriality, transitivity and euclideanness imply
axioms \emph{T, B, D, IV, V} respectively.\footnote{Implication can also be proven in the reverse direction
(which is not needed for our purposes).
Using these definitions, we can derive axioms for the most common modal logics (see also @{cite "C47"}).
Thereby we are free to use either the semantic constraints or the related \emph{Sahlqvist} axioms. Here we provide
both versions. In what follows we use the semantic constraints for improved performance.}}›
lemma "reflexive R  ⟹  ⌊T⌋" by blast
lemma "symmetric R ⟹ ⌊B⌋" by blast
lemma "serial R  ⟹ ⌊D⌋" by blast
lemma "transitive R  ⟹ ⌊IV⌋" by blast
lemma "euclidean R ⟹ ⌊V⌋" by blast
lemma "preorder R ⟹ ⌊T⌋ ∧ ⌊IV⌋" by blast ― ‹S4: reflexive + transitive›
lemma "equivalence R ⟹ ⌊T⌋ ∧ ⌊V⌋" by blast ― ‹S5: preorder + symmetric›
(*<*)
end
(*>*)


# Theory LoweOntologicalArgument_1

(*<*)
theory LoweOntologicalArgument_1

imports QML
begin
nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]
(*>*)

section ‹E. J. Lowe's Modal Ontological Argument›

subsection ‹Introduction›
text‹\noindent{E. J. Lowe presented his argument in an article named "A Modal Version of the Ontological Argument",
which has been published as a chapter in \cite{moreland2013}.
The structure of this argument is very representative of philosophical arguments.
It features eight premises from which new inferences are drawn until arriving at a final conclusion:
the necessary existence of God
(which in this case amounts to the existence of some "necessary concrete being").}›

text‹\noindent{(P1) God is, by definition, a necessary concrete being.}›
text‹\noindent{(P2) Some necessary abstract beings exist.}›
text‹\noindent{(P3) All abstract beings are dependent beings.}›
text‹\noindent{(P4) All dependent beings depend for their existence on independent beings.}›
text‹\noindent{(P5) No contingent being can explain the existence of a necessary being.}›
text‹\noindent{(P6) The existence of any dependent being needs to be explained.}›
text‹\noindent{(P7) Dependent beings of any kind cannot explain their own existence.}›
text‹\noindent{(P8) The existence of dependent beings can only be explained by beings on which they depend
for their existence.}›

text‹\noindent{We will consider in our treatment only a representative subset of the conclusions,
as presented in Lowe's article.}›

text‹\noindent{(C1) All abstract beings depend for their existence on concrete beings.
(Follows from P3 and P4 together with D3 and D4.)}›
text‹\noindent{(C5) In every possible world there exist concrete beings. (Follows from C1 and P2.)}›
text‹\noindent{(C7) The existence of necessary abstract beings needs to be explained. (Follows from P2, P3 and P6.)}›
text‹\noindent{(C8) The existence of necessary abstract beings can only be explained by concrete beings.
(Follows from C1, P3, P7 and P8.)}›
text‹\noindent{(C9) The existence of necessary abstract beings is explained by one or more necessary concrete beings.
(Follows from C7, C8 and P5.)}›
text‹\noindent{(C10) A necessary concrete being exists. (Follows from C9.)}›

text‹\noindent{Lowe also introduces some informal definitions which should help the reader understand
the meaning of the concepts involved in his argument
(necessity, concreteness, ontological dependence, metaphysical explanation, etc.).
In the following discussion, we will see that most of these definitions do not bear the significance
Lowe claims.}›

text‹\noindent{(D1) x is a necessary being := x exists in every possible world.}›
text‹\noindent{(D2) x is a contingent being := x exists in some but not every possible world.}›
text‹\noindent{(D3) x is a concrete being := x exists in space and time, or at least in time.}›
text‹\noindent{(D4) x is an abstract being := x does not exist in space or time.}›
text‹\noindent{(D5) x depends for its existence on y := necessarily, x exists only if y exists.}›
text‹\noindent{(D6) (For any predicates F and G) F depend for their existence on G := necessarily, Fs exist only if Gs exist.}›

text‹\noindent{We will work \emph{iteratively} on Lowe's argument by temporarily fixing truth-values
and inferential relationships among its sentences, and then, after choosing a logic for formalization,
working back and forth on the formalization of its axioms and theorems
by making gradual adjustments while getting automatic real-time feedback about the suitability of our changes,
vis-a-vis the argument's validity.
In this fashion, by engaging in an \emph{iterative} process of trial and error, we work our way
towards a proper understanding
of the concepts involved in the argument, far beyond of what a mere natural-language based discussion would allow.}›

subsection ‹Initial Formalization›

text‹\noindent{We start our first iterations with a formalized version of Lowe's argument in modal logic using the
semantic embedding presented in the previous section.
We first turn to the formalization of premise P1: "God is, by definition, a necessary concrete being".
In order to understand the concept of \emph{necessariness} (i.e. being a "necessary being")
employed in this argument,
we have a look at the definitions D1 and D2 provided by Lowe.
They relate the concepts of necessariness and contingency (i.e. being a "contingent being") with existence:\footnote{
Here, the concepts of necessariness and contingency are meant as properties of beings, in contrast to the
concepts of necessity and possibility which are modals. We will see later how both pairs of
concepts can be related in order to validate this argument.}}›

text‹\noindent{(D1) \emph{x is a necessary being := x exists in every possible world.}}›
text‹\noindent{(D2) \emph{x is a contingent being := x exists in some but not every possible world.}}›

text‹\noindent{The two definitions above, aimed at explicating the concepts of necessariness and contingency
by reducing them to existence and quantification over possible worlds,
have a direct impact on the choice of a logic for formalization.
They not only call for some kind of modal logic with possible-world semantics but also lead us to consider
the complex issue of existence, since we need to restrict the domain of quantification at every world.}›
text‹\noindent{For this argument not to become trivialized, we guarded our quantifiers so they range only over
those entities existing (i.e. being actualized) at a given world.
This approach is known as \emph{actualist quantification}
and is implemented in our semantic embedding by defining a world-dependent meta-logical existence' predicate
(called "actualizedAt" below), which is the one used as a guard in the definition of the quantifiers.
Note that the type \emph{e} characterizes the domain of all beings (existing and non-existing), and
the type \emph{wo} (which is an abbreviation for ‹w⇒bool›) characterizes sets of worlds.
The term "isActualized" thus relates beings to worlds.}›

consts isActualized::"e⇒wo" (infix "actualizedAt"(*<*)70(*>*))

abbreviation forallAct::"(e⇒wo)⇒wo" ("❙∀⇧A")
where "❙∀⇧AΦ ≡ λw.∀x. (x actualizedAt w)⟶(Φ x w)"
abbreviation existsAct::"(e⇒wo)⇒wo" ("❙∃⇧A")
where "❙∃⇧AΦ ≡ λw.∃x. (x actualizedAt w) ∧ (Φ x w)"

text‹\noindent{We also define the corresponding binder syntax below.}›
abbreviation mforallActB::"(e⇒wo)⇒wo" (binder"❙∀⇧A"[8]9)
where "❙∀⇧Ax. (φ x) ≡ ❙∀⇧Aφ"
abbreviation mexistsActB::"(e⇒wo)⇒wo" (binder"❙∃⇧A"[8]9)
where "❙∃⇧Ax. (φ x) ≡ ❙∃⇧Aφ"

text‹\noindent{We use Isabelle's Nitpick tool @{cite "Nitpick"} to verify that actualist quantification validates
neither the Barcan formula nor its converse.}›

lemma "⌊(❙∀⇧Ax. ❙□(φ x)) ❙→ ❙□(❙∀⇧Ax. φ x)⌋"
nitpick oops ― ‹Countermodel found: formula not valid›
lemma "⌊❙□(❙∀⇧Ax. φ x) ❙→ (❙∀⇧Ax. ❙□(φ x))⌋"
nitpick oops ― ‹Countermodel found: formula not valid›

text‹\noindent{With actualist quantification in place we can:
(i) formalize the concept of existence in the usual form (by using a restricted particular quantifier),
(ii) formalize necessariness as existing necessarily, and
(iii) formalize contingency as existing possibly but not necessarily.
}›

definition Existence::"e⇒wo" ("E!") where "E! x  ≡ ❙∃⇧Ay. y ❙≈ x"

definition Necessary::"e⇒wo" where "Necessary x ≡  ❙□E! x"
definition Contingent::"e⇒wo" where "Contingent x≡ ❙◇E! x ❙∧ ❙¬Necessary x"

text‹\noindent{Note that we have just chosen our logic for formalization: a free quantified modal logic \emph{K}
with positive semantics.
The logic is \emph{free} because the domain of quantification (for actualist quantifiers) is a proper subset of
our universe of discourse, so we can refer to non-actual objects. The semantics is \emph{positive} because
we have placed no restriction regarding predication on non-actual objects, so they are also allowed
to exemplify properties and relations.
We are also in a position to embed stronger normal modal logics (\emph{KB, KB5, S4, S5, ...})
by restricting the accessibility relation \emph{R} with additional axioms.}›

text‹\noindent{Having chosen our logic, we can now turn to the formalization of the concepts of abstractness and concreteness.
As seen previously, Lowe has already provided us with an explication of these concepts:}›

text‹\noindent{(D3) \emph{x is a concrete being := x exists in space and time, or at least in time.}}›
text‹\noindent{(D4) \emph{x is an abstract being := x does not exist in space or time.}}›

text‹\noindent{Lowe himself acknowledges that the explication of these concepts in terms of existence
"in space and time" is superfluous, since we are only interested in them being complementary.\footnote{
We quote from Lowe's original article:
"Observe that, according to these definitions, a being cannot be both concrete and abstract:
being concrete and being abstract are mutually exclusive properties of beings.
Also, all beings are either concrete or abstract ... the abstract/concrete distinction is exhaustive.
Consequently, a being is concrete if and only if it is not abstract."}
Thus we start by formalizing concreteness as a \emph{primitive} world-dependent predicate and then derive
abstractness from it, namely as its negation.
}›
consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"

text‹\noindent{We can now formalize the definition of Godlikeness (P1) as follows: }›
abbreviation Godlike::"e⇒wo" where "Godlike x ≡ Necessary x ❙∧ Concrete x"

text‹\noindent{We also formalize premise P2 ("Some necessary abstract beings exist") as shown below:}›
axiomatization where
P2: "⌊❙∃⇧Ax. Necessary x ❙∧ Abstract x⌋" (* Some necessary abstract beings exist.*)

text‹\noindent{Let's now turn to premises P3 ("All abstract beings are dependent beings") and P4
("All dependent beings depend for their existence on independent beings").
We have here three new concepts to be explicated: two predicates "dependent" and "independent"
and a relation "depends (for its existence) on", which has been called
\emph{ontological dependence} by Lowe.
Following our linguistic intuitions concerning their interrelation, we start by proposing
the following formalization:}›

consts dependence::"e⇒e⇒wo" (infix "dependsOn"(*<*)100(*>*))
definition Dependent::"e⇒wo" where "Dependent x ≡ ❙∃⇧Ay. x dependsOn y"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

text‹\noindent{We have formalized ontological dependence as a \emph{primitive} world-dependent relation
and refrained from any explication (as suggested by Lowe).\footnote{
An explication of this concept has been suggested by Lowe in definition D5
("x depends for its existence on y := necessarily, x exists only if y exists").
Concerning this alleged definition, he has written in a footnote to the same article:
"Note, however, that the two definitions (D5) and (D6) presented below are not in fact formally called upon in the
version of the ontological argument that I am now developing, so that in the remainder of
this chapter the notion of existential dependence may, for all intents and purposes, be taken
as primitive. There is an advantage in this, inasmuch as finding a perfectly apt definition of
existential dependence is no easy task, as I explain in Ontological Dependence.'"
Lowe refers hereby to his article on ontological dependence in the Stanford Encyclopedia of Philosophy
@{cite "sep-dependence-ontological"} for further discussion.}

We have called an entity \emph{dependent} if and only if there \emph{actually exists} an object y such that
x \emph{depends for its existence} on it;
accordingly, we have called an entity \emph{independent} if and only if it is not dependent.}›

text‹\noindent{As a consequence, premises P3 ("All abstract beings are dependent beings") and P4
("All dependent beings depend for their existence on independent beings") become formalized as follows.}›

axiomatization where
P3: "⌊❙∀⇧Ax. Abstract x ❙→ Dependent x⌋" and (* All abstract beings are dependent beings.*)
P4: "⌊❙∀⇧Ax. Dependent x ❙→ (❙∃⇧Ay. Independent y ❙∧ x dependsOn y)⌋" (* All dependent beings depend for their existence on independent beings.*)

text‹\noindent{Concerning premises P5 ("No contingent being can explain the existence of a necessary being") and
P6 ("The existence of any dependent being needs to be explained"), a suitable formalization
for expressions of the form: "the entity X explains the existence of Y" and
"the existence of X is explained" needs to be found.
These expressions rely on a single binary relation, which will initially be taken as \emph{primitive}.
This relation has been called \emph{metaphysical explanation} by Lowe.}›

consts explanation::"e⇒e⇒wo" (infix "explains"(*<*)100(*>*))
definition Explained::"e⇒wo" where "Explained x ≡ ❙∃⇧Ay. y explains x"

axiomatization where
P5: "⌊❙¬(❙∃⇧Ax. ❙∃⇧Ay. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋" (* No contingent being can explain the existence of a necessary being. *)

text‹\noindent{Premise P6, together with the last two premises: P7
("Dependent beings of any kind cannot explain their own existence") and
P8 ("The existence of dependent beings can only be explained by beings on which they depend for their existence"),
were introduced by Lowe in order to relate the concept of \emph{metaphysical explanation}
to \emph{ontological dependence}.\footnote{Note that we use non-guarded quantifiers for the formalization of
the last three premises in order to test argument's validity under the strongest assumptions.
As before, we turn a blind eye to modal expressions like "can", "needs to", etc.}}›

axiomatization where
P6: "⌊❙∀x. Dependent x ❙→ Explained x⌋" and (* The existence of any dependent being needs to be explained. *)
P7: "⌊❙∀x. Dependent x ❙→ ❙¬(x explains x)⌋" and (* Dependent beings of any kind cannot explain their own existence. *)
P8: "⌊❙∀x y. y explains x ❙→ x dependsOn y⌋" (* The existence of dependent beings can only be explained by beings on which they depend for their existence. *)

text‹\noindent{Although the last three premises seem to couple very tightly the concepts of (metaphysical) explanation
and (ontological) dependence, both concepts are not meant by Lowe to be equivalent.\footnote{
Lowe says: "Existence-explanation is not simply the inverse of existential dependence.
If x depends for its existence on y, this only means that x cannot exist without y
existing. This is not at all the same as saying that x exists because y exists, or that
x exists in virtue of the fact that y exists."}
We have used Nitpick in order to test this claim. Since a countermodel has been found, we have proven
that the (inverse) equivalence of metaphysical explanation and ontological dependence
is not implied by the axioms.}›
lemma "⌊❙∀x y. x explains y ❙↔ y dependsOn x⌋" nitpick[user_axioms] oops

text‹\noindent{For any being, however, having its existence "explained"
is equivalent to its existence being "dependent" (on some other being).
This follows already from premises P6 and P8, as shown above by Isabelle's prover.}›
lemma "⌊❙∀x. Explained x ❙↔ Dependent x⌋"
using P6 P8 Dependent_def Explained_def by auto

text‹\noindent{The Nitpick model finder is also useful to check axioms' consistency at any stage during the
formalization of an argument.
We instruct Nitpick to generate a model satisfying some tautological sentence
(here we use a trivial True' proposition) while taking into account all previously defined axioms.}›
lemma True nitpick[satisfy, user_axioms] oops

text‹\noindent{In this case, Nitpick was able to find a model satisfying the given tautology; this means that
all axioms defined so far are consistent. The model found has a cardinality of two for the set of
individual objects and a single world.}›

text‹\noindent{We can also use model finders to perform sanity checks'. We can instruct Nitpick
to find a countermodel for some specifically tailored formula which we want to make sure is not valid.
We check below, for instance, that our axioms are not too strong as to imply \emph{metaphysical necessitism}
(i.e. all beings necessarily exist)
or \emph{modal collapse}. Since both would trivially validate the argument.}›

lemma "⌊❙∀x. E! x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found: necessitism is not valid›

lemma "⌊φ ❙→ ❙□φ⌋"
nitpick[user_axioms] oops ― ‹Countermodel found: modal collapse is not valid›

text‹\noindent{By using Isabelle's \emph{Sledgehammer} tool @{cite "Sledgehammer"}, we can verify the validity
of the selected conclusions C1, C5 and C7, and even find the premises they rely upon.}›

text‹\noindent{(C1) \emph{All abstract beings depend for their existence on concrete beings.}}›
theorem C1:  "⌊❙∀⇧Ax. Abstract x ❙→ (❙∃y. Concrete y ❙∧ x dependsOn y)⌋"
using P3 P4 by blast
text‹\noindent{(C5) \emph{In every possible world there exist concrete beings.} }›
theorem C5: "⌊❙∃⇧Ax. Concrete x⌋"
using P2 P3 P4 by blast
text‹\noindent{(C7) \emph{The existence of necessary abstract beings needs to be explained.}}›
theorem C7: "⌊❙∀⇧Ax. (Necessary x ❙∧ Abstract x) ❙→ Explained x⌋"
using P3 P6 by simp

text‹\noindent{The last three conclusions are shown by Nitpick to be non-valid even in an \emph{S5} logic.
\emph{S5} can be easily introduced by postulating that the accessibility relation \emph{R} is an equivalence relation.
This exploits the well-known \emph{Sahlqvist correspondence} which links modal axioms to constraints
on a model's accessibility relation.}›

axiomatization where
S5: "equivalence R" ― ‹@{text "□φ→φ, φ→□◇φ and □φ→□□φ"}›

text‹\noindent{(C8) \emph{The existence  of  necessary  abstract  beings  can  only  be  explained  by  concrete  beings.} }›
lemma C8: "⌊❙∀⇧Ax.(Necessary x ❙∧ Abstract x)❙→(❙∀⇧Ay. y explains x❙→Concrete y)⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›
text‹\noindent{(C9) \emph{The existence of necessary abstract beings is explained by one or more necessary concrete (Godlike) beings.} }›
lemma C9: "⌊❙∀⇧Ax.(Necessary x ❙∧ Abstract x)❙→(❙∃⇧Ay. y explains x ❙∧ Godlike y)⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›
text‹\noindent{(C10) \emph{A necessary concrete (Godlike) being exists.} }›
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›

text‹\noindent{By employing the Isabelle proof assistant we prove non-valid a first formalization attempt of
Lowe's modal ontological argument. This is, however, just the first of many iterations in our
interpretive endeavor. Based on the information recollected so far, we can proceed to make the adjustments
necessary to validate the argument. We will see how these changes have an impact on our understanding of
all concepts (necessariness, concreteness, dependence, explanation, etc.).
}›

(*<*)
end
(*>*)


# Theory LoweOntologicalArgument_2

(*<*)
theory LoweOntologicalArgument_2
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]

consts isActualized::"e⇒wo" (infix "actualizedAt" 70)

abbreviation forallAct::"(e⇒wo)⇒wo" ("❙∀⇧A")
where "❙∀⇧AΦ ≡ λw.∀x. (x actualizedAt w)⟶(Φ x w)"
abbreviation existsAct::"(e⇒wo)⇒wo" ("❙∃⇧A")
where "❙∃⇧AΦ ≡ λw.∃x. (x actualizedAt w) ∧ (Φ x w)"
abbreviation mforallActB::"(e⇒wo)⇒wo" (binder"❙∀⇧A"[8]9)
where "❙∀⇧Ax. (φ x) ≡ ❙∀⇧Aφ"
abbreviation mexistsActB::"(e⇒wo)⇒wo" (binder"❙∃⇧A"[8]9)
where "❙∃⇧Ax. (φ x) ≡ ❙∃⇧Aφ"

definition Existence::"e⇒wo" ("E!") where "E! x  ≡ ❙∃⇧Ay. y❙≈x"
definition Necessary::"e⇒wo" where "Necessary x ≡  ❙□E! x"
definition Contingent::"e⇒wo" where "Contingent x ≡  ❙◇E! x ❙∧ ❙¬(Necessary x)"

consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"

abbreviation Godlike::"e⇒wo"  where "Godlike x ≡ Necessary x ❙∧ Concrete x"

consts dependence::"e⇒e⇒wo" (infix "dependsOn" 100)
definition Dependent::"e⇒wo" where "Dependent x ≡ ❙∃⇧Ay. x dependsOn y"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

consts explanation::"e⇒e⇒wo" (infix "explains" 100)
definition Explained::"e⇒wo" where "Explained x ≡ ❙∃⇧Ay. y explains x"

axiomatization where
P2: "⌊❙∃⇧Ax. Necessary x ❙∧ Abstract x⌋" and
P3: "⌊❙∀⇧Ax. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀⇧Ax. Dependent x ❙→ (❙∃⇧Ay. Independent y ❙∧ x dependsOn y)⌋" and
P5: "⌊❙¬(❙∃⇧Ax. ❙∃⇧Ay. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋" and
P6: "⌊❙∀x. Dependent x ❙→ Explained x⌋" and
P7: "⌊❙∀x. Dependent x ❙→ ❙¬(x explains x)⌋" and
P8:  "⌊❙∀x y. y explains x ❙→ x dependsOn y⌋"

theorem C1:  "⌊❙∀⇧Ax. Abstract x ❙→ (❙∃y. Concrete y ❙∧ x dependsOn y)⌋"  using P3 P4 by blast
theorem C5: "⌊❙∃⇧Ax. Concrete x⌋" using P2 P3 P4 by blast
theorem C7: "⌊❙∀⇧Ax. (Necessary x ❙∧ Abstract x) ❙→ Explained x⌋"  using P3 P6 by blast
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋" nitpick[user_axioms]  oops
(*>*)

subsection ‹Validating the Argument I›
text‹\noindent{By examining the countermodel found by Nitpick for C10 we can see that some necessary beings that
are abstract in the actual world may indeed be concrete in other accessible worlds. Lowe had previously
presented numbers as an example of such necessary abstract beings. It can be argued that numbers, while
existing necessarily, can never be concrete in any possible world, so we add the restriction
of abstractness being an essential property, i.e. a locally rigid predicate.
}›
axiomatization where
abstractness_essential: "⌊❙∀x. Abstract x ❙→ ❙□Abstract x⌋"

theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›

text‹\noindent{As Nitpick shows us, the former restriction is not enough to prove C10.
We try postulating further restrictions on the accessibility relation \emph{R} which, taken together,
would amount to it being an equivalence relation. Following the \emph{Sahlqvist correspondence}, this
would make for a modal logic \emph{S5}, and our abstractness property would consequently
become a (globally) rigid predicate.}›

axiomatization where
T_axiom: "reflexive R" and ― ‹@{text "□φ → φ"}›
B_axiom: "symmetric R" and ― ‹@{text "φ →  □◇φ"}›
IV_axiom: "transitive R"   ― ‹@{text "□φ → □□φ"}›

theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›

text‹\noindent{By examining the new countermodel found by Nitpick we notice that at some worlds there are
non-existent concrete beings. We want to disallow this possibility, so we make concreteness
an existence-entailing property.}›

axiomatization where concrete_exist: "⌊❙∀x. Concrete x ❙→ E! x⌋"

text‹\noindent{We carry out the usual sanity checks' to make sure the argument has not become trivialized.\footnote{
These checks are being carried out after postulating axioms for every iteration,
so we won't mention them anymore.}}›
lemma True
nitpick[satisfy, user_axioms] oops ― ‹Model found: axioms are consistent›
lemma "⌊❙∀x. E! x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found: necessitism is not valid›
lemma "⌊φ ❙→ ❙□φ⌋"
nitpick[user_axioms] oops ― ‹Countermodel found: modal collapse is not valid›

text‹\noindent{Since this time Nitpick was not able to find a countermodel for C10, we have enough confidence in
the validity of the formula to ask Sledgehammer to search for a proof.}›
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋" using Existence_def Necessary_def
abstractness_essential concrete_exist P2 C1 B_axiom by meson

text‹\noindent{Sledgehammer is able to find a proof relying on all premises
but the two modal axioms \emph{T} and \emph{IV}. By the end of this iteration we see
that Lowe's modal ontological argument depends for its validity on three non-stated (i.e. implicit) premises:
the essentiality of abstractness, the existence-entailing nature of concreteness and the modal
axiom \emph{B} (‹φ →  □◇φ›). Moreover, we have also shed some light on the meaning of the concepts
of abstractness and concreteness.}›

(*<*)
end
(*>*)


# Theory LoweOntologicalArgument_3

(*<*)
theory LoweOntologicalArgument_3
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]

consts isActualized::"e⇒wo" (infix "actualizedAt" 70)

abbreviation forallAct::"(e⇒wo)⇒wo" ("❙∀⇧A")
where "❙∀⇧AΦ ≡ λw.∀x. (x actualizedAt w)⟶(Φ x w)"
abbreviation existsAct::"(e⇒wo)⇒wo" ("❙∃⇧A")
where "❙∃⇧AΦ ≡ λw.∃x. (x actualizedAt w) ∧ (Φ x w)"
abbreviation mforallActB::"(e⇒wo)⇒wo" (binder"❙∀⇧A"[8]9)
where "❙∀⇧Ax. (φ x) ≡ ❙∀⇧Aφ"
abbreviation mexistsActB::"(e⇒wo)⇒wo" (binder"❙∃⇧A"[8]9)
where "❙∃⇧Ax. (φ x) ≡ ❙∃⇧Aφ"

definition Existence::"e⇒wo" ("E!") where "E! x  ≡ ❙∃⇧Ay. y❙≈x"
definition Necessary::"e⇒wo" where "Necessary x ≡  ❙□E! x"
definition Contingent::"e⇒wo" where "Contingent x ≡  ❙◇E! x ❙∧ ❙¬(Necessary x)"

consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"

abbreviation Godlike::"e⇒wo"  where "Godlike x ≡ Necessary x ❙∧ Concrete x"

consts dependence::"e⇒e⇒wo" (infix "dependsOn" 100)
definition Dependent::"e⇒wo" where "Dependent x ≡ ❙∃⇧Ay. x dependsOn y"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

consts explanation::"e⇒e⇒wo" (infix "explains" 100)
definition Explained::"e⇒wo" where "Explained x ≡ ❙∃⇧Ay. y explains x"

axiomatization where
P2: "⌊❙∃⇧Ax. Necessary x ❙∧ Abstract x⌋" and
P3: "⌊❙∀⇧Ax. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀⇧Ax. Dependent x ❙→ (❙∃⇧Ay. Independent y ❙∧ x dependsOn y)⌋" and
P5: "⌊❙¬(❙∃⇧Ax. ❙∃⇧Ay. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋"
(*>*)

subsection ‹Validating the Argument II›

text‹\noindent{We present a slightly simplified version of the original argument (without the implicit premises stated in
the previous version). In this variant premises P1 to P5 remain unchanged
and none of the last three premises proposed by Lowe (P6 to P8) show up anymore.
Those last premises have been introduced in order to interrelate the concepts of explanation and dependence
in such a way that they play somewhat opposite roles.
Now we want to go all the way and simply assume that they are inverse relations,
for we want to understand how the interrelation of these two concepts affects the validity of the argument.}›

axiomatization where
dep_expl_inverse: "⌊❙∀x y. y explains x ❙↔ x dependsOn y⌋"

text‹\noindent{We proceed to prove the relevant partial conclusions.}›
theorem C1:  "⌊❙∀⇧Ax. Abstract x ❙→ (❙∃y. Concrete y ❙∧ x dependsOn y)⌋"
using P3 P4 by blast

theorem C5: "⌊❙∃⇧Ax. Concrete x⌋"
using P2 P3 P4 by blast

theorem C7: "⌊❙∀⇧Ax. (Necessary x ❙∧ Abstract x) ❙→ Explained x⌋"
using Explained_def P3 P4 dep_expl_inverse by meson

text‹\noindent{But the final conclusion C10 is still countersatisfiable, as shown by Nitpick:}›
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
nitpick[user_axioms] oops ― ‹Countermodel found›

text‹\noindent{Next, we try assuming a stronger modal logic. We do this by postulating further axioms
using the \emph{Sahlqvist correspondence} and asking Sledgehammer to find a proof.
Sledgehammer is in fact able to find a proof for C10 which only relies on the modal axiom \emph{T}
(‹□φ ❙→ φ›).}›
axiomatization where
T_axiom: "reflexive R" and ― ‹@{text "□φ → φ"}›
B_axiom: "symmetric R" and ― ‹@{text "φ →  □◇φ"}›
IV_axiom: "transitive R"   ― ‹@{text "□φ → □□φ"}›

theorem C10: "⌊❙∃⇧Ax. Godlike x⌋" using Contingent_def Existence_def
P2 P3 P4 P5 dep_expl_inverse T_axiom by meson

text‹\noindent{In this series of iterations we have verified a modified version of the original argument by Lowe.
Our understanding of the concepts of \emph{ontological dependence} and \emph{metaphysical explanation}
have changed after the introduction of an additional axiom constraining both:
they are now inverse relations.
Still, we want to carry on with our iterative process in order to further illuminate the meaning
of the concepts involved in this argument.}›

(*<*)
(* We carry out our sanity checks' as usual.*)
lemma True nitpick[satisfy, user_axioms] oops (* model found: axioms are consistent *)
lemma "⌊Necessary x⌋" nitpick[user_axioms] oops (* counter-model found: axioms do not trivialize argument *)
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops (* counter-model found: modal collapse is not valid *)

end
(*>*)


# Theory LoweOntologicalArgument_4

(*<*)
theory LoweOntologicalArgument_4
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]

consts isActualized::"e⇒wo" (infix "actualizedAt" 70)

abbreviation forallAct::"(e⇒wo)⇒wo" ("❙∀⇧A")
where "❙∀⇧AΦ ≡ λw.∀x. (x actualizedAt w)⟶(Φ x w)"
abbreviation existsAct::"(e⇒wo)⇒wo" ("❙∃⇧A")
where "❙∃⇧AΦ ≡ λw.∃x. (x actualizedAt w) ∧ (Φ x w)"
abbreviation mforallActB::"(e⇒wo)⇒wo" (binder"❙∀⇧A"[8]9)
where "❙∀⇧Ax. (φ x) ≡ ❙∀⇧Aφ"
abbreviation mexistsActB::"(e⇒wo)⇒wo" (binder"❙∃⇧A"[8]9)
where "❙∃⇧Ax. (φ x) ≡ ❙∃⇧Aφ"

definition Existence::"e⇒wo" ("E!") where "E! x  ≡ ❙∃⇧Ay. y❙≈x"
definition Necessary::"e⇒wo" where "Necessary x ≡  ❙□E! x"
definition Contingent::"e⇒wo" where "Contingent x ≡  ❙◇E! x ❙∧ ❙¬(Necessary x)"

consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"

abbreviation Godlike::"e⇒wo"  where "Godlike x ≡ Necessary x ❙∧ Concrete x"

consts dependence::"e⇒e⇒wo" (infix "dependsOn" 100)
definition Dependent::"e⇒wo" where "Dependent x ≡ ❙∃⇧Ay. x dependsOn y"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

axiomatization where
P2: "⌊❙∃⇧Ax. Necessary x ❙∧ Abstract x⌋" and
P3: "⌊❙∀⇧Ax. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀⇧Ax. Dependent x ❙→ (❙∃⇧Ay. Independent y ❙∧ x dependsOn y)⌋"
(*>*)

subsection ‹Simplifying the Argument›

text‹\noindent{After some further iterations we arrive at a new variant of the original argument:
Premises P1 to P4 remain unchanged and a new premise D5
("x depends for its existence on y := necessarily, x exists only if y exists") is added.
D5 corresponds to the definition' of ontological dependence as put forth by
Lowe in his article (though just for illustrative purposes). As mentioned before, this purported definition was never meant by him to become part
of the argument. Nevertheless, we show here how, by assuming the left-to-right direction of this definition,
we get in a position to prove the main conclusions without any further assumptions.
}›
axiomatization where
D5: "⌊❙∀⇧Ax y. x dependsOn y ❙→ ❙□(E! x ❙→ E! y)⌋"

theorem C1:  "⌊❙∀⇧Ax. Abstract x ❙→ (❙∃y. Concrete y ❙∧ x dependsOn y)⌋"
using P3 P4 by meson

theorem C5: "⌊❙∃⇧Ax. Concrete x⌋"
using P2 P3 P4 by meson

theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
using Necessary_def P2 P3 P4 D5 by meson

text‹\noindent{In this variant we have been able to verify the conclusion of the argument without appealing
to the concept of metaphysical explanation. We were able to get by with just the concept of
ontological dependence by explicating it in terms of existence and necessity (as suggested by Lowe).}›

text‹\noindent{As a side note, we can also prove that the original premise P5
("No contingent being can explain the existence of a necessary being")
directly follows from D5 by redefining metaphysical explanation
as the inverse relation of ontological dependence.}›

abbreviation explanation::"(e⇒e⇒wo)" (infix "explains"(*<*)100(*>*))
where "y explains x ≡ x dependsOn y"

lemma P5: "⌊❙¬(❙∃⇧Ax. ❙∃⇧Ay. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋"
using Necessary_def Contingent_def D5 by meson

text‹\noindent{In this series of iterations we have reworked the argument so as to get rid of the somewhat obscure
concept of metaphysical explanation;
we also got some insight into Lowe's concept of ontological dependence vis-a-vis its
inferential role in this argument.}›
text‹\noindent{There are still some interesting issues to consider.
Note that the definitions of existence (‹Existence_def›) and being "dependent" (‹Dependent_def›)
are not needed in any of the highly optimized proofs found by our automated tools.
This raises some suspicions concerning the role played by the existence predicate in the
definitions of necessariness and contingency, as well as putting into question the need for
a definition of being "dependent" linked to the ontological dependence relation.
We will see in the following section that our suspicions are justified and that
this argument can be dramatically simplified.}›

(*<*)
(* We carry out our sanity checks' as usual.*)
lemma True nitpick[satisfy, user_axioms] oops (* model found: axioms are consistent *)
lemma "⌊Necessary x⌋" nitpick[user_axioms] oops (* counter-model found: axioms do not trivialize argument *)
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops (* counter-model found: modal collapse is not valid *)

end
(*>*)


# Theory LoweOntologicalArgument_5

(*<*)
theory LoweOntologicalArgument_5
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]
(*>*)

subsection ‹Arriving at a Non-Modal Argument›

text‹\noindent{A new simplified emendation of Lowe's argument is obtained after abandoning the concept of existence
and redefining necessariness and contingency accordingly. As we will see, this variant
is actually non-modal and can be easily formalized in first-order predicate logic.}›

text‹\noindent{A more literal reading of Lowe's article has suggested a simplified formalization, in which necessariness
and contingency are taken as complementary predicates. According to this, our domain of discourse becomes
divided in four main categories, as exemplified in the table below:\footnote{
As Lowe explains in the article, "there is no logical restriction on combinations of the properties
involved in the concrete/abstract and the necessary/contingent distinctions.
In principle, then, we can have contingent concrete beings, contingent abstract beings,
necessary concrete beings, and necessary abstract beings."}
}›
text‹\noindent{
\begin{center}
\begin{tabular}{ l | c | r | }
& Abstract & Concrete \\ \hline
Necessary & Numbers & God \\ \hline
Contingent & Fiction & Stuff \\
\hline
\end{tabular}
\end{center}
}›
consts Necessary::"e⇒wo"
abbreviation Contingent::"e⇒wo" where "Contingent x ≡ ❙¬(Necessary x)"

consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"

abbreviation Godlike::"e⇒w⇒bool" where "Godlike x≡ Necessary x ❙∧ Concrete x"

consts dependence::"e⇒e⇒wo" (infix "dependsOn"(*<*)100(*>*))
abbreviation explanation::"(e⇒e⇒wo)" (infix "explains"(*<*)100(*>*))
where "y explains x ≡ x dependsOn y"

text‹\noindent{As shown below, we can even define the "dependent" predicate as \emph{primitive},
i.e. bearing no relation to ontological dependence, and still be able to validate the argument.
Being "independent" is defined as the negation of being "dependent", as before.}›
consts Dependent::"e⇒wo"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

text‹\noindent{By taking, once again, metaphysical explanation as the inverse relation of ontological dependence
and by assuming premises P2 to P5 we can prove conclusion C10.}›

axiomatization where
P2: "⌊❙∃x. Necessary x ❙∧ Abstract x⌋" and
P3: "⌊❙∀x. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀x. Dependent x ❙→ (❙∃y. Independent y ❙∧ x dependsOn y)⌋" and
P5: "⌊❙¬(❙∃x. ❙∃y. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋"

theorem C10: "⌊❙∃x. Godlike x⌋" using  P2 P3 P4 P5 by blast

text‹\noindent{Note that, in the axioms above, all actualist quantifiers have been changed into non-guarded quantifiers,
following the elimination of the concept of existence from our argument: Our quantifiers range over \emph{all}
beings, because all beings exist. Also note that all modal operators have disappeared;
thus, this new variant is directly formalizable in classical first-order logic.}›

(*<*)
(* We carry out our sanity checks' as usual.*)
lemma True nitpick[satisfy, user_axioms] oops (* model found: axioms are consistent *)
lemma "⌊Necessary x⌋" nitpick[user_axioms] oops (* counter-model found: axioms do not trivialize argument *)
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops (* counter-model found: modal collapse is not valid *)

end
(*>*)


# Theory LoweOntologicalArgument_6

(*<*)
theory LoweOntologicalArgument_6
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]
(*>*)

subsection ‹Modified Modal Argument I›
text‹\noindent{In the following iterations we want to illustrate an approach in which we start our interpretive endeavor
with no pre-understanding of the concepts involved.
We start by taking all concepts as primitive without providing any definition
or presupposing any interrelation between them. We see how we gradually improve our understanding of these
concepts in the iterative process of adding and removing axioms and, therefore,
by framing their inferential role in the argument.}›

consts Concrete::"e⇒wo"
consts Abstract::"e⇒wo"
consts Necessary::"e⇒wo"
consts Contingent::"e⇒wo"
consts dependence::"e⇒e⇒wo" (infix "dependsOn"(*<*)100(*>*))
consts explanation::"e⇒e⇒wo" (infix "explains"(*<*)100(*>*))
consts Dependent::"e⇒wo"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

text‹\noindent{In order to honor the original intention of the author, i.e.  providing a \emph{modal} variant
of St. Anselm's ontological argument, we are required to make a change in Lowe's original formulation.
In this variant we have restated the expressions "necessary abstract" and "necessary concrete"
as "necessarily abstract" and "necessarily concrete" correspondingly.
With this new adverbial reading of the former "necessary" predicate we are no longer talking
about the concept of \emph{necessariness}, but of \emph{necessity} instead,
so we use the modal box operator (‹□›) for its formalization.
Note that in this variant we are not concerned with the interpretation of the original ontological argument anymore.
We are interested, instead, in showing how our method can go beyond simple interpretation
and foster a creative approach to assessing and improving philosophical arguments.}›

text‹\noindent{Premise P1 now reads: "God is, by definition, a necessari\emph{ly} concrete being."}›
abbreviation Godlike::"e⇒wo" where "Godlike x ≡ ❙□Concrete x"

text‹\noindent{Premise P2 reads: "Some necessari\emph{ly} abstract beings exist".
The rest of the premises remains unchanged.}›
axiomatization where
P2: "⌊❙∃x. ❙□Abstract x⌋" and
P3: "⌊❙∀x. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀x. Dependent x ❙→ (❙∃y. Independent y ❙∧ x dependsOn y)⌋" and
P5: "⌊❙¬(❙∃x. ❙∃y. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋"

text‹\noindent{Without postulating any additional axioms, C10 ("A \emph{necessarily} concrete being exists")
can be falsified by Nitpick.}›
theorem C10: "⌊❙∃x. Godlike x⌋"
nitpick oops ― ‹Countermodel found›

text‹\noindent{An explication of the concepts of necessariness, contingency and explanation is provided below
by axiomatizing their interrelation to other concepts.
We regard necessariness as being \emph{necessarily abstract} or \emph{necessarily concrete}.
We regard explanation as the inverse relation of dependence, as before.}›
axiomatization where
Necessary_expl: "⌊❙∀x. Necessary x ❙↔ (❙□Abstract x ❙∨ ❙□Concrete x)⌋" and
Contingent_expl: "⌊❙∀x. Contingent x ❙↔ ❙¬Necessary x⌋" and
Explanation_expl: "⌊❙∀x y. y explains x ❙↔ x dependsOn y⌋"

text‹\noindent{Without any further constraints, C10 becomes falsified by Nitpick.}›
theorem C10: "⌊❙∃x. Godlike x⌋"
nitpick oops ― ‹Countermodel found›

text‹\noindent{We postulate further modal axioms (using the \emph{Sahlqvist correspondence})
and ask Isabelle's \emph{Sledgehammer} for a proof. Sledgehammer is able to
find a proof for C10 which only relies on the modal axiom T (‹□φ ❙→ φ›).}›

axiomatization where
T_axiom: "reflexive R" and ― ‹@{text "□φ → φ"}›
B_axiom: "symmetric R" and ― ‹@{text "φ →  □◇φ"}›
IV_axiom: "transitive R"   ― ‹@{text "□φ → □□φ"}›

theorem C10: "⌊❙∃x. Godlike x⌋" using Contingent_expl Explanation_expl
Necessary_expl P2 P3 P4 P5 T_axiom by metis

(*<*)
(* We carry out our sanity checks' as usual.*)
lemma True nitpick[satisfy, user_axioms] oops (* model found: axioms are consistent *)
lemma "⌊Necessary x⌋" nitpick[user_axioms] oops (* axioms do not trivialize argument *)
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops (* counter-model found: modal collapse is not valid *)

end
(*>*)


# Theory LoweOntologicalArgument_7

(*<*)
theory LoweOntologicalArgument_7
imports QML
begin

nitpick_params[box=false, user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]

consts Concrete::"e⇒wo"
consts Abstract::"e⇒wo"
consts Necessary::"e⇒wo"
consts Contingent::"e⇒wo"
consts dependence::"e⇒e⇒wo" (infix "dependsOn"(*<*)100(*>*))
consts explanation::"e⇒e⇒wo" (infix "explains"(*<*)100(*>*))
consts Dependent::"e⇒wo"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"

abbreviation Godlike::"e⇒wo" where "Godlike x ≡ ❙□Concrete x"

axiomatization where
P2: "⌊❙∃x. ❙□Abstract x⌋" and
P3: "⌊❙∀x. Abstract x ❙→ Dependent x⌋" and
P4: "⌊❙∀x. Dependent x ❙→ (❙∃y. Independent y ❙∧ x dependsOn y)⌋" and
P5: "⌊❙¬(❙∃x. ❙∃y. Contingent y ❙∧ Necessary x ❙∧ y explains x)⌋"
(*>*)

subsection ‹Modified Modal Argument II›

text‹\noindent{We start again our interpretive process with no pre-understanding of the
concepts involved (by taking them as primitive).
We then see how their inferential role gradually becomes apparent in the process
of axiomatizing further constraints. We follow on with the adverbial reading of the expression "necessary"
as in the previous version.}›

text‹\noindent{Another explication of the concepts of necessariness and contingency is provided below.
We think that this explication, in comparison to the previous one, better fits our intuitive
understanding of necessariness.
We now regard necessariness as being \emph{necessarily} abstract or concrete, and
explanation as the inverse relation of dependence, as before.}›
axiomatization where
Necessary_expl: "⌊❙∀x. Necessary x ❙↔ ❙□(Abstract x ❙∨ Concrete x)⌋" and
Contingent_expl: "⌊❙∀x. Contingent x ❙↔ ❙¬Necessary x⌋" and
Explanation_expl: "⌊❙∀x y. y explains x ❙↔ x dependsOn y⌋"

text‹\noindent{These constraints are, however, not enough to ensure the argument's validity as confirmed by Nitpick.}›
theorem C10: "⌊❙∃x. Godlike x⌋"
nitpick oops ― ‹Countermodel found›

text‹\noindent{After some iterations, we see that, by giving a more satisfactory explication of the concept
of necesariness, we are also required to assume the essentiality of abstractness
(as we did in a former iteration) and to restrict the accessibility relation by enforcing its symmetry
(i.e. assuming the modal axiom \emph{B}).}›
axiomatization where
abstractness_essential: "⌊❙∀x. Abstract x ❙→ ❙□Abstract x⌋" and
B_Axiom:  "symmetric R"

theorem C10: "⌊❙∃x. Godlike x⌋" using Contingent_expl Explanation_expl
Necessary_expl P2 P3 P4 P5 abstractness_essential B_Axiom by metis

text‹\noindent{We have chosen to terminate, after this series of iterations, our interpretive endeavor.
In each of the previous versions we have illustrated how our understanding of the concepts of
necessity/contingency, explanation/dependence and abstractness/concreteness has gradually evolved
thanks to the kind of iterative hypothetico-deductive method which has been made possible
by the real-time feedback provided by Isabelle's automated proving tools.}›

(*<*)
(* We carry out our sanity checks' as usual.*)
lemma True nitpick[satisfy, user_axioms] oops (* model found: axioms are consistent *)
lemma "⌊❙∀x. Necessary x⌋" nitpick[user_axioms] oops ― ‹counter-model found: argument is not trivial›
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops (* counter-model found: modal collapse is not valid *)

end
(*>*)