Hirschfeld and Wheeler proved in 1975 that ∑1 ultrapowers (= “simple models”) are rigid; i.e., they admit no non-trivial automorphisms. We later noted, essentially mimicking their technique, that the same is true of Δ1 ultrapowers (= “Nerode semirings”), a class of models of Π2 Arithmetic that overlaps, but is mutually non-inclusive with, the class of Σ1 ultrapowers. Hirschfeld and Wheeler left as open the question whether some Σ1 ultrapowers might admit proper isomorphic self-injections. We do not answer that question; but (...) we do answer the corresponding question, in the negative, for the Δ1 case. (shrink)

Several problems that pertain to certain arithmetically well-behaved countable subsemirings of Λ, the semiring of isols, are discussed. This is relevant to the present volume memorializing the late John Myhill, in that Myhill was an early co-developer of the theory of Λ.

We construct a recursive ultrapower F/U such that F/U is a tame 1-model in the sense of [6, §3] and FU is existentially incomplete in the models of II2 arithmetic. This enables us to answer in the negative a question about closure with respect to recursive fibers of certain special semirings Γ of isols termed tame models by Barback. Erik Ellentuck had conjuctured that all such semirings enjoy the closure property in question. Our result is that while many do, some (...) do not. (shrink)

We prove that any proof of a [Formula: see text] sentence in the theory [Formula: see text] can be translated into a proof in [Formula: see text] at the cost of a polynomial increase in size. In fact, the proof in [Formula: see text] can be obtained by a polynomial-time algorithm. On the other hand, [Formula: see text] has nonelementary speedup over the weaker base theory [Formula: see text] for proofs of [Formula: see text] sentences. We also show that for (...) [Formula: see text], proofs of [Formula: see text] sentences in [Formula: see text] can be translated into proofs in [Formula: see text] at a polynomial cost in size. Moreover, the [Formula: see text]-conservativity of [Formula: see text] over [Formula: see text] can be proved in [Formula: see text], a fragment of bounded arithmetic corresponding to polynomial-time computation. For [Formula: see text], this answers a question of Clote, Hájek and Paris. (shrink)

A cohesive power of a structure is an effective analog of the classical ultrapower of a structure. We start with a computable structure, and consider its effective power over a cohesive set of natural numbers. A cohesive set is an infinite set of natural numbers that is indecomposable with respect to computably enumerable sets. It plays the role of an ultrafilter, and the elements of a cohesive power are the equivalence classes of certain partial computable functions determined by the cohesive (...) set. Thus, unlike many classical ultrapowers, a cohesive power is a countable structure. In this paper we focus on cohesive powers of graphs, equivalence structures, and computable structures with a single unary function satisfying various properties, which can also be viewed as directed graphs. For these computable structures, we investigate the isomorphism types of their cohesive powers, as well as the properties of cohesive powers when they are not isomorphic to the original structure. (shrink)

Given a Δ1 ultrapower ℱ/[MATHEMATICAL SCRIPT CAPITAL U], let ℒU denote the set of all Π2-correct substructures of ℱ/[MATHEMATICAL SCRIPT CAPITAL U]; i.e., ℒU is the collection of all those subsets of |ℱ/[MATHEMATICAL SCRIPT CAPITAL U]| that are closed under computable functions. Defining in the obvious way the lattice ℒ) with domain ℒU, we obtain some preliminary results about lattice embeddings into – or realization as – an ℒ. The basis for these results, as far as we take the matter, (...) consists of the well-known class of minimal ℱ/[MATHEMATICAL SCRIPT CAPITAL U]'s, which function as atoms, and the class of minimalfree ℱ/[MATHEMATICAL SCRIPT CAPITAL U]'s, to whose nonemptiness a substantial section of the paper is devoted. It is shown that an infinite, convergent monotone sequence together with its limit point is embeddable in an ℒ, and that the initial segment lattices {0, 1,…, n } are not just embeddable in , but in fact realizable as, lattices ℒ. Finally, the diamond is embeddable; and if it is not realizable, then either the 1 - 3 - 1 lattice or the pentagon is at least embeddable. (shrink)

We link two concepts from the literature, namely hard sequences for the satisfiability problem sat and so‐called pseudo proof systems proposed for study by Krajíček. Pseudo proof systems are elements of a particular nonstandard model constructed by forcing with random variables. We show that the existence of mad pseudo proof systems is equivalent to the existence of a randomized polynomial time procedure with a highly restrictive use of randomness which produces satisfiable formulas whose satisfying assignments are probably hard to find.