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