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.