 Intuitionistic logic,  too, has a Kripke semantics, though special valuation clauses are needed for ‘\({\sim}\)’, ‘\(\rightarrow\)’ and ‘\(\forall\)’ in order to accommodate the special meanings these operators have for intuitionists, and ‘\(\Box\)’ is generally not used. The usual first-order intuitionistic logic, the Heyting predicate calculus (HPC)—also called the intuitionistic predicate calculus—has the theorem \(\exists x(x=t)\) and hence is not free. But intuitionists admit the existence only of objects that can in some sense be constructed, while classical mathematicians posit a wider range of objects. Therefore users of HPC cannot legitimately name all the objects that classical mathematicians can. Worse, they cannot legitimately name objects whose constructibility has yet to be determined. Yet some Kripke-style semantics for HPC do allow use of names for such objects (semantically, names of objects that “exist” at worlds accessible from the actual world but not at the actual world itself). Some such semantics, though intended for HPC, have turned out, unexpectedly, not to be adequate for HPC. An obvious fix, advocated by Posy (1982), is to adopt a free intuitionistic logic. For more on this issue, see Nolt 2007.