Theory IHOML
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_synonym io = "(i⇒bool)"
typedecl e ("𝟬")
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)
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)
where "❙∀⇧Ex. φ(x) ≡ ❙∀⇧Eφ"
abbreviation mexistsActB :: "↑⟨↑⟨𝟬⟩⟩" (binder"❙∃⇧E"[8]9)
where "❙∃⇧Ex. φ(x) ≡ ❙∃⇧Eφ"
subsubsection ‹Modal Operators›
consts aRel::"i⇒i⇒bool" (infixr "r" 70)
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 "φ ↓⇩1P ≡ λ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"
subsubsection ‹Equality›
abbreviation meq :: "'t⇒'t⇒io" (infix"❙≈"60)
where "x ❙≈ y ≡ λw. x = y"
abbreviation meqC :: "↑⟨↑𝟬,↑𝟬⟩" (infixr"❙≈⇧C"52)
where "x ❙≈⇧C y ≡ λw. ∀v. (x v) = (y v)"
abbreviation meqL :: "↑⟨𝟬,𝟬⟩" (infixr"❙≈⇧L"52)
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
lemma NEC: "⌊φ⌋ ⟹ ⌊❙□φ⌋" by simp
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
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 "⌊(❙∀⇧Ex.❙□(φ x)) ❙→ ❙□(❙∀⇧Ex.(φ x))⌋" nitpick oops
lemma "⌊❙□(❙∀⇧Ex.(φ x)) ❙→ (❙∀⇧Ex.❙□(φ x))⌋" nitpick oops
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
lemma "⌊❙□φ⌋⇧s⇧a⇧t ⟶ ⌊❙□φ⌋" nitpick oops
text‹ \emph{Modal collapse} is countersatisfiable: ›
lemma "⌊φ ❙→ ❙□φ⌋" nitpick oops
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
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
lemma "equivalence aRel ⟹ ⌊M⌋ ∧ ⌊V⌋" by blast
lemma "reflexive aRel ∧ euclidean aRel ⟹ ⌊M⌋ ∧ ⌊V⌋" by blast
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