# Completeness theorem for intuitionistic logic

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.

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.