The law of non-contradiction in Intuitionistic/Constructive logic

Question

I understand the arguments for why the law of non-contradiction and double negation elimination aren't equivalent in intuitionistic logic, and why the former is valid while the latter is not. From what I understand, it seems like the distinction mostly boils down to the fact that in intuitionistic logic we're allowed to introduce negations, but we aren't allowed to eliminate/cancel them out.

However there is a particular example I'm confused about. I'm looking at a theorem that can be proved using both a non-constructive proof and a constructive proof. As part of the constructive proof, we have to show that a number (which we'll call $b$) is irrational. In order to do so, we assume that it is rational, and then deduce a contradiction. What I'm confused about here is that it seems to me that whether or not this is a constructive proof entirely depends on how you 'label' each condition.

What I mean by this is, it seems like if we let $A = $'$b$ is rational', and then therefore have that $\neg A = $'$b$ is irrational', then disproving $A$ and applying the law of non-contradiction gives us a valid constructive proof that $b$ is irrational.

But it seems like if we switched things, and let $A = $'$b$ is irrational', and then therefore had that $\neg A = $'$b$ is rational', then once we disprove $\neg A$, we could only apply double negation elimination, and thus this would not be a valid constructive proof.

This then makes me think, what is to stop me from just switching the variables around like this for any problem I have (i.e. let $B = \neg A$ and thus let $\neg B = A$, in order to make the law of non-contradiction applicable and thus the proof a valid constructive proof.

I'm sure I'm missing something obvious here, but I'm very confused. I could potentially see an argument that the rejection of double negation elimination prevents me from switching around already established variables as I did just above, but for situations like my example, there aren't any established variables like this, and rationality and irrationality are opposite of each other, so there's not really any good reason to choose $A$ over $\neg A$ to represent rationality, other than the fact that I know how to show the former leading to a constructive proof.

EDIT: Almost as soon as I submitted this I think I may have figured it out, but I'm not sure so I'm going to leave the question up and add my idea here.

We have that the law of non-contradiction $\neg (A \land \neg A)$ is equivalent to $\neg A \lor \neg \neg A$, and so no matter what symbol we choose for rationality, the outcome is the same.

Answer 1

Sure enough, accepting a complementation that explicitly excludes the middle, means that you are no longer strictly using intuionistic logic.

It is accepting the claim that the rational numbers and irrational numbers are disjoint and exhaustive subsets of the real numbers, which allows you to say that when you have proven that a real number is not not irrational (double negative intended), then you have proven that it is irrational.

Answer 2

Long comment

For constructive reasoning, we have to take care of the interplay of quantifiers and negation.

A classically valid principle of reasoning is the indirect proof of the existence of an $A$s by assuming that there is no $x$ such that $A$, then deriving a contradiction, and concluding that such an $x$ exists.

Here the classical law of double negation is used for deriving $\exists x A$ from $\lnot \lnot \exists x A$.

This is not the same as the so-called principle of reductio ad absurdum used to prove a negative proposition: If $A$ leads to a contradiction, then $\lnot A$ can be inferred, principle that is intuitionistically valid.

Due to the lack of double negation, from a constructive point of view is necessary do not conflate the two patterns of reasoning above.

A typical example is the proof of irrationality of a real number $x$: Assume that $x$ is rational, derive a contradiction, and conclude that $x$ is irrational.

This is not an indirect proof, because "to be an irrational number" is a negative property: There do not exist integers $n, m$ such that $x = n/m$.

Thus, in a constructive setting, to derive a contradicition form the assumption that $x$ is irrational is not enough to prove its rationality, due to the lack of double negation.

Answer 3

The short answer is that being "not rational" is the same as being "irrational" by definition of irrational — however, being "not irrational" may be a weaker property than being "rational".

Deriving a contradiction from something being "irrational" merely lets you conclude that it is "not not rational".