Law of excluded middle (Realist vs Intuitionistic mathematics) clarification question

Question

I'm currently reading Thinking about Mathematics by Stewart Shapiro. In chapter 1, it says:

"For an intuitionist, (statement 1) The content of a proposition stating that not all natural numbers have certain property P is that it is refutable that one can construct a number x and show that P does not hold of x. (statement 2) The content of proposition that there is a number that lacks P is that one can construct a number x and show that P does not hold of x.

Intuitionist agree that the latter proposition entails the former, but they balk at the converse because it is possible to show that a property cannot hold universally without constructing a number for which it fails."

I don't understand what he is trying to say here in the last paragraph. So intuitionists agree that statement 2 is the consequence of statement 1 but dont agree that statement 1 is a consequence of statement 2?

Can someone please provide clarity on Shapiro's last paragraph, please!

Answer 1

Let $\phi := \neg \forall x : P(x)$ and $\psi := \exists x : \neg P(x)$. Then (I think) what he says is:

$$\psi \Rightarrow \phi$$

but generally one cannot prove:

$$\phi \Rightarrow \psi$$

because (intuitively) merely knowing, that not all $x$ satisfy $P(x)$ is simply not enough to actually exhibit an $x$ such that $P(x)$.

Related: Do De Morgan's laws hold in propositional intuitionistic logic?

Answer 2

Shapiro's statement [page 9] is about the different intuitionistic meaning of $\exists x \ \lnot P(x)$ and $\lnot \forall x \ P(x)$ :

The content of a proposition that there is a number that lacks $P$ is that ...Intuistionists agree that $\exists x \ \lnot P(x)$ entails $\lnot \forall x \ P(x)$, but they balk at the converse...

The intuitionistic "reading" of $\exists x \ \lnot P(x)$ is:

we have a "construction" (a method, procedure) to find a "witness" $c$ such that $\lnot P(c)$ holds (see Brouwer–Heyting–Kolmogorov interpretation).

The intuitionsitic "reading" of $\lnot \forall x \ P(x)$ is [recall that $\lnot P$ is defined as: $P \to \bot$]:

we have a method that, given a proof of $\forall x \ P(x)$, produces a proof of $\bot$.

But $\bot$ is unprovable, and thus we conclude with the "absurdity" of $\forall x \ P(x)$.

But to know that $\forall x \ P(x)$ is "absurd" does not give us any clue about the witnesses of $\lnot P(x)$, and thus the proof of $\lnot \forall x \ P(x)$ does not licenses us to assert that we have proved $\exists x \ \lnot P(x)$.

Thus, we cannot conclude (intuitionistically) that the two are equivalent.

---

Of course, the other "direction" holds also intutitionistically: if we have a method to construct a witness $c$ for $\exists x \ \lnot P(x)$, we are clearly entitled to assert that $\lnot \forall x \ P(x)$ holds.

To show it, it is enough to assume $\forall x \ P(x)$ and instantiate it with the above witness $c$ to get $P(c)$.

Now we have the contradiction: $P(c) \land \lnot P(c)$, i.e. $\bot$, and thus we have proved $\lnot \forall x \ P(x)$.