Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
started a minimum at de dicto and de re, mainly such as to have a place to point to section 4 of
I expanded this a bit,
I think I’m still struggling with these quantifier-modal operator mixes, but maybe that’s because of the way I’d like to set things up.
If we take a type, say $People(w)$, to be dependent on a collection of worlds $W$, then maybe we want to say that
So that’s fine read the de dicto way. The property of being oldest is world dependent. In each world there’s an oldest, so necessarily there’s an oldest person.
Now the de re way, I need a notion of a person as existing across the worlds. This is why Awodey-Kishida have sheaves in their models.
Perhaps we needed our $W$ to be a groupoid, or we represent the accessibility relation $W \to W'$.
Coming back to this, it suggests having a type base changed along $W \times X \to X$, so $\mathbf{H}/X \to \mathbf{H}/X \times W$ to allow either order of quantifier and modality.
’Transworld identity’ keeps cropping up.
The worries in #3 and #4 are that what we have on this page is incompatible with necessity and possibility. So here we have:
In modal logic a proposition involving the consecutive application of a modal operator and an existential quantifier is called
de dicto if the modal operator is applied after the quantifier
$\Box \underset{x \colon X}{\exists} A(x)$;
de re if it is the other way around
$\underset{x \colon X}{\exists} \Box A(x)$;
Where elsewhere we’ve set the modalities to work on world dependent types:
$(\underset{W}{\lozenge} \dashv \underset{W}{\Box}) \coloneqq \left( \left( W^\ast \circ \underset{w\colon W}{\exists} \right) \dashv \left( W^\ast \circ \underset{w\colon W}{\forall} \right) \right) \;\colon\; \mathbf{H}_{/W} \longrightarrow \mathbf{H}_{/W} \,.$De dicto, I could mean by $\Box \underset{x \colon X}{\exists} A(x)$ that we have a world-dependent type $X(w)$, and then put $\Box_W \underset{x \colon X(w)}{\exists} A(w, x)$. But this $A$ is a dependent type $w: W, x:X(w) \vdash A(w, x):Prop$.
However, de re, I need to have world-independent $X$, to allow the modal operator $\Box_W: \mathbf{H}/(X \times W) \to \mathbf{H}/(X \times W)$ and then $\underset{x \colon X}{\exists}: \mathbf{H}/(X \times W) \to \mathbf{H}/W$.
So
the failure of a modal operator to commute with base change
is not quite so straightforward.
1 to 5 of 5