# Does the notion of logical independence make sense in constructive mathematics?

I have been learning a bit about constructive mathematics and intuitionistic logic and I think I am correct in understanding that a philosophical difference between constructive and classical logic is that in classical logic, at any given moment, the truth value of every proposition is decided (since it is bivalent) and then we seek to establish or discover that truth value by means of proof. The motivation for intuitionstic logic (at least according to some sources) is that exhibiting the proof of an assertion is what defines the truthity of a proposition, thus deciding the truth value upon discovery of the proof.

Now, I am aware of independence results (CH, AC, unfortunately all of them seem to be in the language of set theory..) which I have always interpreted these results as saying "there is no proof this proposition, and there is also no proof of its negation" thus saying we have some $$P$$ for which you cannot prove or disprove $$P$$. Considering this concept in classical logic, which is bivalent, the true truth value of $$P$$ is decided, but the independence proof says we will never have proof the reveals the information. It is also my understanding that the way these proofs work is to show that $$\{ \text{axioms} \} + P$$ is relatively consistent (meaning that if we assume the axioms are consistent, then adding $$P$$ remains consistent, meaning no contradictions).

My (big) question is: Does the idea of independence make sense in classical logical? It seems that it might need to be adapted a bit since "the negation of P" in constructive logic is defined differently.

My immediate thought is that since standard formulations of constructive logic is strictly weaker than classical logic, and you can achieve classical logic by adding in LEM, double negation, etc. then any independent proposition should remain independent when interpreted in constructive logic.

If everything up until here makes sense, and the notion of independence makes sense when doing constructive mathematics,

then my more refined questions is - are there any mathematical propositions that are provably decided in classical logic, but when viewed in constructive logic they become independent. To be clear, I do not mean just that we have not yet found a proof of the proposition, but that one can show there is no proof of $$P$$ or its negation.

Lastly, would the interpretation of an independent statement in constructive logic mean that the statement has no truth value? As opposed to classical logic where it has one, you just can't ever know it?

• Yes, I think I mention all of these things in my post (like, almost verbatim) Commented Nov 6, 2019 at 8:39
• To the mathematician in constructive mathematics, a proposition $P$ for which a proof has not been discovered currently has no definite truth value - but it could be any day which a proof could be discovered, yes? But it still makes sense to wonder "what if a proof of this $P$ does not exist", no? Commented Nov 6, 2019 at 8:42
• An example of a theorem that can be formulated , but not proven within the peano axioms is Goodstein's theorem. This is an example of a theorem that is independent from PA, neither provable nor disprovable. I think, you are away of Goedel's incompleteness theorems and the theorem that a statement is provable if and only if it is true under every interpretation. Commented Nov 6, 2019 at 13:01

$$\newcommand{\P}{\mathcal{P}}$$
Depending on what objects we're allowed to form, there are easy examples. For instance, consider a constructive set theory. There's a singleton set, say: $$1 = \{\{\}\}$$
and it has a power set: $$Ω = \P1$$
Now, consider the proposition: $$∀ x \in Ω. x = 1 ∨ x = 0$$ where $$0$$ is the empty set. Classically this is true because it is equivalent to excluded middle. Constructively it is independent unless we add some anti-classical axioms.
• For my argument to work, it must be the same sort of definition as the classical power set. Here, the set of all subsets of $1$, the elements of which you might think of as $\{\{\}|φ\}$ for any proposition $φ$. The idea is that constructively, there is no method for determining whether an arbitrary subset is $1$ or $0$, because that would be equivalent to deciding the $φ$ used to define it. So you can alternately think of my example as a way of saying $∀P. P ∨ ¬P$ without having to assume we can 'quantify' over propositions (since I assume that's a foreign idea). Commented Nov 7, 2019 at 21:27