Provability, Computability and Reflection.

We show that each of the five basic theories of second order arithmetic that play a central role in reverse mathematics has a natural counterpart in the language of nonstandard arithmetic. In the earlier paper [3] we introduced saturation principles in nonstandard arithmetic which are equivalent in strength to strong choice axioms in second order arithmetic. This paper studies principles which are equivalent in strength to weaker theories in second order arithmetic.

In this paper we continue our study, begun in [5], of the connection between ultraproducts and saturated structures. IfDis an ultrafilter over a setI, andis a structure, the ultrapower ofmoduloDis denoted byD-prod. The ultrapower is important because it is a method of constructing structures which are elementarily equivalent to a given structure. Our ultimate aim is to find out what kinds of structure are ultrapowers of. We made a beginning in [5] by proving that, assuming the generalized continuum hypothesis, for (...) each cardinalαthere is an ultrafilterDover a set of powerαsuch that for all structures,D-prodisα+-saturated. (shrink)

A paradox of self-reference in beliefs in games is identified, which yields a game-theoretic impossibility theorem akin to Russell’s Paradox. An informal version of the paradox is that the following configuration of beliefs is impossible:Ann believes that Bob assumes that.

Shelah's theory of forking is generalized in a way which deals with measures instead of complete types. This allows us to extend the method of forking from the class of stable theories to the larger class of theories which do not have the independence property. When restricted to the special case of stable theories, this paper reduces to a reformulation of the classical approach. However, it goes beyond the classical approach in the case of unstable theories. Methods from ordinary forking (...) theory and the Loeb measure construction from nonstandard analysis are used. (shrink)

We consider extensions of Peano arithmetic suitable for doing some of nonstandard analysis, in which there is a predicate N(x) for an elementary initial segment, along with axiom schemes approximating ω 1 -saturation. We prove that such systems have the same proof-theoretic strength as their natural analogues in second order arithmetic. We close by presenting an even stronger extension of Peano arithmetic, which is equivalent to ZF for arithmetic statements.

Introduction. This paper is a sequel to our paper [3]. In that paper we introduced the notion of a finite approximation to an infinitely long formula, in a language L with infinitely long expressions of the type considered by Henkin in [2]. The results of the paper [3] show relationships between the models of an infinitely long sentence and the models of its finite approximations. In the present paper we shall apply the main result of [3] to prove a number (...) of theorems about ordinary finitely long sentences; these theorems are of a type which one might call “preservation theorems”. The following two known results are typical preservation theorems: A sentence φ is preserved under substructures if and only if φ is equivalent to some universal sentence ; φ is preserved under homomorphic images if and only if φ is equivalent to some positive sentence. An expository account of preservation theorems may be found in Lyndon [9].We shall use freely all of the notation introduced in [3], and shall not attempt to make this paper selfcontained. However, the reader should have no difficulty following this paper after he has read [3]. In § 1 we cover some preliminary topics. In § 2 and § 3 we shall illustrate our method in familiar situations by proving anew the two preservation theorems mentioned above. We shall then obtain four new preservation theorems in §§ 4, 5, and 6, involving respectively direct powers and roots, strong homomorphisms and retracts, and direct factors. The result in § 6 was stated in the abstract [4], while the results in § 5 were stated in the abstract [5]. (shrink)

In a nonstandard universe, the κ-saturation property states that any family of fewer than κ internal sets with the finite intersection property has a nonempty intersection. An ordered field F is said to have the λ-Bolzano-Weierstrass property iff F has cofinality λ and every bounded λ-sequence in F has a convergent λ-subsequence. We show that if $\kappa < \lambda$ are uncountable regular cardinals and $\beta^\alpha < \lambda$ whenever $\alpha < \kappa$ and $\beta < \lambda$, then there is a κ-saturated nonstandard (...) universe in which the hyperreal numbers have the λ-Bolzano-Weierstrass property. The result also applies to certain fragments of set theory and second order arithmetic. (shrink)

In a nonstandard universe, the $\kappa$-saturation property states that any family of fewer than $\kappa$ internal sets with the finite intersection property has a nonempty intersection. An ordered field $F$ is said to have the $\lambda$-Bolzano-Weierstrass property iff $F$ has cofinality $\lambda$ and every bounded $\lambda$-sequence in $F$ has a convergent $\lambda$-subsequence. We show that if $\kappa < \lambda$ are uncountable regular cardinals and $\beta^\alpha < \lambda$ whenever $\alpha < \kappa$ and $\beta < \lambda$, then there is a $\kappa$-saturated nonstandard (...) universe in which the hyperreal numbers have the $\lambda$-Bolzano-Weierstrass property. The result also applies to certain fragments of set theory and second order arithmetic. (shrink)

