# Model theory for intuitionistic predicate logic: a non-empty domain?

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?

-

The quantifier rules for standard intuitionist logic are the same as for standard classical logic, and the inference $\forall xFx \vdash \exists xFx$ (which presupposes a non-empty domain) is valid in both standard systems.