bluuebunny/crossref_metadata_2025 huggingface dataset:
On the strength of König's duality theorem for countable bipartite graphs
Authors: Simpson Stephen G.
Published: May 2006

Let CKDT be the assertion that for every countably infinite bipartite graph G, there exist a vertex covering C of G and a matching M in G such that C consists of exactly one vertex from each edge in M. (This is a theorem of Podewski and Stefifens [12].) Let ATR0 be the subsystem of second-order arithmetic with arithmetical transfinite recursion and restricted induction. Let RCA0 be the subsystem of second-order arithmetic with recursive comprehension and restricted induction. We show that CKDT is provable in ATR0. Combining this with a result of Aharoni, Magidor, and Shore [2], we see that CKDT is logically equivalent to the axioms of ATR0, the equivalence being provable in RCA0.
Hilbert's program and the omega-rule
Authors: Ignjatović Aleksandar
Published: May 2006

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 theoryZ. On the other hand, he claims thatZwith 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) inZdoes not imply that the consistency ofZcannot 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.
On expandability of models of Peano arithmetic to models of the alternative set theory
Authors: Tzouvaras Athanassios
Published: May 2006

We give a sufficient condition for a countable model M of PA to be expandable to an ω-model of AST with absolute Ω-orderings. The condition is in terms of saturation schemes or, equivalently, in terms of the ability of the model to code sequences which have some kind of definition in (M, ω). We also show that a weaker scheme of saturation leads to the existence of wellorderings of the model with nice properties. Finally, we answer affirmatively the question of whether the intersection of all β-expansions of a β-expandable model M is the set RA(M, ω)—the ramified analytical hierarchy over (M, ω).

The results are based on forcing constructions.
Splittings and the finite model property
Authors: Kracht Marcus
Published: May 2006

An old conjecture of modal logics states that every splitting of the major systems K4, S4, G and Grz has the finite model property. In this paper we will prove that all iterated splittings of G have fmp, whereas in the other cases we will give explicit counterexamples. We also introduce a proof technique which will give a positive answer for large classes of splitting frames. The proof works by establishing a rather strong property of these splitting frames namely that they preserve the finite model property in the following sense. Whenever an extension Λ has fmp so does the splitting Λ/f of Λ by f. Although we will also see that this method has its limitations because there are frames lacking this property, it has several desirable side effects. For example, properties such as compactness, decidability and others can be shown to be preserved in a similar way and effective bounds for the size of models can be given. Moreover, all methods and proofs are constructive.
On the Σ2-theory of the upper semilattice of Turing degrees
Authors: Jockusch Carl G. , Slaman Theodore A.
Published: May 2006

A first-order sentence Φ is Σ2 if there is a quantifier-free formula Θ such that Φ has the form . The Σ2-theory of a structure for a language ℒ is the set of Σ2-sentences of ℒ true in . It was shown independently by Lerman and Shore (see [Le, Theorem VII.4.4]) that the Σ2-theory of the structure = 〈D, ≤ 〉 is decidable, where D is the set of degrees of unsolvability and ≤ is the standard ordering of D. This result is optimal in the sense that the Σ3-theory of is undecidable, a result due to J. Schmerl. (For a proof, see [Le, Theorem VII.4.5]. As Lerman has pointed out, this proof should be corrected by defining θσ to be ∀xσ1(x) rather than ∀x(ψ(x)→ σ1(x)).) Nonetheless, in this paper we extend the decidability result of Lerman and Shore by showing that the Σ2-theory of is decidable, where ⋃ is the least upper bound operator and 0 is the least degree. Of course ⋃ is definable in , but many interesting degree-theoretic results are expressible as Σ2-sentences in the language of ∪ but not as Σ2-sentences in the language of . For instance, Simpson observed that the Posner-Robinson cupping theorem could be used to show that for any nonzero degrees a, b, there is a degree g such that b ≤ a ⋃ g, and b ⋠ g (see [PR, Corollary 6]). However, the Posner-Robinson technique does not seem to suffice to decide the Σ2-theory of ∪. We introduce instead a new method for coding a set into the join of two other sets and use it to decide this theory.
Forcing disabled
Authors: Stanley M. C.
Published: May 2006

It is proved (Theorem 1) that if 0# exists, then any constructible forcing property which over L adds no reals, over V collapses an uncountable L-cardinal to cardinality ω. This improves a theorem of Foreman, Magidor, and Shelah. Also, a method for approximating this phenomenon generically is found (Theorem 2). The strategy is first to reduce the problem of ‘disabling’ forcing properties to that of specializing certain trees in a weak sense.
Independence, randomness and the axiom of choice
Authors: van Lambalgen Michiel
Published: May 2006

