Three ways of recognizing essential formulas in sequents

V. P. Orevkov

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 163-175

Résumé

Let $A$ be a formula, $\Gamma\to\Delta$ be a sequent. The formula $A$ is unessential in $A,\Gamma\to\Delta$ if derivability of $A,\Gamma\to\Delta$ implies derivability of $\Gamma\to\Delta$. The paper describes 3 sufficient conditions for a formula to be unessential in classical and intuitionistic predicate calculus. The conditions are applied for proving hereditary unsolvability of these theories: 1) the intuitionistic equality theory with the axiom $\rceil\rceil\forall xy(x=y)$, the scheme \begin{equation} \forall_\alpha\rceil\rceil A\supset\rceil\rceil\forall_\alpha A \end{equation} and the scheme \begin{equation} \rceil A\vee\rceil\rceil A; \end{equation} 2) the intuitionistic monadic predicate calculus with one predicate letter with the axiom the scheme (1) and the scheme (2).