On second order intuitionistic propositional logic without a universal quantifier. (English) Zbl 1163.03010

IPC\(^2\) is the intuitionistic second-order propositional calculus. The author proves that sentences (closed formulas) \(\phi\) without \(\forall\) constitute a Glivenko class: \(\phi\) is provable in IPC\(^2\) iff \(\phi\) is a classical tautology with \(\exists p\alpha(p)\) interpreted as \(\alpha(\top)\vee\alpha(\bot)\). For formulas with free variables, like \(p\vee\neg p\), this is false. The result is shown by a modification of Kalmar’s completeness proof for classical propositional logic. For every \(\phi(p_1,\dots,p_n)\) with free variables \(p_1,\dots,p_n\) without \(\forall\) induction on \(\phi\), the author shows that intuitionistically \(p_1^{\varepsilon_1}\&\dots\&p_n^{\varepsilon_n}\to \phi^{\varepsilon}\), where \(\varepsilon_1,\dots,\varepsilon_n\) are truth-values of \(p_1,\dots,p_n\) and \(\varepsilon\) is the corresponding classical truth-value of \(\phi\). In the (crucial) \(\exists\)-case, one uses the formula \(\phi(\tau)\to\exists p\phi(p)\) for \(\varepsilon=1\) and the formula \((\forall p((p\vee\neg p)\to\neg\phi(p)))\to \neg\exists p\phi(p)\) for \(\varepsilon=0\). As a consequence, \(\forall\) is not intuitionistically definable in terms of the remaining connectives.


03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI


[1] Lectures on the Curry-Howard isomorphism (2006) · Zbl 1183.03004
[2] Matematicheskie Zamietki AN SSSR 22 pp 69– (1977)
[3] Proceedings of TLCA 2005 3461 pp 194– (2005)
[4] Embedding first order predicate logic in fragments of intuitionistic logic 41 pp 705– (1976)
[5] Types for proofs and programs, international workshop TYPES ’93 806 pp 131– (1994) · Zbl 0825.00120
[6] DOI: 10.1305/ndjfl/1039118868 · Zbl 0966.03008
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.