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
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
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
B_axiom: "symmetric R" and
IV_axiom: "transitive R"
theorem C10: "⌊❙∃x. Godlike x⌋" using Contingent_expl Explanation_expl
Necessary_expl P2 P3 P4 P5 T_axiom by metis
lemma True nitpick[satisfy, user_axioms] oops
lemma "⌊Necessary x⌋" nitpick[user_axioms] oops
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops
end