Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae

Author:
Publisher website
Google Scholar
Abstract
The purpose of the present article is to formulate in an intuitionistically meaningful manner the completeness problems for the intuitionistic predicate calculus, and to establish the completeness of certain fragments of it. In these proofs certain translations of classical logic into intuitionistic logic are used, in particular those discovered by Kolmogorov [11] and Gödel [3], and a new one in which negations of prenex formulae are central. Since the last one is of interest also independently of the completeness problems, the details are presented separately at the end of this paper.All arguments are intended to be intuitionistically valid unless the opposite is stated; in particular, ‘proof’ means intuitionistic proof, and ‘formal proof’ means proof in the relevant system of Heyting [4], [5].Open problems are mentioned in Remarks 3.1 and 8.1.German capitals denote formulae of predicate logic, Latin (italic) capitals denote predicate symbols or propositional letters.