We investigate various ways of introducing axioms for randomness in set theory. The results show that these axioms, when added to ZF, imply the failure of AC. But the axiom of extensionality plays an essential role in the derivation, and a deeper analysis may ultimately show that randomness is incompatible with extensionality.
Meager nowhere-dense games (IV): n-tactics (continued)
Authors: Scheepers Marion
Published: May 2006

We consider the infinite game where player ONE chooses terms of a strictly increasing sequence of first category subsets of a space and TWO chooses nowhere dense sets. If after ω innings TWO's nowhere dense sets cover ONE's first category sets, then TWO wins. We prove a theorem which implies for the real line: If TWO has a winning strategy which depends on the most recent n moves of ONE only, then TWO has a winning strategy depending on the most recent 3 moves of ONE (Corollary 3). Our results give some new information concerning Problem 1 of [S1] and clarifies some of the results in [B-J-S] and in [S1].
Filters on the space of partitions Qκ(λ)
Authors: Méndez Gisela M.
Published: May 2006

The importance of the fine and normal filters, which are the theme of this work, appears naturally in the study of large cardinals. It is well known that the filter generated by the closed unbounded sets on Pκ(λ), where κ is a regular cardinal, is the minimal normal filter that contains the cones on each of these spaces. Henle and Zwicker [5] introduce the space Qκ(λ) of partitions of λ with size less than κ and described several notions of normality such that the existence of fine and “normal” ultrafilters on this space has strong implications, such as κ is λ supercompact. We propose in the present paper to study the existence of fine and “normal” filters on Qκ(λ). We will work with the different notions of normality introduced in [5] and also a different new definition for normality on Qκ(λ), characterizing, in case it exists, the minimal “normal” filter containing the cones on Qκ(λ).
Polynomially and superexponentially shorter proofs in fragments of arithmetic
Authors: Montagna Franco
Published: May 2006

In Parikh [71] it is shown that, if T is an r.e. consistent extension of Peano arithmetic PA, then, for each primitive recursive function g, there is a formula φ of PA such that

(In the following, Proof T(z, φ) and Prov T(φ) denote the metalinguistic assertions that z codes a proof of φ in T and that φ is provable in T respectively, where ProofT(z, ┌φ┐) and ProvT(┌φ┐) are the formalizations of Proof T(z,φ) and ProvT(φ) respectively in the language of PA, ┌φ┐ denotes the Gödel number of φ and ┌φ┐ denotes the corresponding numeral. Also, for typographical reasons, subscripts will not be made boldface.) If g is a rapidly increasing function, we express (1) by saying that ProvT(┌φ┐) has a much shorter proof modulo g than φ. Parikh's result is based on the fact that a suitable formula A(x), roughly asserting that (1) holds with x in place of φ, has only provable fixed points. In de Jongh and Montagna [89], this situation is generalized and investigated in a modal context. There, a characterization is given of arithmetical formulas arising from modal formulas of a suitable modal language which have only provable fixed points, and Parikh's result is obtained as a particular case.
Rules of inference with parameters for intuitionistic logic
Authors: Rybakov Vladimir V.
Published: May 2006

An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus H and, in particular, also in the usual form without parameters, is presented. This algorithm is obtained by means of special intuitionistic Kripke models, which are constructed for a given inference rule. Thus, in particular, the direct solution by intuitionistic techniques of Friedman's problem is found. As a corollary an algorithm for the recognition of the solvability of logical equations in H and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in H is constructed.
Prime numbers and factorization in IE1 and weaker systems
Authors: Smith Stuart T.
Published: May 2006

We show that IE1 proves that every element greater than 1 has a unique factorization into prime powers, although we have no way of recovering the exponents from the prime powers which appear. The situation is radically different in Bézout models of open induction. To facilitate the construction of counterexamples, we describe a method of changing irreducibles into powers of irreducibles, and we define the notion of a frugal homomorphism into , the product of the p-adic integers for each prime p.
Indécidabilité de la théorie des paires immédiates de corps valués henseliens
Authors: Delon Françoise
Published: May 2006

The theory of immediate pairs of Henselian valued fields, with a given residual theory (of characteristic zero) and a given theory of valuation group (nonzero), is undecidable and has completions.
Decidable discriminator varieties from unary varieties
Authors: Burris Stanley , Mckenzie Ralph , Valeriote Matthew
Published: May 2006

We determine precisely those locally finite varieties of unary algebras of finite type which, when augmented by a ternary discriminator, generate a variety with a decidable theory.
A construction of superstable ndop-notop groups
Authors: Baudisch Andreas
Published: May 2006

