David Corfield free logic

• SEP

It seems to arise from an extrinsic way of thinking. We have a term. We don’t know if it refers. We can’t assign it the standard domain, type $D$.

Free logic could be seen as an order-sorted logic. Two sorts, $i: D \hookrightarrow E$, where existence is $\exists_D$. Then the coercion is left implicit.

$i^{\ast}$ pulls back predicates on $E$ to predicates on $D$. $\exists x(x = t)$ for $t: E$ is really $\sum_{x: D} i*(x = t)$.

Talk of ‘inner’ and ‘outer’ quantifiers is just, e.g., $\sum_D$ and $\sum_E$. The inner quantifiers defined in terms of the outer quantifiers are:

• $\forall x A =_{def} \Pi x(E!x \rightarrow A)$
• $\exists x A =_{def} \Sigma x(E!x \& A)$

These are just an expression of the fact that since $!_E \cdot i = !_D$, then $\sum_E \sum_i = \sum_D$ and $\prod_E \prod_i = \prod_D$.

Examples

One obvious choice derives from the unit of a possibility monad, $D \hookrightarrow \bigcirc_W D$. Indeed one use of free logic is to discuss possible entities.

Or maybe actualised, $D(a) \hookrightarrow \bigcirc_W D(a)$.