Incompleteness in intuitionistic metamathematics.
David Charles McCarty · Notre Dame Journal of Formal Logic · 1991
There are three main results; all are contributions to the intuitionistic metatheory of intuitionistic systems.First, pure intuitionistic predicate logic is provably incomplete with respect to ordinary model-theoretic semantics, provided that the metatheory is suitably intuitionistic.With the same proviso, intuitionistic propositional logic is also incomplete; in fact, the concept of validity for formulas in one propositional variable is not arithmetically definable.Also, one cannot prove-in standard intuitionistic metatheories-an existence theorem for countable models, even when the relevant theory is that of subfinite sets in the language of pure identity.