In [1], William H. Jobe has shown that a certain three-valued proper logic is canonically complete, i.e., each first order J is expressible by a formula that is in M-normal form. The first order operator Jk(p)1 represents the truth table of a possible formula which has the truth value k in the ith row and the truth value 1 in all other rows. “The M-normal form of a given formula is another formula which has the same truth table as the given formula but which contains no operation symbols other than those of conjunction, disjunction, and undefined unary operations, with no nonunary operation, i.e., conjunction or alternation, included in the scope of an operation which is unary, and no alternation included in the scope of a conjunction.” Here it is shown that it is possible to construct a canonically complete proper logic for each choice of M which contains, in addition to alternation and conjunction, exactly two unary operations. Moreover, it is further shown that at least two unary operations are necessary in order for such a logic to be canonically complete.

If S, T are stationary subsets of a regular uncountable cardinal κ, we say that S reflects fully in T, S < T, if for almost all α ∈ T (except a nonstationary set) S ∩ α stationary in α. This relation is known to be a well-founded partial ordering. We say that a given poset P is realized by the reflection ordering if there is a maximal antichain 〈Xp: p ∈ P〉 of stationary subsets of Reg(κ) so that

We prove that if , and P is an arbitrary well-founded poset of cardinality ≤ κ+ then there is a generic extension where P is realized by the reflection ordering on κ.

In [1] the ω-consistency of arithmetic was proved by a method which yields fine ordinal bounds for κ-consistency, κ ≥ 1. In this paper these bounds are shown to be best possible. The ω-consistency of a number-theoretic system S can be expressed thus: for all sentences ∃xM,

where ProvS is the proof predicate for S, if n is a nonnegative integer then n is the formal numeral (of S) for n, and if G is a formula then ˹G˺ is the Gödel number of G. The κ-consistency of S is the restriction of (1) to Σκ0 sentences ∃xM. The proof in [1] establishes the no-counterexample interpretation of (1), that is, the existence of a constructive functional Φ such that, for all sentences ∃xM, all numbers p, and all functions f,

(see [1, §2]). A functional Φ is an ω-consistency functional for S if it satisfies (2) for all sentences ∃xM, and a κ-consistency functional for S if it satisfies (2) for all Σκ0 sentences ∃xM.

The systems considered in [1] are those obtained from classical first-order arithmetic Z, including the schema for definition of primitive recursive (p.r.) functions, by adjoining, for some p.r. well-founded ordering ≺ of the nonnegative integers, the axiom schema

that is, the least number principle on ≺; it is equivalent to the schema of transfinite induction on ≺.

In this paper we show the finite controllability of the Maslov class of formulas of pure quantification theory (specified immediately below). That is, we show that every formula in the class has a finite model if it has a model at all. A signed atomic formula is an atomic formula or the negation of one; a binary disjunction is a disjunction of the form A1 ⋁ A2, where A1 and A2 are signed atomic formulas; and a formula is Krom if it is a conjunction of binary disjunctions. Finally, a prenex formula is Maslov if its prefix is ∃···∃∀···∀∃···∃ and its matrix is Krom.

A number of decidability results have been obtained for formulas classified along these lines. It is a consequence of Theorems 1.7 and 2.5 of [4] that the following are reduction classes (for satisfiability): the class of Skolem formulas, that is, prenex formulas with prefixes ∀···∀∃···∃, whose matrices are conjunctions one conjunct of which is a ternary disjunction and the rest of which are binary disjunctions; and the class of Skolem formulas containing identity whose matrices are Krom. Moreover, the following results (for pure quantification theory, that is, without identity) are derived in [1] and [2]: the classes of prenex formulas with Krom matrices and prefixes ∃∀∃∀, or prefixes ∀∃∃∀, or prefixes ∀∃∀∀ are all reduction classes, while formulas with Krom matrices and prefixes ∀∃∀ comprise a decidable class. The latter class, however, is not finitely controllable, for it contains formulas satisfiable only over infinite universes. The Maslov class was shown decidable by Maslov in [11].