As part of preparing for a test, I wanted to go through how to tell if a inference is valid/not valid by intuitionistical logic. Given the following inference:
$$ \begin{array}{c} \forall x Fx \to \exists x Gx \\ \hline \exists x (Fx \to Gx) \end{array}$$
This inference is valid by classic logic, but I fail to see where this inference fails intuitionistically. Perhaps that for the conclusion that we would need a proof for some numeral $n$ that $Fn$ leads to $(Fx => Gx)$. But the premise doesn't give us such material?
Thanks for reading and helping!
This is closely related of the principle known as independence of premise. The Wikipedia article gives two heuristic arguments why that principle is not constructively valid. I will sketch them here, in the context of this principle, which is very close but not quite the same.
The first argument is based on the BHK interpretation. To prove the bottom formula, you would need to provide a specific $x$ so that, if $Fx$ holds then $Gx$ holds. To prove the top formula, you only need to provide a method that, given a proof of $\forall x Fx$, produces a proof of $\exists x Gx$. There is no obvious way to take a method of that kind and use it to produce a specific value of $x$, which makes us suspicious of the constructive validity of the deduction.
The second argument is based on a weak counterexample. Let $Gx$ be such that we do not know whether there is any $x_0$ such that $Gx_0$. For example, $G$ could say that $x$ is a counterexample to Goldbach's conjecture. Let $Fx$ be the formula $\exists z Gz$, so $\forall x Fx$ is $\forall x \exists z Gz$. Then the implication $\forall x \exists z Gz \to \exists x Gx$ is trivial to prove constructively, but $\exists x ( \exists z Gz \to Gx)$ cannot be proved constructively unless we can produce an $x$ such that, if there is any counterexample to Goldbach's conjecture then $x$ is such a counterexample. No such value of $x$ is known at the present time.
This weak counterexample can be used to prove more formally that the deduction from the question is not provable in various formal systems of constructive logic. The counterexample shows that, if we work in the language of arithmetic, and we assume the deduction rule from the question, then whenever $Hx$ is a decidable property of natural numbers we would have a way to determine whether $\exists x Hx$ is true. This would contradict the unsolvability of the Halting problem, among other things.