The occurrence of an implication in finitely valid, intuitively improvable formulas of propositional logic

D. P. Skvortsov

Matematičeskie zametki, Tome 20 (1976) no. 3, pp. 383-390.

Résumé

Kabakov has proved that for the finite validity (in Medvedev's sense) of intuitively unprovable propositional formulas it is necessary that an implication occur in the premise $\beta$ or else in the inference $\gamma$ of some subformula of the type $(\beta\to\gamma)$, and, consequently, that at least two implications be present. Here we prove that every finitely valid, intuitively unprovable formula contains the occurrence of an implication necessarily in the premise $\beta$ of some subformula of the form $(\beta\to\gamma)$ and we also present an example of a similar formula containing exactly two implications.