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.



Intuitionistic Lowenheim-Skolem?
I have a reference that says the downward Löwenheim-Skolem theorem does not occur
in intuitionistic logic. In the words of the abstract "even a very powerful
version of intuitionistic set theory does not yield any of the usual forms of a countable
downward Löwenheim-Skolem theorem."


Charles McCarty & Neil Tennant, *Skolem's paradox and constructivism*.
Journal of Philosophical Logic.
Springer Netherlands.
Issue Volume 16, Number 2 / May, 1987.
<https://doi.org/10.1007/BF00257838>


Also
page 341 of
A Companion to Metaphysics
By Jaegwon Kim


"...there is no intuitionistically acceptable analogue
of the classical downward Löwenheim-Skolem theorem"


