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
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.}›
lemma True nitpick[satisfy, user_axioms] oops
lemma "⌊❙∀x. Necessary x⌋" nitpick[user_axioms] oops
lemma "⌊φ ❙→ ❙□φ⌋" nitpick[user_axioms] oops
end