Are there any provers based on a paraconsistent logic?

Question

This question talks about controlled usage of a self-containing top type satisfying $\text{type}\! : \text{type}$.

I'm wondering if there are any provers that deliberately give $\text{type}\!: \text{type}$ a designated truth value, but still make it paradoxical.

(Note: I'm using the term prover generically to refer to a proof assistant or automated theorem prover.)

---

This would require weakening the propositional (fragment of the) logic used by the prover in question.

There are some paraconsistent logics out there where $A \land \lnot A$ is not a contradiction, or, equivalently, $A$ and $\lnot A$ are not mutually exclusive.

For example, the Logic of Paradox is paraconsistent as is the relevant logic R.

Answer 1

I am not sure this is the answer you are looking for, but here it is anyways.

In the proof-as-program paradigm embraced by dependent type theory, inconsistency is not necessarily an issue. Indeed, one does not only care about the truth value of a given statement, as you seem to imply, but also about the computational content of proofs of that statement. For instance, the bool type is inhabited but nobody will ever conflate it with the unit type, which is also inhabited.

All mainstream functional programming languages are inconsistent when seen as logical systems, because using ML syntax it is possible to write a proof boom : unit -> 'a as a non-terminating loop let rec boom () = boom (). When seen through the Curry-Howard mirror, boom () is actually a proof of an arbitrary theorem. Yet nobody complains that such languages allow writing non-terminating programs.

By contrast, most dependent type theories prevent this kind of situation by restricting side-effects in general, and non-termination in particular. It is nonetheless possible to design impure dependent type theories, resulting in an inconsistent logical system but a perfectly fine dependently-typed programming language. A simple example of such an object is the Exceptional Type Theory (ExTT) which can be given as a program translation from MLTT to itself. Because of this you can systematically write ExTT programs in pretty much any proof assistant based on MLTT, through a simple transpilation phase.

ExTT allows raising exceptions, and thus inhabit any type. Still, the equational theory is not degenerate and you get a decent language. Moreover, the target theory also allows to reason safely about those programs and ensure that in some cases, the exception-raising terms are actually well-behaved and do not raise toplevel exceptions. In the end, paraconsistency is in the eye of the beholder.

Answer 2

I don't know if this is a satisfactory example, however Yatsuka Nakamura's THEAX system is inconsistent. There was no intentionality on Nakamura's part; indeed, he discusses the problem in the technical report. Then he solved it by joining Mizar; in fact, Nakamura is one of the historical contributors to Mizar's library and the second most prolific after Yasunari Shidama.