The paper continues [1]. Let S be a complete theory of ultraflat (e.g. planar) graphs as introduced in [4]. We show a strong form of NOTOP for S: The union of two models M1 and M2, independent over a common elementary submodel M0, is the primary model over M1 ∪ M2 of S. Then by results of [1] Mekler's construction [6] gives for such a theory S of nice ultraflat graphs a superstable 2-step-nilpotent group of exponent p (> 2) with NDOP and NOTOP.
A set mapping with no infinite free subsets
Authors: Komjáth P.
Published: May 2006

It is consistent that there exists a set mapping F: [ω2]2 → [ω2]<ω such that F(α,β) ⊆ α for α < β < ω2 and there is no infinite free subset for F. This solves a problem of A. Hajnal and A. Máté.
Weak presentations of computable fields
Authors: Jockusch Carl G. , Shlapentokh Alexandra
Published: May 2006

It is shown that for any computable field K and any r.e. degree a there is an r.e. set A of degree a and a field F ≃ K with underlying set A such that the field operations of F (including subtraction and division) are extendible to (total) recursive functions. Further, it is shown that if a and b are r.e. degrees with b ≤ a, there is a 1-1 recursive function f: ℚ → ω such that f(ℚ) ∈ a, f(ℤ) ∈ b, and the images of the field operations of ℚ under f can be extended to recursive functions.
Definability in functional analysis
Authors: Iovino José
Published: May 2006

The role played by real-valued functions in functional analysis is fundamental. One often considers metrics, or seminorms, or linear functionals, to mention some important examples.

We introduce the notion of definable real-valued function in functional analysis: a real-valued function f defined on a structure of functional analysis is definable if it can be “approximated” by formulas which do not involve f. We characterize definability of real-valued functions in terms of a purely topological condition which does not involve logic.
Completeness of global intuitionistic set theory
Authors: Titani Satoko
Published: May 2006

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequents

Considering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.

The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.

Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.
Lower bounds for cutting planes proofs with small coefficients
Authors: Bonet Maria , Pitassi Toniann , Raz Ran
Published: May 2006

We consider small-weight Cutting Planes (CP*) proofs; that is, Cutting Planes (CP) proofs with coefficients up to Poly(n). We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP* proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution.

We also prove the following two theorems: (1) Tree-like CP* proofs cannot polynomially simulate non-tree-like CP* proofs. (2) Tree-like CP* proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other.

Our proofs also work for some generalizations of the CP* proof system. In particular, they work for CP* with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference.
Branching-time logic with quantification over branches: The point of view of modal logic
Authors: Zanardo Alberto
Published: May 2006

In Ockhamist branching-time logic [Prior 67], formulas are meant to be evaluated on a specified branch, or history, passing through the moment at hand. The linguistic counterpart of the manifoldness of future is a possibility operator which is read as ‘at some branch, or history (passing through the moment at hand)’. Both the bundled-trees semantics [Burgess 79] and the 〈moment, history〉 semantics [Thomason 84] for the possibility operator involve a quantification over sets of moments. The Ockhamist frames are (3-modal) Kripke structures in which this second-order quantification is represented by a first-order quantification. The aim of the present paper is to investigate the notions of modal definability, validity, and axiomatizability concerning 3-modal frames which can be viewed as generalizations of Ockhamist frames.
Lebesque measure zero subsets of the real line and an infinite game
Authors: Scheepers Marion
Published: May 2006

Let denote the ideal of Lebesgue measure zero subsets of the real line. Then add() denotes the minimal cardinality of a subset of whose union is not an element of . In [1] Bartoszynski gave an elegant combinatorial characterization of add(), namely: add() is the least cardinal number κ for which the following assertion fails:

For every family of at mostκ functions from ω to ω there is a function F from ω to the finite subsets of ω such that:

1. For each m, F(m) has at most m + 1 elements, and

2. for each f inthere are only finitely many m such that f(m) is not an element of F(m).

The symbol A(κ) will denote the assertion above about κ. In the course of his proof, Bartoszynski also shows that the cardinality restriction in 1 is not sharp. Indeed, let (Rm: m < ω) be any sequence of integers such that for each m Rm, ≤ Rm+1, and such that limm→∞Rm = ∞. Then the truth of the assertion A(κ) is preserved if in 1 we say instead that

1′. For each m, F(m) has at most Rm elements.

We shall use this observation later on. We now define three more statements, denoted B(κ), C(κ) and D(κ), about cardinal number κ.
How connected is the intuitionistic continuum?
Authors: Dalen Dirk Van
Published: May 2006

In the twenties Brouwer established the well-known continuity theorem “every real function is locally uniformly continuous,” [3, 2, 5]. From this theorem one immediately concludes that the continuum is indecomposable (unzerlegbar), i.e., if ℝ = A ∪ B and A ∩ B = ∅ (denoted by ℝ = A + B), then ℝ = A or ℝ = B.

