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.

Improve this question
$\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.
    Commented 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$
    – James E Hanson
    Commented 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.
    Commented Sep 23, 2023 at 5:49
  • $\begingroup$ Is this written somewhere? $\endgroup$
    – James E Hanson
    Commented 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.
    Commented Sep 23, 2023 at 6:04

1 Answer 1

Reset to default
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.
Improve this answer
$\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.
    Commented Oct 17, 2023 at 5:35
  • 1
    $\begingroup$ No problem! I hope the second part of my answer is nonetheless useful. $\endgroup$
    – Anupam Das
    Commented Oct 17, 2023 at 9:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .