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
lemma "⌊❙□(❙∀⇧Ax. φ x) ❙→ (❙∀⇧Ax. ❙□(φ x))⌋"
nitpick oops
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⌋"
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
P4: "⌊❙∀⇧Ax. Dependent x ❙→ (❙∃⇧Ay. Independent y ❙∧ x dependsOn y)⌋"
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)⌋"
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
P7: "⌊❙∀x. Dependent x ❙→ ❙¬(x explains x)⌋" and
P8: "⌊❙∀x y. y explains x ❙→ x dependsOn y⌋"
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
lemma "⌊φ ❙→ ❙□φ⌋"
nitpick[user_axioms] oops
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‹\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
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
text‹\noindent{(C10) \emph{A necessary concrete (Godlike) being exists.} }›
theorem C10: "⌊❙∃⇧Ax. Godlike x⌋"
nitpick[user_axioms] oops
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