6
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ 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$
    – Z. A. K.
    Sep 23, 2023 at 5:25
  • 2
    $\begingroup$ Do you not need to specify a proof system for SOL? Is there a canonical choice? $\endgroup$ Sep 23, 2023 at 5:30
  • $\begingroup$ @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. $\endgroup$
    – Z. A. K.
    Sep 23, 2023 at 5:49
  • $\begingroup$ Is this written somewhere? $\endgroup$ Sep 23, 2023 at 5:49
  • 2
    $\begingroup$ @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. $\endgroup$
    – Z. A. K.
    Sep 23, 2023 at 6:04

1 Answer 1

5
$\begingroup$

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.
$\endgroup$
2
  • $\begingroup$ 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 🫣. $\endgroup$
    – Z. A. K.
    Oct 17, 2023 at 5:35
  • 1
    $\begingroup$ No problem! I hope the second part of my answer is nonetheless useful. $\endgroup$
    – Anupam Das
    Oct 17, 2023 at 9:22

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.