We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg’s implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player, ∃ros, is trying to construct a proof in normal form while his opponent, ∀phrodite, attempts to build a counter-model. The determinacy of the game implies therefore both completeness and semantic cut-elimination.

We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable.

The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable in presence of free type variables (constants). This contrasts with the result that inutitionistic propositional second-order logic with existential quantifier, conjunction and negation is decidable.

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 ∧, ∨, →, ⊥, ∀, and ∃, 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 ∃ from the propositional connectives and nondefinability of ∀ from ∃ in the second-order intuitionistic propositional logic. We also show (...) that the ∀-free fragment of IPC2 is undecidable. (shrink)