A Paraconsistent Type Theory
In formal logic consistency is defined as follows: A system is consistent if there exists at least one statement that cannot be proven. This definition uses the “principle of explosion”. Once a single contradiction is proven, the entire logic explodes, you can use that to prove any other statement. When everything is provable the system becomes trivial and useless. In type theory there is an equivalent definition using the Curry-Howard correspondence: ...