Warning: I am neither a logician nor a set theorist, just curious about foundations of classical and intuitionistic mathematics. Therefore it might well be that the things to come are plain wrong, and I'd be happy about any clarification of the things I might have misunderstood.
First of all, I understand Goedel's completeness theorem as follows: Within a classical foundation of mathematics like ZFC + classical FOL, a formula in any first order theory is proveable in classical FOL if and only if it is true within every model of the theory.
I am wondering if there are completeness theorems for intuitionistic first order theories as well?
Depending on whether the ambient foundation is classical or intuitionistic, this seems to split in two separate questions:
- Within a classical foundation like ZFC + classical FOL: Given a formula in some first order theory, what is the model-theoretic equivalent of the formula being proveable with respect to intuitionistic FOL? A naive guess would be that it is provable in IFOL if and only if it is true in any model in any elementary topos - is this true?
Edit: For this question, Peter has already given very nice references below.
- Within an intuitionistic ambient foundation like Martin-Loef type theory, one could look at Goedel's statement verbatimly. Proving its validity would then mean to give an algorithm constructing a derivation of a given formula in IFOL from given witnesses for its truth in any model.
I'd be happy about whatever you have to say or correct!