Why this predicate formula is not provable in intuitionistic logic

Question

I'm unable to show the the following is not provable in intuitionistic predicate (first-order) logic:

$$ ∀x ¬¬φ(x) → ¬¬∀x φ(x) $$

(this is not provable according to Wikipedia: https://en.wikipedia.org/wiki/Double-negation_translation#Results)

In particular, I tried to show that there is no proof to this using Gentzen calculus, but got to this proof:

[1] φ(x) → φ(x)

[2] φ(x) → ∀x φ(x)

[3] φ(x),¬∀x φ(x) →

[4] ¬∀x φ(x) → ¬φ(x)

[5] ¬¬φ(x),¬∀x φ(x) →

[6] ∀x ¬¬φ(x),¬∀x φ(x) →

[7] ∀x ¬¬φ(x) → ¬¬∀x φ(x)

Where is my mistake?

Answer 1

Your second step certainly isn't true.

$\varphi(x) \to \forall x\ \varphi(x)$

The predicate rules are the following:

$\varphi(x) \to \exists x\ \varphi(x)$

$\forall x \ \varphi(x) \to \varphi(t)$

where $t$ is a free variable.

---

Note that in intuitionist logic, $p \to \neg\neg p$ but not the converse.