(*<*) theory IHOML imports Relations begin nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d] (*>*) section ‹Introduction› text‹ We present a study on Computational Metaphysics: a computer-formalisation and verification of Fitting's variant of the ontological argument (for the existence of God) as presented in his textbook \emph{Types, Tableaus and G\"odel's God} \<^cite>‹"Fitting"›. Fitting's argument is an emendation of Kurt G\"odel's modern variant \<^cite>‹"GoedelNotes"› (resp. Dana Scott's variant \<^cite>‹"ScottNotes"›) of the ontological argument. › text‹ The motivation is to avoid the \emph{modal collapse} \<^cite>‹Sobel and sobel2004logic›, which has been criticised as an undesirable side-effect of the axioms of G\"odel resp. Scott. The modal collapse essentially states that there are no contingent truths and that everything is determined. Several authors (e.g. \<^cite>‹"anderson90:_some_emend_of_goedel_ontol_proof" and "AndersonGettings" and "Hajek2002" and "bjordal99"›) have proposed emendations of the argument with the aim of maintaining the essential result (the necessary existence of God) while at the same time avoiding the modal collapse. Related work has formalised several of these variants on the computer and verified or falsified them. For example, G\"odel's axioms \<^cite>‹"GoedelNotes"› have been shown inconsistent \<^cite>‹C55 and C60› while Scott's version has been verified \<^cite>‹"ECAI"›. Further experiments, contributing amongst others to the clarification of a related debate between H\'ajek and Anderson, are presented and discussed in \<^cite>‹"J23"›. The enabling technique in all of these experiments has been shallow semantical embeddings of (extensional) higher-order modal logics in classical higher-order logic (see \<^cite>‹J23 and R59› and the references therein). › text‹ Fitting's emendation also intends to avoid the modal collapse. However, in contrast to the above variants, Fitting's solution is based on the use of an intensional as opposed to an extensional higher-order modal logic. For our work this imposed the additional challenge to provide a shallow embedding of this more advanced logic. The experiments presented below confirm that Fitting's argument as presented in his textbook \<^cite>‹"Fitting"› is valid and that it avoids the modal collapse as intended. › text‹ The work presented here originates from the \emph{Computational Metaphysics} lecture course held at FU Berlin in Summer 2016 \<^cite>‹"C65"›. \pagebreak › section ‹Embedding of Intensional Higher-Order Modal Logic› text‹ The object logic being embedded, intensional higher-order modal logic (IHOML), is a modification of the intentional logic developed by Montague and Gallin \<^cite>‹"Gallin75"›. IHOML is introduced by Fitting in the second part of his textbook \<^cite>‹"Fitting"› in order to formalise his emendation of G\"odel's ontological argument. We offer here a shallow embedding of this logic in Isabelle/HOL, which has been inspired by previous work on the semantical embedding of multimodal logics with quantification \<^cite>‹"J23"›. We expand this approach to allow for actualist quantifiers, intensional types and their related operations. › subsection ‹Type Declarations› text‹ Since IHOML and Isabelle/HOL are both typed languages, we introduce a type-mapping between them. We follow as closely as possible the syntax given by Fitting (see p. 86). According to this syntax, if ‹τ› is an extensional type, ‹↑τ› is the corresponding intensional type. For instance, a set of (red) objects has the extensional type ‹⟨𝟬⟩›, whereas the concept `red' has intensional type ‹↑⟨𝟬⟩›. In what follows, terms having extensional (intensional) types will be called extensional (intensional) terms. › typedecl i ― ‹type for possible worlds› type_synonym io = "(i⇒bool)" ― ‹formulas with world-dependent truth-value› typedecl e ("𝟬") ― ‹individuals› text‹ Aliases for common unary predicate types: › type_synonym ie = "(i⇒𝟬)" ("↑𝟬") type_synonym se = "(𝟬⇒bool)" ("⟨𝟬⟩") type_synonym ise = "(𝟬⇒io)" ("↑⟨𝟬⟩") type_synonym sie = "(↑𝟬⇒bool)" ("⟨↑𝟬⟩") type_synonym isie = "(↑𝟬⇒io)" ("↑⟨↑𝟬⟩") type_synonym sise = "(↑⟨𝟬⟩⇒bool)" ("⟨↑⟨𝟬⟩⟩") type_synonym isise = "(↑⟨𝟬⟩⇒io)" ("↑⟨↑⟨𝟬⟩⟩") type_synonym sisise= "(↑⟨↑⟨𝟬⟩⟩⇒bool)" ("⟨↑⟨↑⟨𝟬⟩⟩⟩") type_synonym isisise= "(↑⟨↑⟨𝟬⟩⟩⇒io)" ("↑⟨↑⟨↑⟨𝟬⟩⟩⟩") type_synonym sse = "⟨𝟬⟩⇒bool" ("⟨⟨𝟬⟩⟩") type_synonym isse = "⟨𝟬⟩⇒io" ("↑⟨⟨𝟬⟩⟩") text‹ Aliases for common binary relation types: › type_synonym see = "(𝟬⇒𝟬⇒bool)" ("⟨𝟬,𝟬⟩") type_synonym isee = "(𝟬⇒𝟬⇒io)" ("↑⟨𝟬,𝟬⟩") type_synonym sieie = "(↑𝟬⇒↑𝟬⇒bool)" ("⟨↑𝟬,↑𝟬⟩") type_synonym isieie = "(↑𝟬⇒↑𝟬⇒io)" ("↑⟨↑𝟬,↑𝟬⟩") type_synonym ssese = "(⟨𝟬⟩⇒⟨𝟬⟩⇒bool)" ("⟨⟨𝟬⟩,⟨𝟬⟩⟩") type_synonym issese = "(⟨𝟬⟩⇒⟨𝟬⟩⇒io)" ("↑⟨⟨𝟬⟩,⟨𝟬⟩⟩") type_synonym ssee = "(⟨𝟬⟩⇒𝟬⇒bool)" ("⟨⟨𝟬⟩,𝟬⟩") type_synonym issee = "(⟨𝟬⟩⇒𝟬⇒io)" ("↑⟨⟨𝟬⟩,𝟬⟩") type_synonym isisee = "(↑⟨𝟬⟩⇒𝟬⇒io)" ("↑⟨↑⟨𝟬⟩,𝟬⟩") type_synonym isiseise = "(↑⟨𝟬⟩⇒↑⟨𝟬⟩⇒io)" ("↑⟨↑⟨𝟬⟩,↑⟨𝟬⟩⟩") type_synonym isiseisise= "(↑⟨𝟬⟩⇒↑⟨↑⟨𝟬⟩⟩⇒io)" ("↑⟨↑⟨𝟬⟩,↑⟨↑⟨𝟬⟩⟩⟩") subsection ‹Definitions› subsubsection ‹Logical Operators as Truth-Sets› abbreviation mnot :: "io⇒io" ("❙¬_"[52]53) where "❙¬φ ≡ λw. ¬(φ w)" abbreviation negpred :: "⟨𝟬⟩⇒⟨𝟬⟩" ("⇁_"[52]53) where "⇁Φ ≡ λx. ¬(Φ x)" abbreviation mnegpred :: "↑⟨𝟬⟩⇒↑⟨𝟬⟩" ("❙⇁_"[52]53) where "❙⇁Φ ≡ λx.λw. ¬(Φ x w)" abbreviation mand :: "io⇒io⇒io" (infixr"❙∧"51) where "φ❙∧ψ ≡ λw. (φ w)∧(ψ w)" abbreviation mor :: "io⇒io⇒io" (infixr"❙∨"50) where "φ❙∨ψ ≡ λw. (φ w)∨(ψ w)" abbreviation mimp :: "io⇒io⇒io" (infixr"❙→"49) where "φ❙→ψ ≡ λw. (φ w)⟶(ψ w)" abbreviation mequ :: "io⇒io⇒io" (infixr"❙↔"48) where "φ❙↔ψ ≡ λw. (φ w)⟷(ψ w)" abbreviation xor:: "bool⇒bool⇒bool" (infixr"⊕"50) where "φ⊕ψ ≡ (φ∨ψ) ∧ ¬(φ∧ψ)" abbreviation mxor :: "io⇒io⇒io" (infixr"❙⊕"50) where "φ❙⊕ψ ≡ λw. (φ w)⊕(ψ w)" subsubsection ‹Possibilist Quantification› abbreviation mforall :: "('t⇒io)⇒io" ("❙∀") where "❙∀Φ ≡ λw.∀x. (Φ x w)" abbreviation mexists :: "('t⇒io)⇒io" ("❙∃") where "❙∃Φ ≡ λw.∃x. (Φ x w)" abbreviation mforallB :: "('t⇒io)⇒io" (binder"❙∀"[8]9) ― ‹Binder notation› where "❙∀x. φ(x) ≡ ❙∀φ" abbreviation mexistsB :: "('t⇒io)⇒io" (binder"❙∃"[8]9) where "❙∃x. φ(x) ≡ ❙∃φ" subsubsection ‹Actualist Quantification› text‹ The following predicate is used to model actualist quantifiers by restricting the domain of quantification at every possible world. This standard technique has been referred to as \emph{existence relativization} (\<^cite>‹"fitting98"›, p. 106), highlighting the fact that this predicate can be seen as a kind of meta-logical `existence predicate' telling us which individuals \emph{actually} exist at a given world. This meta-logical concept does not appear in our object language. › consts Exists::"↑⟨𝟬⟩" ("existsAt") abbreviation mforallAct :: "↑⟨↑⟨𝟬⟩⟩" ("❙∀⇧^{E}") where "❙∀⇧^{E}Φ ≡ λw.∀x. (existsAt x w)⟶(Φ x w)" abbreviation mexistsAct :: "↑⟨↑⟨𝟬⟩⟩" ("❙∃⇧^{E}") where "❙∃⇧^{E}Φ ≡ λw.∃x. (existsAt x w) ∧ (Φ x w)" abbreviation mforallActB :: "↑⟨↑⟨𝟬⟩⟩" (binder"❙∀⇧^{E}"[8]9) ― ‹binder notation› where "❙∀⇧^{E}x. φ(x) ≡ ❙∀⇧^{E}φ" abbreviation mexistsActB :: "↑⟨↑⟨𝟬⟩⟩" (binder"❙∃⇧^{E}"[8]9) where "❙∃⇧^{E}x. φ(x) ≡ ❙∃⇧^{E}φ" subsubsection ‹Modal Operators› consts aRel::"i⇒i⇒bool" (infixr "r" 70) ― ‹accessibility relation \emph{r}› abbreviation mbox :: "io⇒io" ("❙□_"[52]53) where "❙□φ ≡ λw.∀v. (w r v)⟶(φ v)" abbreviation mdia :: "io⇒io" ("❙◇_"[52]53) where "❙◇φ ≡ λw.∃v. (w r v)∧(φ v)" subsubsection ‹\emph{Extension-of} Operator› text‹ According to Fitting's semantics (\<^cite>‹"Fitting"›, pp. 92-4) ‹↓› is an unary operator applying only to intensional terms. A term of the form ‹↓α› designates the extension of the intensional object designated by ‹α›, at some \emph{given} world. For instance, suppose we take possible worlds as persons, we can therefore think of the concept `red' as a function that maps each person to the set of objects that person classifies as red (its extension). We can further state, the intensional term \emph{r} of type ‹↑⟨𝟬⟩› designates the concept `red'. As can be seen, intensional terms in IHOML designate functions on possible worlds and they always do it \emph{rigidly}. We will sometimes refer to an intensional object explicitly as `rigid', implying that its (rigidly) designated function has the same extension in all possible worlds. › text‹ Terms of the form ‹↓α› are called \emph{relativized} (extensional) terms; they are always derived from intensional terms and their type is \emph{extensional} (in the color example ‹↓r› would be of type ‹⟨𝟬⟩›). Relativized terms may vary their denotation from world to world of a model, because the extension of an intensional term can change from world to world, i.e. they are non-rigid. › text‹ To recap: an intensional term denotes the same function in all worlds (i.e. it's rigid), whereas a relativized term denotes a (possibly) different extension (an object or a set) at every world (i.e. it's non-rigid). To find out the denotation of a relativized term, a world must be given. Relativized terms are the \emph{only} non-rigid terms. \bigbreak › text‹ For our Isabelle/HOL embedding, we had to follow a slightly different approach; we model ‹↓› as a predicate applying to formulas of the form ‹Φ(↓α⇩_{1},…α⇩_{n})› (for our treatment we only need to consider cases involving one or two arguments, the first one being a relativized term). For instance, the formula ‹Q(↓a⇩_{1})⇧^{w}› (evaluated at world \emph{w}) is modelled as ‹⇃(Q,a⇩_{1})⇧^{w}› (or ‹(Q ⇃ a⇩_{1})⇧^{w}› using infix notation), which gets further translated into ‹Q(a⇩_{1}(w))⇧^{w}›. Depending on the particular types involved, we have to define ‹↓› differently to ensure type correctness (see \emph{a-d} below). Nevertheless, the essence of the \emph{Extension-of} operator remains the same: a term ‹α› preceded by ‹↓› behaves as a non-rigid term, whose denotation at a given possible world corresponds to the extension of the original intensional term ‹α› at that world. › text‹ (\emph{a}) Predicate ‹φ› takes as argument a relativized term derived from an (intensional) individual of type ‹↑𝟬›: › abbreviation extIndivArg::"↑⟨𝟬⟩⇒↑𝟬⇒io" (infix "⇃" 60) where "φ ⇃c ≡ λw. φ (c w) w" text‹ (\emph{b}) A variant of (\emph{a}) for terms derived from predicates (types of form ‹↑⟨t⟩›): › abbreviation extPredArg::"(('t⇒bool)⇒io)⇒('t⇒io)⇒io" (infix "↓" 60) where "φ ↓P ≡ λw. φ (λx. P x w) w" text‹ (\emph{c}) A variant of (\emph{b}) with a second argument (the first one being relativized): › abbreviation extPredArg1::"(('t⇒bool)⇒'b⇒io)⇒('t⇒io)⇒'b⇒io" (infix "↓⇩_{1}" 60) where "φ ↓⇩_{1}P ≡ λz. λw. φ (λx. P x w) z w" text‹ In what follows, the `‹⦇_⦈›' parentheses are an operator used to convert extensional objects into `rigid' intensional ones: › abbreviation trivialConversion::"bool⇒io" ("⦇_⦈") where "⦇φ⦈ ≡ (λw. φ)" text‹ (\emph{d}) A variant of (\emph{b}) where ‹φ› takes `rigid' intensional terms as argument: › abbreviation mextPredArg::"(('t⇒io)⇒io)⇒('t⇒io)⇒io" (infix "❙↓" 60) where "φ ❙↓P ≡ λw. φ (λx. ⦇P x w⦈) w" (* where "φ ❙↓P ≡ λw. φ (λx u. P x w) w"*) subsubsection ‹Equality› abbreviation meq :: "'t⇒'t⇒io" (infix"❙≈"60) ― ‹normal equality (for all types)› where "x ❙≈y ≡ λw. x = y" abbreviation meqC :: "↑⟨↑𝟬,↑𝟬⟩" (infixr"❙≈⇧^{C}"52) ― ‹eq. for individual concepts› where "x ❙≈⇧^{C}y ≡ λw. ∀v. (x v) = (y v)" abbreviation meqL :: "↑⟨𝟬,𝟬⟩" (infixr"❙≈⇧^{L}"52) ― ‹Leibniz eq. for individuals› where "x ❙≈⇧^{L}y ≡ ❙∀φ. φ(x)❙→φ(y)" subsubsection ‹Meta-logical Predicates› abbreviation valid :: "io⇒bool" ("⌊_⌋" [8]) where "⌊ψ⌋ ≡ ∀w.(ψ w)" abbreviation satisfiable :: "io⇒bool" ("⌊_⌋⇧^{s}⇧^{a}⇧^{t}" [8]) where "⌊ψ⌋⇧^{s}⇧^{a}⇧^{t}≡ ∃w.(ψ w)" abbreviation countersat :: "io⇒bool" ("⌊_⌋⇧^{c}⇧^{s}⇧^{a}⇧^{t}" [8]) where "⌊ψ⌋⇧^{c}⇧^{s}⇧^{a}⇧^{t}≡ ∃w.¬(ψ w)" abbreviation invalid :: "io⇒bool" ("⌊_⌋⇧^{i}⇧^{n}⇧^{v}" [8]) where "⌊ψ⌋⇧^{i}⇧^{n}⇧^{v}≡ ∀w.¬(ψ w)" subsection ‹Verifying the Embedding› text‹ The above definitions introduce modal logic \emph{K} with possibilist and actualist quantifiers, as evidenced by the following tests: › text‹ Verifying \emph{K} Principle and Necessitation: › lemma K: "⌊(❙□(φ ❙→ψ)) ❙→(❙□φ ❙→❙□ψ)⌋" by simp ― ‹\emph{K} schema› lemma NEC: "⌊φ⌋ ⟹ ⌊❙□φ⌋" by simp ― ‹necessitation› text‹ Local consequence implies global consequence (we will use this lemma often): › lemma localImpGlobalCons: "⌊φ ❙→ξ⌋ ⟹ ⌊φ⌋ ⟶ ⌊ξ⌋" by simp text‹ But global consequence does not imply local consequence: › lemma "⌊φ⌋ ⟶ ⌊ξ⌋ ⟹ ⌊φ ❙→ξ⌋" nitpick oops ― ‹countersatisfiable› text‹ Barcan and Converse Barcan Formulas are satisfied for standard (possibilist) quantifiers: › lemma "⌊(❙∀x.❙□(φ x)) ❙→❙□(❙∀x.(φ x))⌋" by simp lemma "⌊❙□(❙∀x.(φ x)) ❙→(❙∀x.❙□(φ x))⌋" by simp text‹ (Converse) Barcan Formulas not satisfied for actualist quantifiers: › lemma "⌊(❙∀⇧^{E}x.❙□(φ x)) ❙→❙□(❙∀⇧^{E}x.(φ x))⌋" nitpick oops ― ‹countersatisfiable› lemma "⌊❙□(❙∀⇧^{E}x.(φ x)) ❙→(❙∀⇧^{E}x.❙□(φ x))⌋" nitpick oops ― ‹countersatisfiable› text‹ Above we have made use of (counter-)model finder \emph{Nitpick} \<^cite>‹"Nitpick"› for the first time. For all the conjectured lemmas above, \emph{Nitpick} has found a countermodel, i.e. a model satisfying all the axioms which falsifies the given formula. This means, the formulas are not valid. › text‹ Well known relations between meta-logical notions: › lemma "⌊φ⌋ ⟷ ¬⌊φ⌋⇧^{c}⇧^{s}⇧^{a}⇧^{t}" by simp lemma "⌊φ⌋⇧^{s}⇧^{a}⇧^{t}⟷ ¬⌊φ⌋⇧^{i}⇧^{n}⇧^{v}" by simp text‹ Contingent truth does not allow for necessitation: › lemma "⌊❙◇φ⌋ ⟶ ⌊❙□φ⌋" nitpick oops ― ‹countersatisfiable› lemma "⌊❙□φ⌋⇧^{s}⇧^{a}⇧^{t}⟶ ⌊❙□φ⌋" nitpick oops ― ‹countersatisfiable› text‹ \emph{Modal collapse} is countersatisfiable: › lemma "⌊φ ❙→❙□φ⌋" nitpick oops ― ‹countersatisfiable› text‹ \pagebreak › subsection ‹Useful Definitions for Axiomatization of Further Logics› text‹ The best known normal logics (\emph{K4, K5, KB, K45, KB5, D, D4, D5, D45, ...}) can be obtained by combinations of the following axioms: › abbreviation M where "M ≡ ❙∀φ. ❙□φ ❙→φ" abbreviation B where "B ≡ ❙∀φ. φ ❙→❙□❙◇φ" abbreviation D where "D ≡ ❙∀φ. ❙□φ ❙→❙◇φ" abbreviation IV where "IV ≡ ❙∀φ. ❙□φ ❙→❙□❙□φ" abbreviation V where "V ≡ ❙∀φ. ❙◇φ ❙→❙□❙◇φ" text‹ Instead of postulating (combinations of) the above axioms we instead make use of the well-known \emph{Sahlqvist correspondence}, which links axioms to constraints on a model's accessibility relation (e.g. reflexive, symmetric, etc.; the definitions of which are not shown here). We show that reflexivity, symmetry, seriality, transitivity and euclideanness imply axioms $M, B, D, IV, V$ respectively. › lemma "reflexive aRel ⟹ ⌊M⌋" by blast ― ‹aka T› lemma "symmetric aRel ⟹ ⌊B⌋" by blast lemma "serial aRel ⟹ ⌊D⌋" by blast lemma "transitive aRel ⟹ ⌊IV⌋" by blast lemma "euclidean aRel ⟹ ⌊V⌋" by blast lemma "preorder aRel ⟹ ⌊M⌋ ∧ ⌊IV⌋" by blast ― ‹S4: reflexive + transitive› lemma "equivalence aRel ⟹ ⌊M⌋ ∧ ⌊V⌋" by blast ― ‹S5: preorder + symmetric› lemma "reflexive aRel ∧ euclidean aRel ⟹ ⌊M⌋ ∧ ⌊V⌋" by blast ― ‹S5› text‹ Using these definitions, we can derive axioms for the most common modal logics (see also \<^cite>‹"C47"›). Thereby we are free to use either the semantic constraints or the related \emph{Sahlqvist} axioms. Here we provide both versions. In what follows we use the semantic constraints (for improved performance). \pagebreak › (*<*) end (*>*)