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, 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?

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?