The LNC as a mathematical theorem

Question

One of the most intriguing things I've read about over the last few years is Diaconescu's theorem, which says that, in some forms of constructivist/intuitionistic set theory, even if the law of the excluded middle is not presupposed in the background logic, the LEM is still a theorem under a set-theoretic principle, the axiom of choice. Hence, to remain constructive, that kind of set theory has to reject the AC, which is not necessarily appealing to constructivists, at least one of whom (Bishop) has claimed that the AC is constructively plausible, as he said something like "a choice is presupposed by the very concept of existence".

Now, as far as I can tell, the law of noncontradiction is not quite an axiom in normal modern logic, but instead a theorem of the argument from explosions. I'm wondering, though, if there is a set-theoretic, or at least broadly "mathematical," principle that does the same for the LNC as the AC does for the LEM? This is all I've come up with so far:

Let $$\mathfrak{j}(S) = a$$ be the justification function on sentences S, where 𝑎 = the justification value (c.f. Fregean truth values) of S. Assume the following:

1. $$\mathfrak{j}(A \land B) = \mathfrak{j}(A) + \mathfrak{j}(B)$$
2. $$(\mathfrak{j}(A) > 0) \rightarrow (\mathfrak{j}(\neg A) < 0)$$ also $$(\mathfrak{j}(A) = x) \rightarrow (\mathfrak{j}(\neg A) = -x)$$
3. $$\Box(\mathfrak{j}(B) = 0) \rightarrow \neg B$$

Then $$\mathfrak{j}(A \land \neg A) = \mathfrak{j}(A) + \mathfrak{j}(\neg A) = x + (-x) = x - x = 0$$

["Modalized"] Then $$\Box(\mathfrak{j}(A \land \neg A) = 0)$$ i.e. the LNC is (via (3)) true. QED

When using (3), one must proceed with caution. Taking the concept of justification in play to be stated in terms of something like abstract evidentialism, (3) is perilously close to Fitch's paradox of knowability, which says that if all truths can be known, then all of them are, wherefore it follows that there apparently must be unknowable truths (or else we would be hyperlogically omniscient). So for now, I would recommend limiting the domain of the justification function as such, to a closed-off set-theoretic or category-theoretic mathematical universe.

Another problem I'm having with how I've formulated the argument is that (2) seems to involve double-negation introduction, and anyway the whole idea has it that negative numbers are more elementary than they are in normal set theory (e.g. if we style the logic along the lines of a Boolean algebra augmented by a negative unit of antijustification value). IIRC, constructivists/intuitionists reject DN elimination, but not necessarily DN introduction. So if I was trying to maneuver around the ~LEM crowd, here, maybe I pulled the maneuver off with respect to (2), as it resembles DNI more than DNE. Still, I've never felt that DNI/E were far off from the LNC, either; I didn't see too much difference between the following:

1. $$\neg(x = \neg x)$$
2. $$x ≠ \neg x$$
3. $$\neg\neg x = x$$
4. $$x = \neg\neg x$$

According to one common and at least moderately strong argument, the semantic content/identity of the negation operator is equivalent to the LNC. I would say, though, that DNI/E, which "look like" the law of identity, are the content/identity in question. By contrast, the LNC seems like the identity law applied to the negation and conjunction operators together (and the LEM "looks like" identity + negation + disjunction).

Are there any set/category/other such theories, in which a mathematical principle generates the LNC? I tried Googling "law of noncontradiction is a theorem" but the only seemingly relevant result I remember seeing had something to do with Hegel-style dialectical logic or whatever.

Answer 1

Non-contradiction can only be a mathematical theorem, rather than a logical assumption, against a background of some logic which does not already contain it. One of the few well-motivated systems with that property is relevant logic.

So the best answer to your question would be some mathematical theory, like a relevant theory of arithmetic $T$, using relevant logic, for which $T\vdash PA$. Then non-contradiction for arithmetic statements would follow from the logic and arithmetic together but not from the logic alone.

One place to start looking for such a theory is Friedman and Meyer’s 1971 paper Whither Relevant Arithmetic. Their theory $RA$ of relevant arithmetic does not imply all the theorems of $PA$, and they considered bridging the gap with an $\omega$-rule.

You could look for arithmetical axioms to bridge the gap also, motivated by the arithmetical results left unproved by their theory $RA$. Any such axioms would give a positive answer to your question.