Theory LoweOntologicalArgument_5

(*<*) 
theory LoweOntologicalArgument_5
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 ‹Arriving at a Non-Modal Argument›
  
text‹\noindent{A new simplified emendation of Lowe's argument is obtained after abandoning the concept of existence
and redefining necessariness and contingency accordingly. As we will see, this variant
is actually non-modal and can be easily formalized in first-order predicate logic.}›
  
text‹\noindent{A more literal reading of Lowe's article has suggested a simplified formalization, in which necessariness
and contingency are taken as complementary predicates. According to this, our domain of discourse becomes
divided in four main categories, as exemplified in the table below:\footnote{
As Lowe explains in the article, "there is no logical restriction on combinations of the properties
involved in the concrete/abstract and the necessary/contingent distinctions.
In principle, then, we can have contingent concrete beings, contingent abstract beings,
necessary concrete beings, and necessary abstract beings."}
}›
text‹\noindent{
\begin{center}
  \begin{tabular}{ l | c | r | }   
     & Abstract & Concrete \\ \hline
    Necessary & Numbers & God \\ \hline
    Contingent & Fiction & Stuff \\
    \hline
  \end{tabular}
\end{center}
}›
consts Necessary::"e⇒wo"
abbreviation Contingent::"e⇒wo" where "Contingent x ≡ ❙¬(Necessary x)"
    
consts Concrete::"e⇒wo"
abbreviation Abstract::"e⇒wo" where "Abstract x ≡  ❙¬(Concrete x)"
  
abbreviation Godlike::"e⇒w⇒bool" where "Godlike x≡ Necessary x ❙∧ Concrete x" 
        
consts dependence::"e⇒e⇒wo" (infix ‹dependsOn›(*<*)100(*>*))
abbreviation explanation::"(e⇒e⇒wo)" (infix ‹explains›(*<*)100(*>*))
  where "y explains x ≡ x dependsOn y"

text‹\noindent{As shown below, we can even define the "dependent" predicate as \emph{primitive},
i.e. bearing no relation to ontological dependence, and still be able to validate the argument.
Being "independent" is defined as the negation of being "dependent", as before.}›
consts Dependent::"e⇒wo"
abbreviation Independent::"e⇒wo" where "Independent x  ≡ ❙¬(Dependent x)"
  
text‹\noindent{By taking, once again, metaphysical explanation as the inverse relation of ontological dependence
and by assuming premises P2 to P5 we can prove conclusion C10.}›
  
axiomatization where
P2: "⌊❙∃x. Necessary 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)⌋"

theorem C10: "⌊❙∃x. Godlike x⌋" using  P2 P3 P4 P5 by blast
    
text‹\noindent{Note that, in the axioms above, all actualist quantifiers have been changed into non-guarded quantifiers,
following the elimination of the concept of existence from our argument: Our quantifiers range over \emph{all}
beings, because all beings exist. Also note that all modal operators have disappeared;
thus, this new variant is directly formalizable in classical first-order logic.}›

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