David Corfield de dicto-de re

Idea

Use the type-theoretic account of definite description.

Say I have a type A, and have judged that $(a, b): IsContr(A)$ (so a: A, and b witnesses its uniqueness). Then I’m allowed to define ‘The A’ as a: A. Then I may use this term de re.

On the other hand, say I know merely that A can’t not be contractible, since I’ve proved this by contradiction. Even without the witness, I may still say ‘The A’ and be able to assert properties it possesses. Especially if $A$ is a finite set.

The murderer of X (whoever they may be) must be insane (by virtue of this deed).

Perhaps the latter de dicto form could be seen in hypothetical terms. If there is such a thing as `The A', then it must be $\phi$.

$$(x, y): IsContr(A) \vdash p(x, y): \phi(x)$$

Also possible worlds semantics, 35th Potus and Nixon.

35th Potus(a) = Nixon(a)