Brouwer deduced the indecomposability directly from the fan theorem (cf. the 1927 Berline Lectures, [7, p. 49]).

The theorem was published for the first time in [6], it was used to refute the principle of the excluded middle: ¬∀x ∈ ℝ (x ∈ ℚ ∨ ¬x ∈ ℚ).

The indecomposability of ℝ is a peculiar feature of constructive universa, it shows that ℝ is much more closely knit in constructive mathematics, than in classically mathematics. The classically comparable fact is the topological connectedness of ℝ. In a way this characterizes the position of ℝ: the only (classically) connected subsets of ℝ are the various kinds of segments. In intuitionistic mathematics the situation is different; the continuum has, as it were, a syrupy nature, one cannot simply take away one point. In the classical continuum one can, thanks to the principle of the excluded third, do so. To put it picturesquely, the classical continuum is the frozen intuitionistic continuum. If one removes one point from the intuitionistic continuum, there still are all those points for which it is unknown whether or not they belong to the remaining part.
Tychonoff's theorem in the framework of formal topologies
Authors: Negri Sara , Valentini Silvio
Published: May 2006

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).

The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.
Gentzenizations of relevant logics with distribution
Authors: Brady Ross T.
Published: May 2006

We establish cut-free left-handed Gentzenizations for a range of major relevant logics from B through to R, all with distribution. B is the basic system of the Routley-Meyer semantics (see [15], pp. 287–300) and R is the logic of relevant implication (see [1], p. 341). Previously, the contractionless logics DW, TW, EW, RW and RWK were Gentzenized in [3], [4] and [5], and also the distributionless logics LBQ, LDWQ, LTWQo, LEWQot, LRWQ, LRWKQ and LRQ in [6] and [7]. This paper provides Gentzenizations for the logics DJ, TJ, T and R, with various levels of contraction, and for the contractionless logic B, which could not be included in [4] using the technique developed there. We also include the Gentzenization of TW in order to compare it with that in [4]. The Gentzenizations that we obtain here for DW and RW are inferior to those already obtained in [4], but they are included for reference when constructing other systems. The logics EW and E present a difficulty for our method and are omitted. For background to the Gentzenization of relevant logics, see [6], and for motivation behind the logics involved, see [6], [1] and [15]. Because of the number of properties that are brought to bear in obtaining these systems, we prefer to consider Gentzenizations for particular logics rather than for arbitrary bunches of axioms.
The Sacks density theorem and Σ2-bounding
Authors: Groszek Marcia J. , Mytilinaios Michael E. , Slaman Theodore A.
Published: May 2006

The Sacks Density Theorem [7] states that the Turing degrees of the recursively enumerable sets are dense. We show that the Density Theorem holds in every model of P− + BΣ2. The proof has two components: a lemma that in any model of P− + BΣ2, if B is recursively enumerable and incomplete then IΣ1 holds relative to B and an adaptation of Shore's [9] blocking technique in α-recursion theory to models of arithmetic.
Set theoretic naturalism
Authors: Maddy Penelope
Published: May 2006

My aim in this paper is to propose what seems to me a distinctive approach to set theoretic methodology. By ‘methodology’ I mean the study of the actual methods used by practitioners, the study of how these methods might be justified or reformed or extended. So, for example, when the intuitionist's philosophical analysis recommends a wholesale revision of the methods of proof used in classical mathematics, this is a piece of reformist methodology. In contrast with the intuitionist, I will focus more narrowly on the methods of contemporary set theory, and, more importantly, I will certainly recommend no sweeping reforms. Rather, I begin from the assumption that the methodologist's job is to account for set theory as it is practiced, not as some philosophy would have it be. This credo lies at the very heart of the so-called ‘naturalism’ to be described here.

A philosopher looking at set theoretic practice from the outside, so to speak, might notice any number of interesting methodological questions, beginning with the intuitionist's ‘why use classical logic?’, but this sort of question is not a live issue for most practicing set theorists. One central question on which the philosopher's and the practitioner's interests converge is this: what is the status of independent statements like the continuum hypothesis (CH)? A number of large questions arise in its wake: what criteria should guide the search for new axioms? For that matter, what reasons support our adoption of the old axioms?
Scott heights of abelian groups
Authors: Nadel Mark E.
Published: May 2006

The Scott height of a structure gives ordinal measure of the inhomogeneity of the structure. The Scott specturm of a collection of structures is the set of Scott heights of structures in the collection. We will recall the precise definitions of these and related concepts in the next section. The reader thoroughly unfamiliar with these notions may want to skip ahead before reading the rest of this Introduction.

