2
$\begingroup$

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}$$

$\endgroup$

1 Answer 1

3
$\begingroup$

A professor at my university (and its research group) is using free logic in Isabelle/HOL. For example, here (https://bibbase.org/network/publication/benzmller-scott-automatingfreelogicinholwithanexperimentalapplicationincategorytheory-2020) is a paper where they use free logic to deal with the only partially defined composition in categories. Isabelle/HOL does not have dependent types.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.