Theory AOT_model
theory AOT_model
imports Main "HOL-Cardinals.Cardinals"
begin
declare[[typedef_overloaded]]
section‹References›
text‹
A full description of this formalization including references can be found
at @{url ‹http://dx.doi.org/10.17169/refubium-35141›}.
The version of Principia Logico-Metaphysica (PLM) implemented in this formalization
can be found at @{url ‹http://mally.stanford.edu/principia-2021-10-13.pdf›}, while
the latest version of PLM is available at @{url ‹http://mally.stanford.edu/principia.pdf›}.
›
section‹Model for the Logic of AOT›
text‹We introduce a primitive type for hyperintensional propositions.›
typedecl 𝗈
text‹To be able to model modal operators following Kripke semantics,
we introduce a primitive type for possible worlds and assert, by axiom,
that there is a surjective function mapping propositions to the
boolean-valued functions acting on possible worlds. We call the result
of applying this function to a proposition the Montague intension
of the proposition.›
typedecl w
axiomatization AOT_model_d𝗈 :: ‹𝗈⇒(w⇒bool)› where
d𝗈_surj: ‹surj AOT_model_d𝗈›
text‹The axioms of PLM require the existence of a non-actual world.›
consts w⇩0 :: w
axiomatization where AOT_model_nonactual_world: ‹∃w . w ≠ w⇩0›
text‹Validity of a proposition in a given world can now be modelled as the result
of applying that world to the Montague intension of the proposition.›
definition AOT_model_valid_in :: ‹w⇒𝗈⇒bool› where
‹AOT_model_valid_in w φ ≡ AOT_model_d𝗈 φ w›
text‹By construction, we can choose a proposition for any given Montague intension,
s.t. the proposition is valid in a possible world iff the Montague intension
evaluates to true at that world.›
definition AOT_model_proposition_choice :: ‹(w⇒bool) ⇒ 𝗈› (binder ‹ε⇩𝗈 › 8)
where ‹ε⇩𝗈 w. φ w ≡ (inv AOT_model_d𝗈) φ›
lemma AOT_model_proposition_choice_simp: ‹AOT_model_valid_in w (ε⇩𝗈 w. φ w) = φ w›
by (simp add: surj_f_inv_f[OF d𝗈_surj] AOT_model_valid_in_def
AOT_model_proposition_choice_def)
text‹Nitpick can trivially show that there are models for the axioms above.›
lemma ‹True› nitpick[satisfy, user_axioms, expect = genuine] ..
typedecl ω
text‹Validating extended relation comprehension requires a large set of
special urelements. For simple models that do not validate extended
relation comprehension (and consequently the predecessor axiom in the
theory of natural numbers), it suffices to use a primitive type as @{text σ},
i.e. @{theory_text ‹typedecl σ›}.›
typedecl σ'
typedef σ = ‹UNIV::((ω ⇒ w ⇒ bool) set × (ω ⇒ w ⇒ bool) set × σ') set› ..
typedecl null