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
(*>*)