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!


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.

| cite | improve this answer | |
  • $\begingroup$ Thank you very much! This seems to be precisely what I was looking for :) Just to make sure I got it right: Completeness is hence also constructively valid for models in topoi, since they subsume the sheaf models? Do you have a reference for the non-existence of a constructive proof of completeness for Kripke semantics? $\endgroup$ – Hanno May 21 '14 at 5:56
  • $\begingroup$ The thing about toposes is that certain basic propositions, like "sheaf toposes are toposes" require the power set axiom. This turns out to not be a problem when it comes to extracting algorithms, but power set is rejected by many constructivists for being "impredicative". In particular it is not usually part of type theory. $\endgroup$ – aws May 21 '14 at 14:18
  • $\begingroup$ On Kripke models, the usual completeness proofs for example in Troelstra and van Dalen, Constructivism in Mathematics use excluded middle, but I found it hard to find a proof that it is stricly necessary. The SEP page on intuitionistic logic mentions that Kreisel showed that it requires Markov's Principle. This is actually not so bad constructively speaking, but it could cause a problem when it comes to extracting an algorithm. $\endgroup$ – aws May 21 '14 at 14:23
  • $\begingroup$ The thing is, that even with a classical proof one can give an algorithm that works but is very inefficient: just run through every potential proof and check them one by one until you find one that works. I think a proof that requires Markov's principle could give a similarly inefficient and impractical algorithm. An algorithm based on sheaf models (which don't, I believe, require Markov's principle) could I think be much more efficient and maybe even work well in practice. I hope that helps. $\endgroup$ – aws May 21 '14 at 14:28
  • $\begingroup$ Also I should point out that there are variants of Kripke models that have constructive completeness proofs (this is mentioned on the same SEP page I linked to above). $\endgroup$ – aws May 21 '14 at 14:30

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

| cite | improve this answer | |
  • $\begingroup$ Thank you very much, Peter, these seem to be very helpful references! So if I understand it correctly, this answers part (1), i.e. it gives a completeness theorem for IFOL in terms of Kripke semantics or Topoi, on the basis of a classical foundation - right? Do you know anything about completeness theorems for classical or intuitionistic logic within an intuitionistic framework? $\endgroup$ – Hanno May 10 '14 at 6:43
  • $\begingroup$ @Hanno: Some things to note. The internal logic of a topos is an intuitionistic set theory. We can reason classically about whether intuitionistic logic can deduce anything. Boolean logic is an intuitionistic logic (intuitionistic logic doesn't assume the denial of excluded middle). Any intuitionistic logic "contains" a classical logic: the law of the excluded middle always works with negated propositions. $\endgroup$ – user14972 May 10 '14 at 12:35
  • $\begingroup$ @Hurkyl: I'm not sure I got precisely what you mean with your first sentence. As far as I understand, a particular topos can only be considered within an already given ambient set theory. Within that set theory, I can consider first order theories and their interpretations within the given topos; the class of statements semantically valid then contains those provable wrt IFOL, but in general not all of those provable wrt classical FOL. However, unless I describe an explicit calculus for this class, I don't know how to externalize it to an ambient logic, having to stick to general IFOL. $\endgroup$ – Hanno May 10 '14 at 12:58
  • $\begingroup$ cont'd: My first question is then whether, when looking at all internal logics of topoi, the intersection of their respective classes of tautologies for a fixed first order theory is indeed what IFOL generates -- and according to Peter's answer, this seems to be true. ... but maybe I just misunderstood you and you wanted to point to something different? $\endgroup$ – Hanno May 10 '14 at 13:07
  • $\begingroup$ @Hurkyl: Concerning your second statement -- couldn't it be that in an intuitionistic framework we can say less about what intuitionistic logic can deduce? E.g. that we really need LEM to establish the completeness of IFOL with respect to interpretations in topoi? $\endgroup$ – Hanno May 10 '14 at 13:10

Constable and Bickford, Intuitionistic Completeness of First-Order Logic


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.