Henkin-style completeness proofs are founded on a few basic presuppositions, such as the assumptions that the language of a logical theory must be enumerable (or at least that the axiom of choice holds), and that it must contain a (not necessarily primitive) logical connective for negation.

One could fairly describe its general method as follows:

  1. By (reverse) contraposition, assume that $\Gamma \nvdash p$;
  2. Show that $\Gamma \cup \{\neg p\}$ is consistent;
  3. Extend $\Gamma \cup \{\neg p\}$ to a maximal consistent set $\Delta$ as follows: \begin{align} \Delta_0 :=& \Gamma \cup \{\neg p\} \\ \Delta_{n+1} :=& \begin{cases} \Delta_n \cup \{\varphi_{n+1}\} & \text{if } \Delta_n \cup \{\varphi_{n+1}\} \text{ is consistent} \\ \Delta_n \cup \{\neg \varphi_{n+1}\} & \text{otherwise} \end{cases} \\ \Delta :=& \bigcup_{n \in \mathbb{N}} \Delta_{n}. \end{align}
  4. Prove that $\Delta$ is consistent, maximal and that $\Gamma \cup \{\neg p\} \subseteq \Delta$;
  5. Construct a model $\mathcal{M}$ s.t. $\left[\!\!\left[ \varphi \right]\!\!\right]_\mathcal{M}=1$ iff $\varphi \in \Delta$;
  6. Derive a contradiction by showing that $\left[\!\!\left[ \Gamma \right]\!\!\right]_\mathcal{M}=1$ but $\left[\!\!\left[ p \right]\!\!\right]_\mathcal{M}=0$.

However, a moment's reflection shows that the inference from (1) to (2) fails for constructive logics, or, more precisely, logics without the inference rule of double negation elimination. In such logics, a context that does not prove $p$ may prove $\neg\neg p$ (thus being consistent with $p$). Constructively, we can only obtain a weakened form of (1)$-$(2), that is, $$ \Gamma \nvdash \neg \neg p \quad \Longrightarrow \quad \Gamma, \neg p \nvdash \bot.$$ This reveals that, as they are commonly formulated, Henkin-style proofs can only be obtained for logical theories that allow for classical (as opposed to constructive) reasoning. In other words, the logic must be able to prove the law of the excluded middle, double negation elimination etc.

I wonder if a slight modified form of Henkin-style completeness proof is still possible for intuitionistic logic? Is there any reference on the subject? It is known to be complete with respect to topological models, Kripke semantics, and Heyting algebras. Are the proofs given using another method?

  • 3
    $\begingroup$ Completeness in this case is: if $p$ is valid in every model then it is provable. Henkin-style poof of completeness takes the contra-positive form: assume that $p$ is not provable and construct a model in which $p$ is not valid. Thus even if you could overcome the problem you are describing, you still would not get completeness, but rather its contrapositive form. Nevertheless, completeness of intuitionistic propositional calculus is of course established (for the cases you mention). The method is different. $\endgroup$ Jan 6, 2019 at 0:17

2 Answers 2


What you are looking for is a proof of completeness for intuitionistic logic in a constructive metatheory. When one turns constructive, even the notion of completeness varies according to how it is formulated. For example, saying that a valid sentence is provable is not equivalent anymore to saying that a consistent theory has a model.

By arguments of Gödel and Kreisel, a constructive proof of (first-order) intuitionistic completeness without further modifications is not possible since such a completeness result would entail non constructive principles. However, Veldman (1976) found a workaround to this, by introducing Kripke models with so called exploding nodes, which are nodes which are allowed to force $\bot$. Classically, one could always discard the exploding nodes without changing the forcing at the other nodes, but constructively, the change is crucial: the fact that a node is exploding or not might not be decidable. Veldman sacrificed the decidability of a node being exploding in favour of a constructive proof of completeness for intuitionistic logic with respect to the semantics of these modified Kripke models. The result is described in "An Intuitionistic Completeness Theorem for Intuitionistic Predicate Logic" (The Journal of Symbolic Logic, Vol. 41, No. 1, 1976, pp. 159-166).

