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

Question

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?

Answer 1

$\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.

I'm not sure what to say about, 'truth values,' because that's a fairly complicated subject (and I don't think about it often enough to just rattle off an answer). I would probably say that you can only talk about them sensibly relative to a model, and they're generally more complicated for constructive logics than classical ones. Also, if you think there is a 'real' truth value for every sentence in every classical logic, I think you're wrong. :)