# Existence property for second-order propositional logic

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $$\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$$ language.

Question: Assume that $$\Gamma$$ and $$\Psi$$ are quantifier-free. Assume further that $$\Gamma \vdash \exists X. \Psi(X)$$ is derivable in intuitionistic propositional SOL. Can we find a quantifier-free formula $$T$$ such that $$\Gamma \vdash \Psi(T)$$ is derivable?

The question is motivated by trying to get a better understanding of the predicative variant of SOL studied e.g. by F. Ferreira), which restricts substitution in the $$\exists R$$ and $$\forall L$$ rules to quantifier-free formula.

• 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. Sep 23, 2023 at 5:25
• Do you not need to specify a proof system for SOL? Is there a canonical choice? Sep 23, 2023 at 5:30
• @James Hanson: Indeed. Iintuitionistic propositional SOL is defined by a proof system, it's giving it semantics that'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 an arbitrary formula) for the existential quantifier, and dual rules for the universal $\forall$, added to the usual sequent calculus for intuitionistic logic. Sep 23, 2023 at 5:49
• Is this written somewhere? Sep 23, 2023 at 5:49
• @JamesHanson: In many places, first in Takeuti's 1953 article. But that presentation is a bit long-winded: you can see the rules at a glance in e.g. Fig. 1 of Hermant-Lipton, and in many other articles. Basically, this is the system that was the subject of Takeuti's conjecture, settled by Tait-Girard-others in the late 60s/early 70s. Sep 23, 2023 at 6:04

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.
• Thanks a lot for the answer. Funnily enough, the Pitts quantifier theorem was the main workhorse of the article I was writing that led me to ask the question in the first place, but somehow I still failed to observe its implications for the Harrop case đź«Ł. Oct 17, 2023 at 5:35
• No problem! I hope the second part of my answer is nonetheless useful. Oct 17, 2023 at 9:22