In classical logic we tend to make the assumption 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 is question is, 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_o \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?