In [11] it is shown that every model of the complete theory of (, +, 1), where, as usual, denotes the integers, is ℵ0-homogeneous, and therefore has Scott height at most ω. On the other hand, a footnote in [1] gives a model of the theory of (, +) which is not ℵ0-homogeneous, while in [11] such a model is described which can be expanded to a model of the theory of (, +, 1). However, since it is also true that any model of the theory of (, +) is isomorphic to a subgroup, in fact a pure subgroup, of a direct sum of and a torsion-free divisible group, it is easy to see that any such model must be ≡∞ω to a model of cardinality at most and so must have Scott height below .

After having recalled the relevant material about Scott heights in §2, we will review the situation for torsion abelian groups in §3. In §4 we shall produce torsion-free abelian groups of high Scott height. It is the proof of Theorem 15 that was our primary motivation in writing this paper.
Embedding lattices into the wtt-degrees below 0′
Authors: Downey Rod , Haught Christine
Published: May 2006

A reducibility ≤p is a procedure whereby a set A can be computed from a set B. The most general and most extensively studied reducibility is Turing reducibility (≤T). However, when one analyzes effectiveness considerations in classical mathematics, one often discovers that the relevant reducibilities are stronger (i.e., more restrictive) than ≤T. To illustrate, in combinatorial group theory we find that the word problem is many-one reducible to the conjugacy problem, and that word problems occur in each r.e. truth table (tt-) degree (see, for example, Miller [17]).

In the present paper we are concerned with another strong reducibility: weak truth table (wtt-) reducibility. Here the reader should recall that A ≤wtt, β means that there is a procedure Φ and a recursive function φ such that Φ(β) = A and for all x, the u(Φ(β; X)) < φ (x). That is, the amount of information used in the computation is bounded by φ. The critical difference between truth table and weak truth table reducibilities is that for tt we will at once be “given the whole table.” Thus if Δ is a tt-procedure and δ is its use, then for all x and all strings σ of length δ(x) we can figure out Δ(σ; x). On the other hand if Δ is merely a wtt-procedure it may be that for some string σ, Δ(σ; x)↓, whilst for another string μ of the same length it may be that Δ{μ; x) ↑. We remark that wtt-reducibility arises very naturally both in effective algebra and in the structure of the r.e. T-degrees R. The reader should see, for instance, Downey and Remmel [3], where it is shown that the complexity of r.e. bases of an r.e. vector space V is characterised precisely by the wtt-degrees below V, and also Ladner and Sasso [14] or Downey [1], where the wtt-degrees are used to investigate cupping and capping in R.
∀-free metabelian groups
Authors: Chapuis Olivier
Published: May 2006

