Is there a version of the Löwenheim-Skolem theorem in intuitionistic logic?  I'm particularly interested in the "downward" form.  The standard proof I know uses the Tarski-Vaught test for elementary substructures, which in turn relies on the fact that "forall" is equivalent to "not exists not", and that fails intuitionistically.