Does $A \lor \neg A$ assert decidability in intuitionistic logic?

Question

I'm new to intuitionistic logic, so forgive my silly question.

In intuitionistic logic, does $A \lor \neg A$ assert the decidability of $A$? For example, let's say I don't personally have a proof of $A$, but I know someone who has either a proof or a refutation of $A$, but I don't know which one. Can I say in that case that $A \lor \neg A$ is true?

Answer 1

No, you can't. The intuitionstic meaning of $A \lor \lnot A$ is that you have a proof of $A$, or a proof of $\lnot A$. If you had the proof, you could look at it and decide whether it proves $A$ or whether it proves $\lnot A$. So, if you don't know which option holds, you must not have a proof, and so you can't assert $A \lor \lnot A$.

In general, one way to learn about intuitionistic logic is to look into the BHK interpretation, which gives a (recursive) intuitionistic reading of what it means to prove a formula with any given main connective. The goal here is not to be completely formal (although it can be made formal) - we just want to convey the sense of what a connective means by espressing how to work with the connective in an intuitionistic proof.

• A proof of $A \lor B$ is a proof of $A$ or a proof of $B$
• A proof of $A \to B$ is a procedure that, given a proof of $A$, produces a proof of $B$
• A proof of $A \land B$ consists of a proof of $A$ and a proof of $B$ (an ordered pair of proofs)
• A proof of $\lnot A$ is a procedure that, given a proof of $A$, produces a proof of a contradiction
• A proof of $(\exists x \in S)P(x)$ is a pair $(a,b)$ where $a$ is an object (or a name for an object) and $b$ is a proof that $a \in S$ and $P(a)$ holds
• A proof of $(\forall x \in S)P(x)$ is a procedure that, given an object $a \in S$ (or a name for such an object), produces a proof that $P(a)$ holds.

Answer 2

In model theoretic view we say we know $A\vee B$ for some sentence $A \vee B$ if we know $A$ or we know $B$, therefore if you want to prove $A \vee \neg A$ for some sentence $A$ then you should prove $A$ or prove $\neg A$ and this leads to decidability of $A$.