Confusion around quantifiers in intuitionistic logic As laid out in Joel Hamkins' A question for the mathematics oracle, I am interested in considering the possibility that some arithmetic sentences might not satisfy the law of the excluded middle.
Suppose such a sentence is of the form $Q = \forall n P(n)$. I imagine that, for any given value of $n$, I might agree that $P(n) \vee ¬P(n)$ is true, and also that $¬P(n)$ should imply $¬Q$. But that seems like it should not lead me to commit to the statement $Q \vee ¬Q$.
Similarly, suppose the sentence is of the form $Q' = \exists n P'(n)$. Then, for any given value of $n$, I might agree that $P'(n) \vee ¬P'(n)$ is true, and also that $P'(n)$ should imply $Q'$. But that seems like it should not lead me to commit to the statement $Q' \vee ¬Q'$.
I'm not familiar enough with intuitionistic logic to make this reasoning precise. Could anyone please clarify what's going on?
 A: The key to keep in mind is that in intuitionistic logic, and more generally in constructive logic, is that something is true only if you can prove it.
In particular in order to prove a formula of the form $A \lor B$ you have to provide a proof of $A$ or a proof $B$.
With this in mind, your assumption, namely that for each $n$ the formula $P(n) \lor \neg P(n)$ is true, would mean that you have a way, an algorithm if you like, to provide for every $n$ a proof of $P(n)$ or a proof $\neg P(n)$. 
Assuming that this function/algorithm exists does not provide any information on the algorithm, in particular we do not know if this algorithm returns for every $n$ a proof of $P(n)$ or if there is a $n$ for which it returns a proof for $\neg P(n)$.
Not having this information we can neither state if $\forall n P(n)$ or not nor whether $\neg \forall n P(n)$.
Hence we are left in a situation in which we are not able to prove eithr $\forall n P(n)$ or its negation, so we cannot prove $(\forall n P(n))\lor(\neg \forall n P(n))$.
Hope this helps.
