Goedel's completeness theorem in and/or for intuitionistic first order logic

Question

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:

1. 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!

Thank you!

Answer 1

Intuitionistic logic has a variety of different notions of model.

Realizability provides a notion of model that satisfies a "soundness theorem," but does not satisfy any "completeness theorem" (at least in the way it is usually presented).

Kripke models are both sound and complete with respect to intuitionistic logic, but the completeness theorem is not constructively valid. (So for Kripke models the answer to your second question is "false").

Beth models are both sound and complete and both of these can be proved constructively. The same is true for sheaf models. (So for Beth models and sheaf models the answer to your second question is "true").

For a constructive completeness theorem for sheaf models see Palmgren, Constructive Sheaf Semantics. This is basically the same procedure as for toposes, except that he ensures that all the proofs can be carried out predicatively (which would be necessary in order to formalize them in the usual forms of Martin-Löf type theory, say). In fact he shows that for every theory $\Sigma$ over a language $L$, there is one "generic" sheaf model $\mathcal{M}(\Sigma, L)$ such that for any formula $\phi$, $\phi$ is provable if and only if it holds in $\mathcal{M}(\Sigma, L)$. In particular it does indeed give a way to construct a proof of $\phi$ from a (meta) proof that $\phi$ holds in every sheaf model.

Answer 2

I'm not sure from the way the question is posed what you already know. But just in case it is news ....

There's a completeness proof of first-order intuitionistic logic with respect to the now standard Kripke semantics. You will find an outline and a lot of references at http://plato.stanford.edu/archives/spr2004/entries/logic-intuitionistic/#5.1

For something on the connection between topos theory and Kripke semantics (often called Kripke-Joyal semantics by category theorists), you could look e.g. at some lectures by Olivia Caramello http://www.oliviacaramello.com/teaching/cambridgetopostheorycourselectures17to20.pdf

Answer 3

Constable and Bickford, Intuitionistic Completeness of First-Order Logic

http://arxiv.org/abs/1110.1614

Quoting the abstract:

We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL and mFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform minimal evidence into a formal first-order proof. We have implemented Prf. Uniform validity is defined using the intersection operator as a universal quantifier over the domain of discourse and atomic predicates. Formulas of iFOL that are uniformly valid are also intuitionistically valid, but not conversely. Our strongest result requires the Fan Theorem; it can also be proved classically by showing that Prf terminates using Konig's Theorem. The fundamental idea behind our completeness theorem is that a single evidence term evd witnesses the uniform validity of a minimal logic formula F. Finding even one uniform realizer guarantees intuitionistic validity because Prf(F, evd) builds a first-order proof of F, establishing its intuitionistic validity and providing a purely logical normalized realizer. We establish completeness for iFOL as follows. Friedman showed that iFOL can be embedded in minimal logic (mFOL) by his A-transformation, mapping formula F to FA. If F is uniformly valid, then so is FA, and by our completeness theorem, we can find a proof of FA in minimal logic. Then we intuitionistically prove F from FFalse, i.e. by taking False for A and for \bot of mFOL. Our result resolves an open question posed by Beth in 1947.