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.

We can tinker in the same way with the rules in both the classical and the intuitionist case to allow for empty domains (this is particularly neatly done in the case of 'tree' systems).

The intuitionist and classic cases are, in this respect, quite parallel.

It is a further question whether the intuitionist has a special reason, over and above those available to the classical logician, to drop the standard assumption of non-empty domains. The classicist, after all, could also argue that the presumption that there are some objects to quantify over (in a given case) is not in general a _logical_ assumption.