Type theory and constructivist mathematics with paraconsistent logic?

Question

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs from classical logic in that it doesn’t have the law of excluded middle as a logical axiom/derivation rule. But it does have the principle of explosion: From a proof of False, anything can be derived. Is there a serious attempt to study what can and cannot be proven within mathematics if one takes intuitionistic logic, and drops the axiom that anything can be derived from a proof of False?

Answer 1

In general, there are credible early attempts to study aspects of mathematics in the context of paraconsistent calculi (there are many, just look at the ToC of Priest's textbook).

That said, the answer to the precise question you actually asked, the one regarding type theory, is negative.

In type theory (as in most foundational systems), the statement $0=1$ is naturally explosive, in the sense that you can prove anything using $0=1$ without ever invoking $\bot$-elimination. Why? As in my answer to your other question about type theory, given types $A,B$, you can use $\mathbb{N}$-induction to construct a function $f: \mathbb{N} \rightarrow \mathcal{U}$ such that $f(0)$ reduces to $A$ and $f(Sn)$ reduces to $B$. Applying the congruence rule to $0=1$ yields $A = B$, so all types are equal, and in particular $A \rightarrow B$ holds. In fact, Martin-Löf type theory is maximally explosive: if you can inhabit a type $T$ in the empty context without using $\bot$-elimination, an induction on the structure of the proof shows that you could have inhabited the type $T^{\bot \leftarrow 0=1}$, the type obtained from $T$ by replacing every occurrence of $\bot$ with $0=1$. There is nothing specific about $0=1$ here: Martin-Löf type theory without explosion is really just a world where $\bot$ denotes an arbitrary proposition. In particular, if $A$ does not mention $\bot$, then MLTT without explosion proves $A \rightarrow \bot$ precisely if $A$ is explosive.

This means that, as long as you don't intend to add new, classically inadmissible principles, there is not much point in studying these "minimal" type theories based on minimal logic. The situation is more interesting in e.g. the variant of Heyting arithmetic that uses minimal logic instead of intuitionistic logic as its logical substrate. This theory is almost, but not quite, the same as full intuitionistic Heyting arithmetic, since $0=1$ is explosive.

For example, if you want to prove using $0=1$ that every number is even, you can multiply the inconsistent equality by $2$ to get $0=2$, apply transitivity to get $1=2$, then replace $1$ with $2$ in $\forall x. 1x = x$ to conclude $\forall x. 2x=x$, and then $\forall x. \exists y. 2y=x$. You can do this systematically (by induction on the structure of the formula $A$) to prove that $0 = 1 \rightarrow A$.

This time, the converse does not hold, and Heyting arithmetic formulated in minimal logic is not maximally explosive: there are positive statements that it proves false, but that are not explosive. That's because one of the axioms of Heyting arithmetic says something non-trivial about $\bot$. There are two ways to conclude $\bot$ in Heyting arithmetic:

1. From an induction axiom. This is not a problem: when you replace all occurrences of $\bot$ with $0=1$ in an induction axiom, the result is another induction axiom. (This is the only case in MLTT, which is why it justifies explosion.)

2. By applying the non-logical axiom $\forall x. 0 = Sx \rightarrow \bot$ to some $St = 0$. The problem is that you cannot replace this axiom with $\forall x. 0 = Sx \rightarrow 0 = 1$: it takes some work to show that this really cannot be done: it turns out that $0 = 2$ does not provably imply $0=1$ if you formulate Heyting arithmetic inside minimal logic. For details you can consult Heerkens' MSc thesis.

This is, however, the only obstacle: you replace $\forall x. 0 = Sx \rightarrow \bot$ with $\forall x. 0 = Sx \rightarrow 0 = 1$, and you get a minimal arithmetic that coincides perfectly with intuitionistic Heyting arithmetic. One can argue that this modified axiom is philosophically justified purely on basis of what we want arithmetic to be.