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.