4
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.
$\endgroup$
  • $\begingroup$ Thank you for the answer and for the pointer to the BHK interpretation! $\endgroup$ – Dan Oneață Nov 23 '15 at 20:41
2
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.