Completeness theorem for intuitionistic logic

Question

Reading from Wikipedia about intuitionistic logic, I am guessing that there is a formal proof system for intuitionistic logic. (Note: My knowledge of intuitionistic logic is almost nil). My understanding of Godel's completeness theorem is that one designs the class of sets in a way (by adding the axiom of choice) to make sure that every consistent theory has a model.

Question: Is there a completeness theorem for intuitionistic logic ?

My guess is that there must not be a constructive way of finding models for theories that are consistent in intuitionistic logic. Hence, I am guessing that there is no intuitionsitc proof in the maeta language that the formal intuitionistic proof system is complete. What I am asking for is a formalist meta proof (i.e. possibly non-constructive) that the formal intuitionistic proof system is complete. Perhaps one would impose/relax new constraints on the world of sets (just like relaxation of allowing choice that I mentioned earlier) to make sure that theories are intuitionistically consistent iff they have a model (by possibly redefining models in a natural way). Is there any work in this direction ?

I hope my question is not vague for you.

Thank you.

Answer 1

In order to speak of completeness, you must first decide what family of "models" are considered, i.e., what the semantics are. In the case of classical predicate calculus, models are simply a structure with relations for the various relations in the language, and satisfaction is defined in the obvious way. In the case of intuitionist predicate calculus, since we're working in a classical ambient world, we can't just do that (for example, we don't want to impose $\forall x.(x=x \lor \neg x=x)$). There are several different semantics (i.e., definitions of what a "model" is) that are complete, but you have to choose one for your question to make sense: essentially, Heyting-valued models or Kripke semantics.

A Heyting-valued model (or rather: structure) consists of a set $M$ (the domain) and a Heyting algebra $H$ of "truth values" together with, for every $n$-ary relation $R$ in the language including equality, a map $R\colon M^n \to H$ which gives the "truth value" of $R$. If you don't know what a Heyting algebra is, you can take it to be the set of open sets of a topological space (ordered by inclusion): define $U\land V$ and $U\lor V$ to be $U\cap V$ and $U\cup V$ respectively, and $U\Rightarrow V$ to be the largest open set $W$ such that $U\cap W \subseteq V$ (this exists). If we further interpret $\exists x.(U(x))$ to be $\bigcup_x U_x$ and $\forall x.(U(x))$ as the largest open set contained in (=interior of) $\bigcap_x U_x$, then, using the relations in the model for elementary formulæ, we can give a truth value (an open set, or element of $H$) to every formula of predicate calculus with variables from $M$. Then we can say that $M$ is a model for a theory $T$ in intuitionistic predicate calculus (containing the axioms of equality) when the truth value of every axiom of $T$ is $\top$ (the largest element of $H$, or the full open set). This defines a semantic, and, yes, it is complete: any consistent theory has a model. See here for example.