In my paper [1], with which I assume the reader is familiar, I defined an arithmetic theory of constructions ATC and gave an interpretation of intuitionistic arithmetic HA in ATC. I proved that, in a suitable sense, every formula provable in HA is also provable in ATC. I proved the converse of this result only for positive sentences. In the present paper I will prove in full generality that any formula of HA which is provable in ATC is already provable in HA. In a later paper I shall use this result to obtain new information about certain extensions of HA by addition of higher types.

Let ZF be the usual Zermelo-Fraenkel set theory formulated without identity, and with the collection axiom scheme. Let ZF−-extensionality be obtained from ZF by using intuitionistic logic instead of classical logic, and dropping the axiom of extensionality. We give a syntactic transformation of ZF into ZF−-extensionality.

Let CPC, HPC respectively be classical, intuitionistic predicate calculus without identity, whose only homological symbol is ∈. We use the ~ ~-translation, a basic tool in the metatheory of intuitionistic systems, which is defined by

The two fundamental lemmas about this ~ ~ -translation we will use are

For proofs, see Kleene [3, Lemma 43a, Theorem 60d].

This - would provide the desired syntactic transformation at least for ZF into ZF− with extensionality, if A− were provable in ZF− for each axiom A of ZF. Unfortunately, the ~ ~-translations of extensionality and power set appear not to be provable in ZF−. We therefore form an auxiliary classical theory S which has no extensionality and has a weakened power set axiom, and show in §2 that the ~ ~-translation of each axiom of Sis provable in ZF−-extensionality. §1 is devoted to the translation of ZF in S.

Let A be a countable admissible set (as defined in [1], [3]). The language LA consists of all infinitary finite-quantifier formulas (identified with sets, as in [1]) that are elements of A. Notationally, LA = A ∩ Lω1ω. Then LA is a countable subset of Lω1ω, the language of all infinitary finite-quantifier formulas with all conjunctions countable. The set is the set of Lω1ω sentences defined in 2.2 below. The following theorem characterizes those A-Σ1 sets Φ of LA sentences that have uncountable models.

Main Theorem (3.1.). If Φ is an A-Σ1set of LA sentences, then the following are equivalent:

(a) Φ has an uncountable model,

(b) Φ has a model with a proper LA-elementary extension,

(c) for every , ⋀Φ → C is not valid.

This theorem was announced in [2] and is proved in §§3, 4, 5. Makkai's earlier [4, Theorem 1] implies that, if Φ determines countable structure up to Lω1ω-elementary equivalence, then (a) is equivalent to (c′) for all , ⋀Φ → C is not valid.

The requirement in 3.1 that Φ is A-Σ1 is essential when the set ω of all natural numbers is an element of A. For by the example of [2], then there is a set Φ LA sentences such that (b) holds and (a) fails; it is easier to show that, if ω ϵ A, there is a set Φ of LA sentences such that (c) holds and (b) fails.

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.

The first section of this paper is concerned with the intrinsic properties of elementary monadic logic (EM), and characterizations in the spirit of Lindström [2] are given. His proofs do not apply to monadic logic since relations are used, and intrinsic properties of EM turn out to differ in certain ways from those of the elementary logic of relations (i.e., the predicate calculus), which we shall call EL. In the second section we investigate connections between higher-order monadic and polyadic logics.

EM is the subsystem of EL which results by the restriction to one-place predicate letters. We omit constants (for simplicity) but take EM to contain identity. Let a type be any finite sequence (possibly empty) of one-place predicate letters. A model M of type has a nonempty universe ∣M∣ and assigns to each predicate letter P of a subset PM of ∣M∣.

Let us take a monadic logic L to be any collection of classes of models, called L-classes, satisfying the following:

1. All models in a given L-class are of the same type (called the type of the class).

2. Isomorphic models lie in the same L-classes.

3. If and are L-classes of the same type, then and are L-classes.

The system , proposed without a claim as to its consistency in [CLg, §15C], has turned out to entail a consequence which is extremely suspicious. For from the axiom ⊦LH it follows that

holds for arbitrary X; hence for X ≡ YH, where Y is a fixed-point combinator, we have

Whether or not this leads to an actual contradiction it would be interesting to know; but, no matter whether it does or not, (2) seems highly counterintuitive.

The aim of this note is to point out that a related system, here called , is demonstrably consistent and sufficient for all practical purposes served by , and at the same time to correct an error in [CLg, §15D2], which was discovered too late to be corrected on the proofs. This is formed from by dropping H from the list of θ's, and hence deleting ⊦LH and (1). The new system does not allow inferential rules to be converted into formulas with the same ease as does ; but if one is content with stating the results as rules, is adequate for all the main results deduced for in [CLg, §15C–D].