Theory ExtendedDDL
theory ExtendedDDL
imports CJDDLplus
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3]
section ‹Extending the Carmo and Jones DDL Logical Framework›
text‹\noindent{In the last section, we have modelled Kaplanian contexts by introducing a new type of object (type c) and modelled
sentence meanings as so-called "characters", i.e. functions from contexts to sets of worlds (type ‹c⇒w⇒o›).
We also made the corresponding adjustments to the original semantic embedding of Carmo and Jones' DDL \<^cite>‹"C71"› \<^cite>‹"BenzmuellerDDL"›.
So far we haven't said much about what these Kaplanian contexts are or which effect they should have on the evaluation
of logical validity. We restricted ourselves to illustrating that their introduction does not have any influence
on the (classical) modal validity of several DDL key theorems.
In this section we introduce an alternative notion of logical validity suited for working with contexts:
indexical validity \<^cite>‹"Kaplan1979"› \<^cite>‹"Kaplan1989"›.}›
subsection ‹Context Features›
text‹\noindent{Kaplan's theory ("Logic of Demonstratives" \<^cite>‹"Kaplan1979"›) aims at modelling the behaviour of
certain context-sensitive linguistic expressions like
the pronouns 'I', 'my', 'you', 'he', 'his', 'she', 'it', the demonstrative pronouns 'that', 'this', the adverbs 'here', 'now',
'tomorrow', 'yesterday', the adjectives 'actual', 'present', and others. Such expressions are known as "indexicals"
and so Kaplan's logical system (among others) is usually referred to as a "logic of indexicals" (although
in his seminal work he referred to it as a "logic of demonstratives" (LD)) \<^cite>‹"Kaplan1979"›.
In the following we will refer to Kaplan's logic as the logic "LD".
It is characteristic of an indexical that its content varies with context, i.e. they have a context-sensitive character.
Non-indexicals have a fixed character. The same content is invoked in all contexts.
Kaplan's logical system models context-sensitivity by representing contexts as tuples of features
(‹⟨Agent(c), Position(c), World(c), Time(c)⟩›). The agent and the position of context c can be seen as the actual speaker
and place of the utterance respectively, while c's world and time stand for the circumstances of evaluation of the
expression's content and allow for the interaction of indexicals with alethic and tense modalities respectively.}›
text‹\noindent{To keep things simple (and relevant for our task) we restrict ourselves to representing a context c as the pair: ‹⟨Agent(c), World(c)⟩›.
For this purpose we represent the functional concepts "Agent" and "World" as logical constants.}›
consts Agent::"c⇒e"
consts World::"c⇒w"
subsection ‹Logical Validity›
text‹\noindent{Kaplan's notion of (context-dependent) logical truth for a sentence corresponds to its (context-sensitive) formula
(of type ‹c⇒w⇒bool› i.e. m) being true in the given context and at its corresponding world.}›
abbreviation ldtruectx::"m⇒c⇒bool" ("⌊_⌋⇩_") where "⌊φ⌋⇩c ≡ φ c (World c)"
text‹\noindent{Kaplan's LD notion of logical validity for a sentence corresponds to its being true in all contexts.
This notion is also known as indexical validity.}›
abbreviation ldvalid::"m⇒bool" ("⌊_⌋⇧D") where "⌊φ⌋⇧D ≡ ∀c. ⌊φ⌋⇩c"
text‹\noindent{Here we show that indexical validity is indeed weaker than its classical modal counterpart (truth at all worlds for all contexts):}›
lemma "⌊A⌋ ⟹ ⌊A⌋⇧D" by simp
lemma "⌊A⌋⇧D ⟹ ⌊A⌋" nitpick oops
text‹\noindent{Here we show that the interplay between indexical validity and the DDL modal and deontic operators does not
result in modal collapse.}›
lemma "⌊P ❙→ ❙O⇩aP⌋⇧D" nitpick oops
lemma "⌊P ❙→ ❙□⇩aP⌋⇧D" nitpick oops
text‹\noindent{Next we show that the necessitation rule does not work for indexical validity (in contrast to classical modal validity as defined for DDL).}›
lemma NecLDa: "⌊A⌋⇧D ⟹ ⌊❙□⇩aA⌋⇧D" nitpick oops
lemma NecLDp: "⌊A⌋⇧D ⟹ ⌊❙□⇩pA⌋⇧D" nitpick oops
text‹\noindent{The following can be seen as a kind of 'analytic/a priori necessity' operator (to be contrasted to the more
traditional alethic necessity).
In Kaplan's framework, a sentence being logically (i.e. indexically) valid means its being true \emph{a priori}: it is guaranteed to be true
in every possible context in which it is uttered, even though it may express distinct propositions in different contexts. This correlation
between indexical validity and \emph{a prioricity} has also been claimed in other two-dimensional semantic frameworks \<^cite>‹"SEP2DSem"›.}›
abbreviation ldvalidbox :: "m⇒m" ("❙□⇧D_" [52]53) where "❙□⇧Dφ ≡ λc w. ⌊φ⌋⇧D"
lemma "⌊❙□⇧Dφ⌋⇩C ≡ ∀c.⌊φ⌋⇩c" by simp
text‹\noindent{Quite trivially, the necessitation rule works for the combination of indexical validity with the previous operator.}›
lemma NecLD: "⌊A⌋⇧D ⟹ ⌊❙□⇧DA⌋⇧D" by simp
text‹\noindent{The operator above is not part of the original Kaplan's LD (\<^cite>‹"Kaplan1979"›) and has been added
by us in order to better highlight some semantic features of our formalisation of Gewirth's argument in the next section and to being able to
use the necessitation rule for some inference steps.}›
subsection ‹Quantification›
text‹\noindent{ We also enrich our logic with (higher-order) quantifiers (using parameterised types).}›
abbreviation mforall::"('t⇒m)⇒m" ("❙∀") where "❙∀Φ ≡ λc w.∀x. (Φ x c w)"
abbreviation mexists::"('t⇒m)⇒m" ("❙∃") where "❙∃Φ ≡ λc w.∃x. (Φ x c w)"
abbreviation mforallBinder::"('t⇒m)⇒m" (binder"❙∀"[8]9) where "❙∀x. (φ x) ≡ ❙∀φ"
abbreviation mexistsBinder::"('t⇒m)⇒m" (binder"❙∃"[8]9) where "❙∃x. (φ x) ≡ ❙∃φ"
end