In § 1 of this paper, we characterize the isomorphism property of nonstandard universes in terms of the realization of some second-order types in model theory. In §2, several applications are given. One of the applications answers a question of D. Ross in [this Journal, vol. 55 (1990), pp. 1233–1242] about infinite Loeb measure spaces.

A Boolean algebra B is said to be openly generated if {A : A ≤rcB, ∣A∣ = ℵ0} includes a club subset of . We show:

(V = L). For any cardinal κ there exists an L∞κ-free Boolean algebra which is not openly generated (Proposition 4.1).

(MA+(σ-closed)). Every -free Boolean algebra is openly generated (Theorem 4.2).

The last assertion follows from a characterization of openly generated Boolean algebras under MA+(σ-closed) (Theorem 3.1). Using this characterization we also prove the independence of problem 7 in Ščepin [15] (Proposition 4.3 and Theorem 4.4).

Let T be a one-based theory. We define a notion of width, in the case of T having the finiteness property, for the lattice of finitely generated algebraically closed sets and prove

Theorem. Let T be one-based with the finiteness property. If T is of bounded width, then every type in T is nonorthogonal to a weight one type. If T is countable, the converse is true.

In the first part of this paper we discuss some aspects of Detlefsen's attempt to save Hilbert's Program from the consequences of Gödel's Second Incompleteness Theorem. His arguments are based on his interpretation of the long standing and well-known controversy on what, exactly, finitistic means are. In his paper [1] Detlefsen takes the position that there is a form of the ω-rule which is a finitistically valid means of proof, sufficient to prove the consistency of elementary number theory Z. On the other hand, he claims that Z with its first-order logic is not strong enough to allow a formalization of such an ω-rule. This would explain why the unprovability of Con(Z) in Z does not imply that the consistency of Z cannot be proved by finitistic means. We show that Detlefsen's proposal is unacceptable as originally formulated in [1], but that a reasonable modification of the rule he suggest leads to a partial program already studied for many years. We investigate the scope of such a program in terms of proof-theoretic reducibilities. We also show that this partial program encompasses mathematically important theories studied in the “Reverse Mathematics” program. In order to investigate the provability with such a modified rule, we define new consistency and provability predicates which are weaker than the usual ones. We then investigate their properties, including a few that have no apparent philosophical significance but compare interestingly with the properties of the program based on the iteration of our ω-rule. We determine some of the limitations of such programs, pointing out that these limitations partly explain why partial programs that have been successfully carried out use quite different and substantially more radical extensions of finitistic methods with more general forms of restricted reasoning.