I need help to show that such prime theory exists In this question $\vdash$ stands for the consequence relation in the intuitionistic propositional Hilbert-calculus.
A set of formulas $T$ is a theory if it's closed in relation with $\vdash$, that is, if for every formula $\varphi$ such that $T \vdash \varphi$, it follows that $\varphi \in T.$ It is easily seen that intersection of theories is again a theory.
A theory $T$ is called a prime theory if $\varphi \vee \psi \in T \implies \varphi \in T\,\,\,\text{or}\,\,\, \psi \in T$. Then we have the following results:
Theorem: For every set of formulas $\Gamma$ and every formula $\varphi$, if $\Gamma \not \vdash \varphi$ then there is a prime theory $T$ such that $\Gamma \subseteq T$ and $\varphi \not \in T$.
Corollary: $\Gamma \vdash \varphi$ iff $\varphi$ belongs to every prime theory $T$ such that $\Gamma \subseteq T.$
Question that I need to solve: Show that for every theory $T$ and every non-empty set of formulas $\Delta$ closed under $\vee$ such that $T \cap \Delta= \emptyset$, there is a prime theory $T'$ that includes $T$ and is also disjoint from $\Delta$.
My attempt: Since $\Delta$ is countable, we can write that set as $\Delta=\{\delta_1,\dots,\delta_n,\dots\}$. For each $n \in \mathbb{N}$ it's true that $\delta_1 \vee\,\dots\vee \delta_n \in \Delta$ and noticing that $T \not \vdash \delta_1 \vee\,\dots\vee \delta_n$, it follows by the Theorem that there exists a prime theory $T_{\delta_1 \vee\,\dots\vee \delta_n}$ such that $T \subseteq T_{\delta_1 \vee\,\dots\vee \delta_n}$ and $\delta_1 \vee\,\dots\vee \delta_n \not \in T_{\delta_1 \vee\,\dots\vee \delta_n}.$ Now define:
$$ T'=\bigcap_{n=1}^{\infty} T_{\delta_1 \vee\,\dots\vee \delta_n}.$$
$T$ is obviously a subset of $T'$, a theory and $\Delta \cap T'=\emptyset.$ The only problem is: how to prove that $T'$ is prime?
I'm open to new approachs to solve the problem too.
I thank in advance every help!
 A: Your proof can be fixed! Let $\mathcal U$ be a non-principal ultrafilter on $\mathbb N,$ and define $T’$ to be the set of $\phi$ such that $\{n:\phi\in T_{\delta_1\vee\dots\vee\delta_n}\}\in\mathcal U.$ Then $T’$ is a prime theory including $T$ and disjoint from $\Delta.$
There is a serious point here: the result you want follows from the Theorem by compactness. This is an important technique and you will often see authors simply say that a result like yours follows “by compactness” or “by a standard compactness argument”.
At the risk of making it look complicated, here are some more details. Create a classical propositional variable $X_\phi$ for each sentence $\phi$ of intuitionistic propositional logic. Let $T_b$ be the following collection of axioms in classical propositional logic.

*

*“$X_{\phi_1}\wedge \dots \wedge X_{\phi_n}\implies X_{\psi}$” whenever $\phi_1,\dots,\phi_n\vdash \psi$

*“$X_{\phi\vee \psi}\implies (X_\phi\vee X_\psi)$” for all $\phi,\psi$

*“$X_\phi$” for all $\phi\in T$