In 1965, during the first All-Union Symposium on Group Theory, Kargapolov presented the following two problems: (a) describe the universal theory of free nilpotent groups of class m; (b) describe the universal theory of free groups (see [18, 1.28 and 1.27]). The first of these problems is still open and it is known [25] that a positive solution of this problem for an m ≤ 2 should imply the decidability of the universal theory of the field of the rationals (this last problem is equivalent to Hilbert's tenth problem for the field of the rationals which is a difficult open problem; see [17] and [20] for discussions on this problem). Regarding the second problem, Makanin proved in 1985 that a free group has a decidable universal theory (see [15] for stronger results), however, the problem of deriving an explicit description of the universal theory of free groups is open. To try to solve this problem Remeslennikov gave different characterization of finitely generated groups with the same universal theory as a noncyclic free group (see [21] and [22] and also [11]). Recently, the author proved in [8] that a free metabelian group has a decidable universal theory, but the proof of [8] does not give an explicit description of the universal theory of free metabelian groups.
Canonical forms for definable subsets of algebraically closed and real closed valued fields
Authors: Holly Jan E.
Published: May 2006

We present a canonical form for definable subsets of algebraically closed valued fields by means of decompositions into sets of a simple form, and do the same for definable subsets of real closed valued fields. Both cases involve discs, forming “Swiss cheeses” in the algebraically closed case, and cuts in the real closed case. As a step in the development, we give a proof for the fact that in “most” valued fields F, if f(x), g(x) ∈ F[x] and v is the valuation map, then the set {x: v(f(x)) ≤ v(g(x))} is a Boolean combination of discs; in fact, it is a finite union of Swiss cheeses. The development also depends on the introduction of “valued trees”, which we define formally.
Some theories with positive induction of ordinal strength φω0
Authors: Jäger Gerhard , Strahm Thomas
Published: May 2006

This paper deals with: (i) the theory which results from by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω0.
Decidability of the two-quantifier theory of the recursively enumerable weak truth-table degrees and other distributive upper semi-lattices
Authors: Ambos-Spies Klaus , Fejer Peter A. , Lempp Steffen , Lerman Manuel
Published: May 2006

We give a decision procedure for the ∀∃-theory of the weak truth-table (wtt) degrees of the recursively enumerable sets. The key to this decision procedure is a characterization of the finite lattices which can be embedded into the r.e.wtt-degrees by a map which preserves the least and greatest elements: a finite lattice has such an embedding if and only if it is distributive and the ideal generated by its cappable elements and the filter generated by its cuppable elements are disjoint.

We formulate general criteria that allow one to conclude that a distributive upper semi-lattice has a decidable two-quantifier theory. These criteria are applied not only to the weak truth-table degrees of the recursively enumerable sets but also to various substructures of the polynomial many-one (pm) degrees of the recursive sets. These applications to thepmdegrees require no new complexity-theoretic results. The fact that thepm-degrees of the recursive sets have a decidable two-quantifier theory answers a question raised by Shore and Slaman in [21].
Some model theory for almost real closed fields
Authors: Delon Françoise , Farré Rafel
Published: May 2006

We study the model theory of fields k carrying a henselian valuation with real closed residue field. We give a criteria for elementary equivalence and elementary inclusion of such fields involving the value group of a not necessarily definable valuation. This allows us to translate theories of such fields to theories of ordered abelian groups, and we study the properties of this translation. We also characterize the first-order definable convex subgroups of a given ordered abelian group and prove that the definable real valuation rings of k are in correspondence with the definable convex subgroups of the value group of a certain real valuation of k.
Minimal complementation below uniform upper bounds for the arithmetical degrees
Authors: Kumabe Masahiro
Published: May 2006

This paper was inspired by Lerman [15] in which he proved various properties of upper bounds for the arithmetical degrees. We discuss the complementation property of upper bounds for the arithmetical degrees. In Lerman [15], it is proved that uniform upper bounds for the arithmetical degrees are jumps of upper bounds for the arithmetical degrees. So any uniform upper bound for the arithmetical degrees is not a minimal upper bound for the arithmetical degrees. Given a uniform upper bound a for the arithmetical degrees, we prove a minimal complementation theorem for the upper bounds for the arithmetical degrees below a. Namely, given such a and b < a which is an upper bound for the arithmetical degrees, there is a minimal upper bound for the arithmetical degrees c such that b ∪ c = a. This answers a question in Lerman [15]. We prove this theorem by different methods depending on whether a has a function which is not dominated by any arithmetical function. We prove two propositions (see §1), of which the theorem is an immediate consequence.

Our notation is almost standard. Let A ⊕ B = {2n∣n ∈ A} ∪ {2n + 1∣n + 1∣n ∈ B} for any sets A and B. Let ω be the set of nonnegative natural numbers.
If there is an exactly λ-free abelian group then there is an exactly λ-separable one in λ
Authors: Shelah Saharon
Published: May 2006

We give a solution stated in the title to problem 3 of part 1 of the problems listed in the book of Eklof and Mekler [2], p. 453. There, in pp. 241-242, this is discussed and proved in some cases. The existence of strongly λ-free ones was proved earlier by the criteria in [5] and [3]. We can apply a similar proof to a large class of other varieties in particular to the variety of (non-commutative) groups.
Noncappable enumeration degrees below 0e′
Authors: Cooper S. Barry , Sorbi Andrea
Published: May 2006

We prove that there exists a noncappable enumeration degree strictly below 0e′.
Weight ω in stable theories with few types
Authors: Herwig Bernhard
Published: May 2006

We construct a type p with preweight ω with respect to itself in a theory with few types. A type with this property must be present in a stable theory with finitely many (but more than one) countable models. The construction is a modification of Hrushovski's important pseudoplane construction.
The dimension of the negation of transitive closure
Authors: McColm Gregory L.
Published: May 2006

We prove that any positive elementary (least fixed point) induction expressing the negation of transitive closure on finite nondirected graphs requires at least two recursion variables.
Cylindric modal logic
Authors: Venema Yde
Published: May 2006

Treating the existential quantification ∃νi as a diamond ♢i and the identity νi = νj as a constant δij, we study restricted versions of first order logic as if they were modal formalisms. This approach is closely related to algebraic logic, as the Kripke frames of our system have the type of the atom structures of cylindric algebras; the full cylindric set algebras are the complex algebras of the intended multidimensional frames called cubes.

The main contribution of the paper is a characterization of these cube frames for the finite-dimensional case and, as a consequence of the special form of this characterization, a completeness theorem for this class. These results lead to finite, though unorthodox, derivation systems for several related formalisms, e.g. for the valid n-variable first order formulas, for type-free valid formulas and for the equational theory of representable cylindric algebras. The result for type-free valid formulas indicates a positive solution to Problem 4.16 of Henkin, Monk and Tarski [16].
Compactly expandable models and stability
Authors: Casanovas Enrique
Published: May 2006

In analogy to ω-logic, one defines M-logic for an arbitrary structure M (see [5],[6]). In M-logic only those structures are considered in which a special part, determined by a fixed unary predicate, is isomorphic to M. Let L be the similarity type of M and T its complete theory. We say that M-logic is κ-compact if it satisfies the compactness theorem for sets of < κ sentences. In this paper we introduce the related notion of compactness for expandability: a model M is κ-compactly expandable if for every extension T′ ⊇ T of cardinality < κ, if every finite subset of T′ can be satisfied in an expansion of M, then T′ can also be satisfied in an expansion of M. Moreover, M is compactly expandable if it is ∥M∥+-compactly expandable. It turns out that M-logic is κ-compact iff M is κ-compactly expandable.

Whereas for first-order logic consistency and finite satisfiability are the same, consistency with T and finite satisfiability in M are, in general, no longer the same thing. We call the model Mκ-expandable if every consistent extension T′ ⊇ T of cardinality < κ can be satisfied in an expansion of M. We say that M is expandable if it is ∥M∥+-expandable. Here we study the relationship between saturation, expandability and compactness for expandability. There is a close parallelism between our results about compactly expandable models and some theorems of S. Shelah about expandable models, which are in fact expressed in terms of categoricity of PC-classes (see [7, Th. VI.5.3, VI.5.4 and VI.5.5]). Our results could be obtained directly from these theorems of Shelah if expandability and compactness for expandability were the same notion.
On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
Authors: Buss Samuel R.
Published: May 2006

This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact, unbounded) proof speedup of (i + l)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and • as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as axioms and allows all generalizations of axioms as axioms.

Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman.
A jump operator for subrecursion theories
Authors: Heaton A.J.
Published: May 2006

