In classical logic we tend to make the assumption that the domain of quantification is non-empty. This isn't (too) problematic because classical mathematicians assume a language/mind/proof independent existence of mathematical objects.
My question is this:
Does the model theory for intuitionistic logic make a similar assumption of a non-empty domain?
Since Intuitionists view mathematical statements as having no truth value until proven, we can say that mathematical statements are indexed with a time, $t_0 \dots t_n$.
If we take $t_0$ to be the starting point at which no proofs have been given, my question is must the domain at $t_0$ be taken to be non-empty, even though no mathematical objects have been constructed at that point?