*“$\neg X_\phi$” for all $\phi\in\Delta$
Any finite set $F\subset T_b$ is consistent. Indeed, by the Theorem there is a prime theory $T'$ extending $T$ and avoiding the disjunction of the sentences of $\Delta$ mentioned in $F.$ The classical propositional theory $\{X_\phi:\phi\in T'\}\cup\{\neg X_\phi:\phi\not\in T'\}$ is then a complete extension of $F,$ demonstrating consistency. By the compactness theorem for classical propositional logic (for countable languages), there is a complete theory $T’_b$ extending $T_b.$ Taking $T’=\{\phi:X_\phi\in T’_b\}$ gives a prime theory including $T$ and disjoint from $\Delta.$
A: Your current method won't work, because intersection of prime theories in general is not prime. What you want is essentially to reprove your first theorem, but using a different application of Zorn's lemma. First, I'll write down the proof for this particular problem at hand; but note that as I'll comment below, this is just a restatement and special case of the Boolean prime filter theorem for the countably generated Heyting algebra.

First, let us close $\Delta$ downwards: let $\psi\in \Delta'$ iff there is $\phi\in \Delta$, such that $\psi\vdash \phi$. Note that since $T$ is a theory, $T\cap \Delta'=\emptyset$ again.
Now, consider:
$$P := \{T' : T' \text{ is a theory and } T'\cap \Delta' =\emptyset\}$$
It is straightforward to check that if you have a chain of elements of $P$ ordered by inclusion, their union will again be a theory distjoint from $\Delta$. So by Zorn's lemma, this has a maximal element, call it $T^{*}$. Then you want to check that $T^{*}$ is a prime theory. Suppose that $\phi\vee\psi\in T^{*}$ but neither $\phi$ nor $\psi$ are in $T^{*}$. Then $T^{*}\nvdash \phi$ and $T^{*}\nvdash \psi$. Then consider:
$$F_{\phi} := D(\{\phi\wedge \chi : \chi \in T^{*}\})$$
Where $D$ denotes the operator which takes the smallest theory containing all the formulas. This is indeed a theory extending $T^{*}$, so $F_{\phi}\cap \Delta'\neq \emptyset$. Let $\psi'\in F_{\phi}\cap\Delta'$. We have that $\phi\wedge\chi\vdash \psi'$ for some $\chi\in T^{*}$. Then $\phi\wedge\chi\in \Delta'$, because we closed it downwards. Analogously, $\psi\wedge \chi'\in \Delta'$ for some $\chi'\in T^{*}$. But then, note that:
\begin{align*}
\phi\wedge\chi \wedge \chi' \vdash \phi \wedge \chi \text{ and } \psi\wedge\chi \wedge \chi' \vdash \psi \wedge \chi'
\end{align*}
So this implies:
$$(\phi \vee \psi)\wedge (\chi'\wedge \chi) \in T' \text{ and } (\phi \vee \psi)\wedge (\chi'\wedge \chi) = (\phi\wedge \chi'\wedge \chi) \vee (\psi \wedge \chi'\wedge \chi) \in \Delta'$$
These statements follows from distributivity, the definition of $T'$ and $\Delta'$, and the fact that $Delta'$ is closed under joins. It is also a contradiction, which was to show.

In case this might also be useful - since writing this proof is quite clunky relative to the context in which it would naturally appear - note that in an abstract sense, what you're asking for is essentially just the strong form of the Boolean Prime Filter Theorem, in a given special Heyting Algebra - namely the Free Heyting Algebra on countably many generators. The generators are propositional variables, and the elements of this Heyting algebra are formulas.
In such a Heyting algebra, your theories are precisely filters (in the usual lattice theoretic sense). You can prove this directly, which given you are working with a Hilbert Calculus might be a bit morose, though doable. If you can afford to jump to an algebraic setting (using the completeness of IPC with respect to the Hilbert calculus, and then the algebraic completeness of IPC with respect to the variety of Heyting algebras, and the fact that $HA=\textbf{HSP}(\textbf{F}(\aleph_{0}))$), and for that you only need to note that implication and the usual order relation in Heyting algebras are very closely related, namely:
$$a\rightarrow b = 1 \iff a\leq b$$
If you establish that connection, then it is quite easy to see that prime theories are just prime filters over this Heyting algebra. Likewise, subsets closed under join can be extended to ideals by taking their downwards closure. Then the usual prime ideal theorem will be precisely the statement you want.
A: Assume $\phi\lor\psi \in T$, but neither $\phi\in T$ nor $\psi\in T$. Then for some $n$, $\phi\notin T_{\delta_1\lor\cdots\lor\delta_n}$ and for some $m$, $\psi\notin T_{\delta_1\lor\cdots\lor\delta_m}$. Conclude $\phi,\psi$ are both $\notin  T_{\delta_1\lor\cdots\lor\delta_{\max\{n,m\}}}$.