In classical recursion theory, the jump operator is an important concept fundamental in the study of degrees. In particular, it provides a way of defining the hyperarithmetic hierarchy by iterating over Kleene's O. In subrecursion theories, hierarchies (variants of the fast growing hierarchy) are also important in underlying the central concepts, e.g. in classifying provably recursive functions and associated independence results for given theories (see, e.g. [BW87], [HW96], [R84] and [Z77]). A major difference with the hyperarithmetic hierarchy is in the way each level of a subrecursive hierarchy is crucially dependent upon the system of ordinal notations used (see [F62]). This has been perhaps the major stumbling block in finding a classification of all general recursive functions using such hierarchies.

Here we present a natural subrecursive analogue of the jump operator and prove that the hierarchy based on the ”subrecursive jump” is elementarily equivalent to the fast growing hierarchy.

The paper is organised as follows. First the preliminary definitions are given together with a statement of the main theorem and a brief outline of its proof. The proof of the theorem is then given, with the more technical parts separated out as facts which are proven afterwards.

We let {e}g(x) denote computation of the e-th partial recursion with oracle g, on input x. Furthermore [e] denotes the e-th elementary recursive function, defined so that

Similarly, for a given oracle g the e-th relativized elementary function is denoted by [e]g.
Prime e.c. commutative rings in characteristic n ≥ 2
Authors: Saracino Dan
Published: May 2006

Let CR denote the first-order theory of commutative rings with unity, formulated in the language L = 〈 +, •, 0, 1〉. Virtually everything that is known about existentially complete (e.c.) models of CR is contained in Cherlin's paper [2], where it is shown, in particular, that the e.c. models are not first-order axiomatizable. The purpose of this note is to show that, in analogy with the case of fields, there exists a unique prime e.c. model of CR in each characteristic n > 2. As a consequence we settle Problem 8 in the list of open questions at the end of Hodges' book Building models by games ([5], p. 278).

By a “prime” e.c. model of characteristic n ≥ 2 we mean one that embeds in every e.c. model of characteristic n. (The embedding is not always elementary, since [2] not all e.c. models of characteristic n are elementarily equivalent.) The prime model is characterized by the fact that it is the union of a chain of finite subrings each of which is an amalgamation base for CR. In §1 we describe the finite amalgamation bases for CR and show that every finite model embeds in a finite amalgamation base; in §2 we use this information to obtain prime e.c. models and answer Hodges' question.

Our results on prime e.c. models were obtained some years ago, during the fall term of 1982, while the author was a visitor at Wesleyan University. The author wishes to take this opportunity to thank the mathematics department at Wesleyan for its hospitality during that visit, and subsequent ones.
Transfering saturation, the finite cover property, and stability
Authors: Baldwin John T. , Grossberg Rami , Shelah Saharon
Published: May 2006

