# Is there any work on the use of free logic in proof assistants?

I've been reading up on free logic. I have a hunch it could be useful for type theory. For example, the fixed point of an expression might not always exist or an expression might not be well typed in a different context or modality. I have some basic ideas but I would be really interested in seeing if free logic has shown up in the literature.

I would guess if universal instantiation corresponds to type preservation of substitution you want the following to be derivable.

$$\frac{\begin{split} \Gamma \vdash e_0 \colon \tau_0 \\ \Gamma, x \colon \tau_0 \vdash e_1 \colon \tau_1\\ \mathop{\text{E}!} e_0 \end{split}}{\Gamma \vdash [x := e_0] e_1 \colon \tau }$$

Also you want existence preservation

$$\frac{\begin{split} \Gamma \vdash e_0 \colon \tau_0 \\ \Gamma, x \colon \tau_0 \vdash e_1 \colon \tau_1\\ \mathop{\text{E}!} e_0 \\ \mathop{\text{E}!} e_1 \end{split}}{\mathop{\text{E}!}( [x := e_0] e_1) }$$

So taking the STLC as an example, function application ought to be guarded by an existence check as well as any other place that might infect a variable.

$$\frac{\begin{split} \Gamma \vdash e \colon \tau \rightarrow \tau'\\ \Gamma \vdash e' \colon \tau \\ \Gamma \vdash \mathop{\text{E}!} e' \end{split}}{\Gamma \vdash e e' \colon \tau' }$$

An existence judgement is mostly just crawling over terms

$$\mathop{\text{E}!} x$$

$$\frac{\begin{split}\mathop{\text{E}!} e \\ \mathop{\text{E}!} e' \end{split}}{\mathop{\text{E}!} (e e')}$$

$$\frac{\mathop{\text{E}!} e}{\mathop{\text{E}!} (\lambda x\colon \tau. e)}$$

You ought to be able to use free logic to add a description operator but the details are tricky. To avoid dealing with predicates directly you could maybe use the image of a function.

$$\frac{\Gamma, x\colon \tau_1 \vdash e \colon \tau_2 }{\Gamma \vdash \{ e \mid x\colon \tau_1 \} \colon \tau_2}$$ $$\frac{\begin{split} \mathop{\text{E!}} e_2\\ \bullet \vdash e_2 \colon \tau \\ \mathop{\text{E!}} ( [x := e_2] e_1) \end{split}}{\mathop{\text{E!}} \{ e_1 \mid x\colon \tau \} }$$

$$\frac{\begin{split}\mathop{\text{E!}} e_2 \\ \bullet \vdash e_2 \colon \tau \\ [x := e_2] e_0 \equiv e_1 \end{split}}{\{ e_0 \mid x\colon \tau \} \equiv e_1}$$