Subsequently other proofs were found, for example one by Harrie de Swart: "Another intuitionistic completeness proof" (The Journal of Symbolic Logic Vol. 41, No. 3 1976, pp. 644-662). There is also a categorical treatment of such constructive completeness theorems in a joint paper of mine with Henrik Forssell: "Constructive completeness and non-discrete languages" (https://arxiv.org/abs/1709.05817), in which we also see what happens if one considers languages of arbitrary size and languages for which equality between the elements of the signature is not decidable. It is also established that the use of the FAN theorem (compactness of the Cantor space) in these constructive completeness results is unavoidable. The proof here is in essence a Henkin-style argument of building models out of constants (which is at the heart of Joyal's completeness theorem), and which avoids the non-constructive detours of the usual first-order version of the proof you sketched.

  • $\begingroup$ In Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (archive.org/details/constructivismin0002troe/page/718/mode/2up) completeness of intuitionistic predicate calculus is proven in an intuitionistic meta-theory using heyting algebra semantics. Can you assist me in reconciling this result in light of arguements by Gödel and Kreisel. Thanks! $\endgroup$
    – ToucanIan
    Sep 30, 2021 at 15:42
  • 1
    $\begingroup$ @ToucanIan The semantics are different. The results of Gödel and Kreisel apply to Tarski/Kripke semantics, not Heyting algebra semantics. $\endgroup$
    – godelian
    Sep 30, 2021 at 15:45
  • $\begingroup$ Can you give more detail on how the semantics differ? Other than just the definitions, etc. I have asked a question regarding this here: mathoverflow.net/questions/405055/…. It was suggested that maybe Heyting Algebra Semantics have less entailments. $\endgroup$
    – ToucanIan
    Sep 30, 2021 at 15:56
  • 1
    $\begingroup$ @ToucanIan The point is that in the Heyting algebra semantics the notion of provability is built-in in the Lindembaum-Tarski construction, so the connection to provability can be made constructively. For Tarski/Kripke semantics the connection is more remote and will involve non-constructive principles. $\endgroup$
    – godelian
    Sep 30, 2021 at 16:24

Henkin-style completeness proofs for intuitionistic logic are perfectly possible: instead of maximal consistent sets, you consider, for each formula $A$, maximal sets $\Gamma$ such that $\Gamma\nvdash A$; the collection of all such sets (for all $A$ together) will form a Kripke model, where the sets are ordered by inclusion ($A$ is ignored for the ordering). In this model, each point $\Gamma$ will satisfy all formulas from $\Gamma$, and it will not satisfy the formula $A$ with respect to which $\Gamma$ was maximal.

Completeness with respect to Heyting algebras is even more trivial: just as in any other algebraizable logic, you just construct the Lindenbaum–Tarski algebra. That is, for a fixed $\Gamma$, you take the algebra of formulas with operations given by the connectives, preordered by $$A\le B\iff\Gamma\vdash A\to B,$$ and then its quotient by the kernel equivalence relation $A\le B\land B\le A$ is a Heyting algebra in which the canonical assignment gives $\Gamma$ value $1$, and all $A$ unprovable from $\Gamma$ a smaller value.

There are some more issues with predicate logic, but I’m assuming from the question that you mean propositional logic.

  • $\begingroup$ What are the issues in the context of predicate logic? $\endgroup$ Mar 21, 2019 at 19:36
  • 1
    $\begingroup$ For one thing, you need all existentially quantified sentences in the sets to be witnessed by Henkin constants. This means you cannot just take maximal sets by appealing to Zorn’n lemma, you actually need to carry out an inductive completion procedure. Another nasty thing is to handle the selection of new constants properly: you need sets higher up to be able to use more constants, so that the domains have more elements, but if you want to define the whole Kripke model at once as in the propositional case, you need all the constants to be drawn from the same pool so that the model is a set. $\endgroup$ Mar 22, 2019 at 10:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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