Theory LoweOntologicalArgument_2

(*<*) 
theory LoweOntologicalArgument_2
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)⌋" and
  P6: "⌊❙∀x. Dependent x ❙→ Explained x⌋" and
  P7: "⌊❙∀x. Dependent x ❙→ ❙¬(x explains x)⌋" and
  P8:  "⌊❙∀x y. y explains x ❙→ x dependsOn y⌋"
  
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 P3 P6 by blast
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋" nitpick[user_axioms]  oops
(*>*) 
    
subsection ‹Validating the Argument I›
text‹\noindent{By examining the countermodel found by Nitpick for C10 we can see that some necessary beings that
are abstract in the actual world may indeed be concrete in other accessible worlds. Lowe had previously
presented numbers as an example of such necessary abstract beings. It can be argued that numbers, while
existing necessarily, can never be concrete in any possible world, so we add the restriction
of abstractness being an essential property, i.e. a locally rigid predicate.
}›
axiomatization where
  abstractness_essential: "⌊❙∀x. Abstract x ❙→ ❙□Abstract x⌋"

theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
  nitpick[user_axioms] oops ― ‹Countermodel found›
    
text‹\noindent{As Nitpick shows us, the former restriction is not enough to prove C10.
We try postulating further restrictions on the accessibility relation \emph{R} which, taken together,
would amount to it being an equivalence relation. Following the \emph{Sahlqvist correspondence}, this
would make for a modal logic \emph{S5}, and our abstractness property would consequently
become a (globally) rigid predicate.}›
    
axiomatization where 
 T_axiom: "reflexive R" and ― ‹@{text "□φ → φ"}›
 B_axiom: "symmetric R" and ― ‹@{text "φ →  □◇φ"}›
 IV_axiom: "transitive R"   ― ‹@{text "□φ → □□φ"}›
 
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋"
  nitpick[user_axioms] oops ― ‹Countermodel found›

text‹\noindent{By examining the new countermodel found by Nitpick we notice that at some worlds there are  
non-existent concrete beings. We want to disallow this possibility, so we make concreteness
an existence-entailing property.}›    
    
axiomatization where concrete_exist: "⌊❙∀x. Concrete x ❙→ E! x⌋"

text‹\noindent{We carry out the usual `sanity checks' to make sure the argument has not become trivialized.\footnote{
These checks are being carried out after postulating axioms for every iteration,
so we won't mention them anymore.}}›  
lemma True
  nitpick[satisfy, user_axioms] oops ― ‹Model found: axioms are consistent›
lemma "⌊❙∀x. E! x⌋"
  nitpick[user_axioms] oops ― ‹Countermodel found: necessitism is not valid›
lemma "⌊φ ❙→ ❙□φ⌋"
  nitpick[user_axioms] oops ― ‹Countermodel found: modal collapse is not valid›

text‹\noindent{Since this time Nitpick was not able to find a countermodel for C10, we have enough confidence in
the validity of the formula to ask Sledgehammer to search for a proof.}›
theorem C10:  "⌊❙∃⇧Ax. Godlike x⌋" using Existence_def Necessary_def
    abstractness_essential concrete_exist P2 C1 B_axiom by meson
    
text‹\noindent{Sledgehammer is able to find a proof relying on all premises
but the two modal axioms \emph{T} and \emph{IV}. By the end of this iteration we see
that Lowe's modal ontological argument depends for its validity on three non-stated (i.e. implicit) premises:
the essentiality of abstractness, the existence-entailing nature of concreteness and the modal
axiom \emph{B} (‹φ →  □◇φ›). Moreover, we have also shed some light on the meaning of the concepts
of abstractness and concreteness.}›

(*<*)
end
(*>*)