Thank you for your reply. How exactly would you prove that P cannot be neither true nor false without using the law of excluded middle?

@Mark Saving: is constructive logic modeled by some kind of lattice that relaxes the properties of a Boolean algebra? If so, what kind of lattice?

@user953376 Check Heyting algebras

@user953376 Just as amrsa says, Heyting algebras model constructive logic. Constructive propositional logic is complete over Heyting algebras just as classical propositional logic is complete over Boolean algebras. All Boolean algebras are also Heyting algebras.

@MohamedShereef If $P$ is not true, then that is equivalent to saying $\neg P$. Thus, $P$ must be false in that case, by the argument I made above. So it can't be the case that $P$ is not true and also not false, since if $P$ were not true, it must be false.

@MarkSaving but doesn’t that mean that we can prove that the intuitionist logic is wrong without using the law of excluded middle?

@MohamedShereef Intuitionist logic doesn't state that LEM is wrong; it simply doesn't affirm LEM. So intuitionist logic isn't "wrong" just because LEM is right. What exactly do you mean by intuitionist logic being "wrong"? If you mean that LEM can in fact be proved from intuitionist logic, you are incorrect, but it might be instructive to see what your thoughts are and point out where you go wrong.

@MarkSaving I did not realize that intuitionist logic doesn’t state that LEM is wrong that is why I said that. But why do you say that LEM can’t be proven from intuitionist logic, isn’t that what you did in your answer above.

@MohamedShereef I proved $\neg (P \land \neg P)$. This is not necessarily equivalent to $P \lor \neg P$ if you have intuitionist logic. The expression $\neg (P \land \neg P)$ is equivalent to $\neg \neg (P \lor \neg P)$. But because we don't have double-negation elimination, we cannot say this is equivalent to $P \lor \neg P$.

+1: nice answer, but I don't see what you mean by the penultimate paragraph. In the usual algebraic semantics for IL using Heyting algebras, there are typically lots of "middle values".

@RobArthan And in the usual semantics for classical logic using Boolean algebras, there are also lots of "middle values" in most cases. There's a difference between what holds externally about a model and what holds internally.

That wasn't quite my point. Let me put it more directly: what do you mean by "we can still prove that $P$ cannot be neither true nor false"? What statement of IL denotes that? The double negation of LEM?

@RobArthan Formally, the statement $\neg (\neg P \land \neg (\neg P))$ is the statement "it is not the case that both $P$ is false and also $\neg P$ is false". This is a tautology in intuitionist logic.

I think that part of your answer would be much clearer if you gave that formal statement. Note that by applying one negation, you have mapped into the world where intuitionistic and classical logic agree.

@RobArthan Thanks for that edit suggestion. I have followed through on it.

I thought proof by contrapositive was constructively valid; just proof by contradiction isn't.

@AsafKaragila The contrapositive principle is equivalent to the law of excluded middle.

@AsafKaragila Proof by contrapositive is $(\neg P \implies \neg Q) \implies (Q \implies P)$. If you substitute $\top$ for $Q$, this gives you $(P \implies \neg \top) \implies (\top \implies P)$. Noting that $\top \implies P$ is equivalent to $P$, and noting that $\neg \top$ is equivalent to $\bot$, means that $(P \implies \neg \top) \implies (\top \implies P)$ is equivalent to $(\neg P \implies \bot) \implies P$, which is exactly proof by contradiction. So accepting the proof-by-contrapositive principle requires us to accept proof by contradiction. Thus, constructive logic doesn't allow it.

@The_Sympathizer It would mean relaxing the law of noncontradiction. In my view, I would say a logic permits a "third truth value" if the statement $\neg A \land \neg \neg A$ is consistent with the logic. This would be a logic with radically different rules than any sort of ordinary logic.

@Mark Saving: So what happens when we consider simple "three valued logics" like mentioned here?: en.wikipedia.org/wiki/Three-valued_logic#Logics One might at first think these work okay because they do not validate the principle of contradiction - for example in the simple Kleene logic $\neg (A \wedge \neg A)$ can be "unknown" (U), not necessarily "true" (T). But on the other hand, it seems $\neg A \wedge \neg \neg A$ is never true - it is at most "unknown" (U). So does this mean the "U" value here is not a "real" truth value and so in a sense it fails to achieve its mission?