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

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.

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?

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.

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

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

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?

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

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.

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?

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language. Predicative SOL (studied e.g. by F. Ferreira) denotes the variant of SOL in the same language which restricts the quantifier rules of SOL

$$\frac{\Gamma \vdash \varphi[X:=A]}{\Gamma \vdash \exists X. \varphi} \ \ \ \ \ \ \ \ \ \ \ \ \frac{\Gamma, \varphi[X:=A] \vdash \Delta}{\Gamma, \forall X.\varphi \vdash \Delta}$$

by requiring that $A$ be a quantifier-free formula.

Question: How conservative is full SOL over its predicative variant? In particular, consider a sequent $\Gamma \vdash \exists X. \varphi$ in which $\Gamma$ and $\varphi$ are both quantifier-free. If $\Gamma \vdash \exists X. \varphi$ has a SOL-proof, does it always have a Predicative SOL proof?

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

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

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?