The answer to your question, strictly speaking, is **negative**. For instance take the sequent $P \vee Q \vdash \exists X ((X \wedge P) \vee (\neg X \wedge Q))$, which is (intuitionistically) derivable since both the following are:

- $P \vdash \exists X ((X \wedge P) \vee (\neg X \wedge Q))$ by setting $X = \top$; and,
- $Q \vdash \exists X ((X \wedge P) \vee (\neg X \wedge Q))$ by setting $X = \bot$.

However note that no single formula $\chi$ can witness the existential when the antecedent is $P\vee Q$, regardless of whether it is quantifier-free or not. To see this suppose for contradiction that $P\vee Q \vdash (\chi \wedge P) \vee (\neg \chi \wedge Q)$ is derivable. This implies the derivability of both:

- $P \vdash (\chi \wedge P) \vee (\neg \chi \wedge Q)$; and,
- $Q \vdash (\chi \wedge P) \vee (\neg \chi \wedge Q)$.

By the disjunction property (or simply the only possible rule application in bottom-up cut-free proof search), and since we have neither $P\vdash Q$ nor $Q\vdash P$, we must have derivability of both:

- $P \vdash \chi$; and,
- $Q \vdash \neg \chi$.

However this is not even classsically possible, as one of $\chi$ and $\neg \chi$ is always false, and so contradicts the assignment that sets both $P$ and $Q$ true.

Usually for disjunction and existential properties to hold in the presence of a context $\Gamma$ one requires some further conditions, e.g. that $\Gamma$ consists only of Harrop formulas (this is sufficient but not necessary).

Of course we could reformulate the question to assume that $\Gamma$ is Harrop (or similar), but more generally let us just suppose that $\Gamma \vdash \exists X \psi(X)$ is derivable and has a *second-order witness*, say $\chi$, i.e. that $\Gamma \vdash \psi(\chi)$ is derivable and address whether there is necessarily a *quantifier-free* such witness. The answer to this question is indeed **positive** by the following argument.

It is well known that first-order intuitionistic propositional logic enjoys *uniform interpolation*, and so interprets its second-order version, a result due to Pitts. In fact there is such an interpretation that commutes with all of first-order intuitionistic propositional logic, say the $*$-translation in Section 3 of Pitts. So we can reason as follows:

- Assume $\Gamma \vdash \psi(\chi)$ is derivable.
- Then also $\Gamma^* \vdash (\psi(\chi))^*$ is derivable by Proposition 9 of Pitts.
- Since $*$ commutes with (first-order) propositional connectives we have that $\Gamma^* = \Gamma$ and $(\psi(\chi))^* = \psi(\chi^*)$ and so $\Gamma \vdash \psi(\chi^*)$ is derivable.
- However $\chi^*$ is quantifier-free, and so serves as the desired witness.

edit note: I changed the title of this question, and edited the order of the presentation, so that the actual question being asked can be ascertained faster. $\endgroup$isdefined by a proof system, it's giving itsemanticsthat's hard. The canonical rules are the sequent rules $\Gamma \vdash P[X:=T] $\Rightarrow \Gamma \vdash \exists X. P$ and $\Gamma, P[X:=Y] \vdash \Delta $\Rightarrow \Gamma, \exists X.P \vdash \Delta$ (where $X$ is a variable, $Y$ is a fresh variable, and $T$ is anarbitraryformula) for the existential quantifier, and dual rules for the universal $\forall$, added to the usual sequent calculus for intuitionistic logic. $\endgroup$3more comments