zbMATH — the first resource for mathematics

A syntactic embedding of predicate logic into second-order propositional logic. (English) Zbl 1216.03029
Summary: We give a syntactic translation from first-order intuitionistic predicate logic into second-order intuitionistic propositional logic IPC2. The translation covers the full set of logical connectives \(\land , \vee , \rightarrow , \perp , \forall \), and \(\exists \), extending our previous work, which studied the significantly simpler case of the universal-implicational fragment of predicate logic. As corollaries of our approach, we obtain simple proofs of nondefinability of \(\exists \) from the propositional connectives and nondefinability of \(\forall \) from \(\exists \) in the second-order intuitionistic propositional logic. We also show that the \(\forall \)-free fragment of IPC2 is undecidable.

03B20 Subsystems of classical logic (including intuitionistic logic)
03B15 Higher-order logic; type theory (MSC2010)
03B25 Decidability of theories and sets of sentences
Full Text: DOI