David Corfield
free logic


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 DD.

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

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

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

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

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


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

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

Last revised on May 5, 2021 at 17:28:36. See the history of this page for a list of all contributions to it.