Full Idea
The inference of 'distribution' (∀x)(A v B) |- (∀x)A v (∃x)B) is valid in classical logic but invalid intuitionistically. It is straightforward to construct a 'stage' at which the LHS is true but the RHS is not.
Gist of Idea
(∀x)(A v B) |- (∀x)A v (∃x)B) is valid in classical logic but invalid intuitionistically
Source
JC Beall / G Restall (Logical Pluralism [2006], 6.1.2)
Book Reference
Beall,J/Restall,G: 'Logical Pluralism' [OUP 2006], p.64
A Reaction
This seems to parallel the iterative notion in set theory, that you must construct your hierarchy. All part of the general 'constructivist' approach to things. Is some kind of mad platonism the only alternative?