1(*<*)2theoryAOT_model3importsMain"HOL-Cardinals.Cardinals"4begin56declare[[typedef_overloaded]]7(*>*)89section‹References›1011text‹
12A full description of this formalization including references can be found
13at @{url‹http://dx.doi.org/10.17169/refubium-35141›}.
1415The version of Principia Logico-Metaphysica (PLM) implemented in this formalization
16can be found at @{url‹http://mally.stanford.edu/principia-2021-10-13.pdf›}, while
17the latest version of PLM is available at @{url‹http://mally.stanford.edu/principia.pdf›}.
1819›2021section‹Model for the Logic of AOT›2223text‹We introduce a primitive type for hyperintensional propositions.›24typedecl𝗈2526text‹To be able to model modal operators following Kripke semantics,
27 we introduce a primitive type for possible worlds and assert, by axiom,
28 that there is a surjective function mapping propositions to the
29 boolean-valued functions acting on possible worlds. We call the result
30 of applying this function to a proposition the Montague intension
31 of the proposition.›32typedeclw―‹The primtive type of possible worlds.›33axiomatizationAOT_model_d𝗈::‹𝗈⇒(w⇒bool)›where34d𝗈_surj:‹surjAOT_model_d𝗈›3536text‹The axioms of PLM require the existence of a non-actual world.›37constsw⇩0::w―‹The designated actual world.›38axiomatizationwhereAOT_model_nonactual_world:‹∃w.w≠w⇩0›3940text‹Validity of a proposition in a given world can now be modelled as the result
41 of applying that world to the Montague intension of the proposition.›42definitionAOT_model_valid_in::‹w⇒𝗈⇒bool›where43‹AOT_model_valid_inwφ≡AOT_model_d𝗈φw›4445text‹By construction, we can choose a proposition for any given Montague intension,
46 s.t. the proposition is valid in a possible world iff the Montague intension
47 evaluates to true at that world.›48definitionAOT_model_proposition_choice::‹(w⇒bool)⇒𝗈›(binder‹ε⇩𝗈 › 8)49where‹ε⇩𝗈w.φw≡(invAOT_model_d𝗈)φ›50lemmaAOT_model_proposition_choice_simp:‹AOT_model_valid_inw(ε⇩𝗈w.φw)=φw›51by(simpadd:surj_f_inv_f[OFd𝗈_surj]AOT_model_valid_in_def52AOT_model_proposition_choice_def)5354text‹Nitpick can trivially show that there are models for the axioms above.›55lemma‹True›nitpick[satisfy, user_axioms, expect = genuine]..5657typedeclω―‹The primtive type of ordinary objects/urelements.›5859text‹Validating extended relation comprehension requires a large set of
60 special urelements. For simple models that do not validate extended
61 relation comprehension (and consequently the predecessor axiom in the
62 theory of natural numbers), it suffices to use a primitive type as @{textσ},
63 i.e. @{theory_text‹typedecl σ›}.›64typedeclσ'65typedefσ=‹UNIV::((ω⇒w⇒bool)set×(ω⇒w⇒bool)set×σ')set›..6667typedeclnull― ‹Null-urelements representing non-denoting terms.›6869