Problems with validity in type theory

Question

I'm twisting my brains over some simple formulas in intensional type theory.

First:

If $\exists x \Box (x=^{\vee}j)$, s.t. $x$ is of type $<e>$ and refers to an entity $e$ and $j$ is of type $<s,e>$, refering to a function from possible worlds to intensional entities and $^{\vee}$ refers to the extension of $j$, I wonder is $\exists x \Box (x=^{\vee}j)$ valid?

I'm thinking on the hand that since extensions of an intensional expression are allowed to vary from one world to another on this theory, we cannot obtain a fixed constant $c$ of type $<e>$, being equivalent to the extension of $j$, for every possible world? But on the other hand, isn't it the case that constats aren't rigid on this theory, so that there are no grounds for saying that even a constant $c$ refers to a single entity e in every possible world?

Second:

If $\exists x \Box(^{\wedge}x=j)$ where $x$ is of type $<e>$ and $j$ is of type $<s,e>$ and $^{\wedge}$ refers to the intension of $x$, is $\exists x \Box(^{\wedge}x=j)$ valid?

Here my primary concerns really revolve around the concept of intension. If $^{\wedge}x$ was substituted for $j$ of type $<s,e>$ let's say, would that make the equivalence valid? Would the intensions then be equivalent on every world? Is it saying something like $\Box(Mark Twain=Mark Twain)$ even if $\neg\Box(Mark Twain=Samuel Clemens)$ intensionally conceived? And could the former be granted for $\exists x \Box(^{\wedge}x=j)$? Mainly, is there a case where two intensional expressions are necessarily equivalent?

Answer 1

Regarding : $∃x \square (x=^{\vee} j)$, you are right; in order to compute its truth-value, we have to "unwind" the semantical specifications of Definition 4, page 123.

We have that :

$[[∃x \square (x=^\lor j)]]=1$ iff for some $d \in D, [[\square (x=^{\vee} j)]]_{M,w,g(x/d)} = 1$,

where $x$ is a variable of type $e$ and $j$ a constant of the same type.

This in turn holds iff for all $w' \in W : [[(x=^{\vee} j)]]_{M,w',g(x/d)} = 1$.

For the constant $j$, according to clause (ix), we have that $I(j) \in D^W$, i.e. $I(j)$ is a function mapping possible worlds into elements of $D$, and thus $I(j)(w)$ is an element of $D$, the reference of $j$ in $w$.

But it is not an individual constant $c$; thus its reference is not the same in every world.

We have that [page 57] :

in every world $w, I_w(=) = \{ (d,d) | d \in D_w \}$;

thus, we cannot conclude that :

for all $w' \in W : d = I(j)(w')$,

and so :

$∃x \square (x=^{\vee} j)$ is not valid.

---

With $∃x \square(^{\wedge} x=j)$, we have that $(^{\wedge} x=j)$ is a function from possible worlds into an open formula, i.e. an object of type $<s, <e,t>>$; accordingly, having chosen $d \in D$, we have that $[(^{\wedge} x=j)]_{M,g(x/d)}$ is a sentence, i.e. an object of type $<s,t>$.

Again we must have :

$[[∃x \square(^{\wedge} x=j)]] = 1$ iff for some $d \in D$ and for all $w' \in W : [[(^{\wedge} x=j)]]_{M,w',g(x/d)} = 1$.

Now we have to apply cluase (viii) : $[[(^{\wedge} x=j)]]_{M,w',g(x/d)}$ is that function $h \in \{ 0,1 \}^w$ such that for all $w' \in W : h(w') = 1$ iff $d = I(j)(w')$, and thus :

$∃x \square (^{\wedge} x=j)$ is valid.