Saturation is (μ, κ)-transferable in T if and only if there is an expansion T1 of T with |T1| = |T| such that if M is a μ-saturated model of T1 and |M| ≥ κ then the reduct M|L(T) is κ-saturated. We characterize theories which are superstable without f.c.p., or without f.c.p. as, respectively those where saturation is (ℵ0, λ)-transferable or (κ(T), λ)-transferable for all λ. Further if for some μ ≥ |T|,2μ > μ+, stability is equivalent to for all μ ≥ |T|, saturation is (μ, 2μ)-transferable.
On a class of m.a.d. families
Authors: Zhang Yi
Published: May 2006

We compare several closely related continuum invariants, i.e., a, ae. ap in two forcing models. And we shall ask some open questions in this field.
Interpolation, preservation, and pebble games
Authors: Barwise Jon , van Benthem Johan
Published: May 2006

Preservation and interpolation results are obtained for L∞ω and sublogics ⊆ L∞ω such that equivalence in can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.
An abstract algebraic logic approach to tetravalent modal logics
Authors: Font Josep Maria , Rius Miquel
Published: May 2006

This paper contains a joint study of two sentential logics that combine a many-valued character, namely tetravalence, with a modal character; one of them is normal and the other one quasinormal. The method is to study their algebraic counterparts and their abstract models with the tools of Abstract Algebraic Logic, and particularly with those of Brown and Suszko's theory of abstract logics as recently developed by Font and Jansana in their “A General Algebraic Semantics for Sentential Logics”. The logics studied here arise from the algebraic and lattice-theoretical properties we review of Tetravalent Modal Algebras, a class of algebras studied mainly by Loureiro, and also by Figallo. Landini and Ziliani, at the suggestion of the late Antonio Monteiro.
An elementary definability theorem for first order logic
Authors: Butz C. , Moerdijk I.
Published: May 2006

In this paper, we will present a definability theorem for first order logic. This theorem is very easy to state, and its proof only uses elementary tools. To explain the theorem, let us first observe that if M is a model of a theory T in a language , then, clearly, any definable subset S ⊂ M (i.e., a subset S = {a ∣ M ⊨ φ(a)} defined by some formula φ) is invariant under all automorphisms of M. The same is of course true for subsets of Mn defined by formulas with n free variables.

Our theorem states that, if one allows Boolean valued models, the converse holds. More precisely, for any theory T we will construct a Boolean valued model M, in which precisely the T -provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a formula .

Our presentation is entirely selfcontained, and only requires familiarity with the most elementary properties of model theory. In particular, we have added a first section in which we review the basic definitions concerning Boolean valued models.
Implicit measurements of dynamic complexity properties and splittings of speedable sets
Authors: Jahn Michael A.
Published: May 2006

We prove that any speedable computably enumerable set may be split into a disjoint pair of speedable computably enumerable sets. This solves a longstanding question of J.B. Remmel concerning the behavior of computably enumerable sets in Blum's machine independent complexity theory. We specify dynamic requirements and implement a novel way of detecting speedability—by embedding the relevant measurements into the substage structure of the tree construction. Technical difficulties in satisfying the dynamic requirements lead us to implement “local” strategies that only look down the tree. The (obvious) problems with locality are then resolved by placing an isomorphic copy of the entire priority tree below each strategy (yielding a self-similar tree). This part of the construction could be replaced by an application of the Recursion Theorem, but shows how to achieve the same effect with a more direct construction.
Freeness in classes without equality
Authors: Elgueta Raimon
Published: May 2006

This paper is a continuation of [27], where we provide the background and the basic tools for studying the structural properties of classes of models over languages without equality. In the context of such languages, it is natural to make distinction between two kinds of classes, the so-calledabstruct classes, which correspond to those closed under isomorphic copies in the presence of equality, and thereduced classes, i.e., those obtained by factoring structures by their largest congruences. The generic problem described in [27] is to investigate under what conditions thisreduction processdoes not alter the metatheory of a class.

Here we focus our attention on a concrete aspect of this generic problem that we import from universal algebra, namely the existence and description of free models. As in [27], we can find here again the basic notion ofprotoalgebraicity, which was originally introduced in [7] as the weakest condition to guarantee that the reduction process behaves reasonably well from an algebraic point of view. Our concern, however, takes us to handle a further notion, that ofsemialgebraicity, which corresponds to the notion ofequivalential logicof [18]; semialgebraicity turns out to be the property which ensures that freeness is fully preserved by the reduction process.