The separation, uniformization, and other properties of the Borel and projective hierarchies over hyperfinite sets are investigated and compared to the corresponding properties in classical descriptive set theory. The techniques used in this investigation also provide some results about countably determined sets and functions, as well as an improvement of an earlier theorem of Kunen and Miller.

We shall prove quantifier elimination theorems for neocompact formulas, which define neocompact sets and are built from atomic formulas using finite disjunctions, infinite conjunctions, existential quantifiers, and bounded universal quantifiers. The neocompact sets were first introduced to provide an easy alternative to nonstandard methods of proving existence theorems in probability theory, where they behave like compact sets. The quantifier elimination theorems in this paper can be applied in a general setting to show that the family of neocompact sets is countably (...) compact. To provide the necessary setting we introduce the notion of a law structure. This notion was motivated by the probability law of a random variable. However, in this paper we discuss a variety of model theoretic examples of the notion in the light of our quantifier elimination results. (shrink)

This paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn on properties S that says "there are n components having S". We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if (...) the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt on properties which has the same relationship with the Circuit Value Problem as reach has with the Directed Reachability Problem. We use alt to show that Πn⊈ FO, Σn⊈ FO, and Δn+1⊈ FOB, solving some open problems raised in [Mat98]. (shrink)

We prove that if is a model of size at most [kappa], λ[kappa] = λ, and a game sentence of length 2λ is true in a 2λ-saturated model ≡ , then player has a winning strategy for a related game in some ultrapower ΠD of . The moves in the new game are taken in the cartesian power λA, and the ultrafilter D over λ must be chosen after the game is played. By taking advantage of the expressive power of (...) game sentences, we obtain several applications showing the existence of ultrapowers with certain properties. In each case, it was previously known that such ultrapowers exist under the assumption of the GCH, and we get them without the GCH. Article O. (shrink)

A general metatheorem is proved which reduces a wide class of statements about continuous time stochastic processes to statements about discrete time processes. We introduce a strong language for stochastic processes, and a concept of forcing for sequences of discrete time processes. The main theorem states that a sentence in the language is true if and only if it is forced. Although the stochastic process case is emphasized in order to motivate the results, they apply to a wider class of (...) random variables. At the end of the paper we illustrate how the theorem can be used with three applications involving submartingales. (shrink)

We obtain an almost everywhere quantifier elimination for (the noncritical fragment of) the logic with probability quantifiers, introduced by the first author in [10]. This logic has quantifiers like $\exists ^{ \ge 3/4} y$ which says that "for at least 3/4 of all y". These results improve upon the 0-1 law for a fragment of this logic obtained by Knyazev [11]. Our improvements are: 1. We deal with the quantifier $\exists ^{ \ge r} y$ , where y is a tuple (...) of variables. 2. We remove the closedness restriction, which requires that the variables in y occur in all atomic subformulas of the quantifier scope. 3. Instead of the unbiased measure where each model with universe n has the same probability, we work with any measure generated by independent atomic probabilities pR for each predicate symbol R. 4. We extend the results to parametric classes of finite models (for example, the classes of bipartite graphs, undirected graphs, and oriented graphs). 5. We extend the results to a natural (noncritical) fragment of the infinitary logic with probability quantifiers. 6. We allow each pR , as well as each r in the probability quantifier $(\exists ^{ \ge r} y)$ , to depend on the size of the universe. (shrink)

Answering a question of Cifú Lopes, we give a syntactic characterization of those continuous sentences that are preserved under reduced products of metric structures. In fact, we settle this question in the wider context of general structures as introduced by the second author.

We characterize Maharam spectra of Loeb probability spaces and give some applications of the results.

The randomization of a complete first-order theory [Formula: see text] is the complete continuous theory [Formula: see text] with two sorts, a sort for random elements of models of [Formula: see text] and a sort for events in an underlying atomless probability space. We study independence relations and related ternary relations on the randomization of [Formula: see text]. We show that if [Formula: see text] has the exchange property and [Formula: see text], then [Formula: see text] has a strict independence (...) relation in the home sort, and hence is real rosy. In particular, if [Formula: see text] is o-minimal, then [Formula: see text] is real rosy. (shrink)

Let T be a complete theory with infinite models in a countable language. The stability function g T (κ) is defined as the supremum of the number of types over models of T of power κ. It is proved that there are only six possible stability functions, namely $\kappa, \kappa + 2^\omega, \kappa^\omega, \operatorname{ded} \kappa, (\operatorname{ded} \kappa)^\omega, 2^\kappa$.

We settle a number of questions concerning definability in first order logic with an extra predicate symbol ranging over semi-linear sets. We give new results both on the positive and negative side: we show that in first-order logic one cannot query a semi-linear set as to whether or not it contains a line, or whether or not it contains the line segment between two given points. However, we show that some of these queries become definable if one makes small restrictions (...) on the semi-linear sets considered. (shrink)