Completeness of HPC with Respect to RE and Post Structures

Abstract

Validity in recursive structures has been investigated by several authors. Kreisel has shown that there exists a consistent sentence of classical predicate calculus (CPC) that does not possess a recursive model. The sentence is a conjunction of the axioms of a variant of Bernay’s set theory, including the axiom of infinity. The language contains additional constants besides ∈. Later Kreisel and Mostowski presented a sentence (not possessing recursive models) which was a conjunction of axioms of a variant of Bernay’s set theory without the axiom of infinity but still with additional constants besides ∈. Later Mostowski improved the result by giving a sentence which can be demonstrated in Heyting arithmetic to be consistent and to have no recursive models. Rabin obtained a simple proof that some sentence of set theory with the single nonlogical constant ∈ does not have any recursively enumerable models.