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.