bluuebunny/crossref_metadata_2025 huggingface dataset:
Polynomial time operations in explicit mathematics
Authors: Strahm Thomas
Published: May 2006

In this paper we study (self-)applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on = {0, 1}* are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.
Infinitary logics and very sparse random graphs
Authors: Lynch James F.
Published: May 2006

Let be the infinitary language obtained from the first-order language of graphs by closure under conjunctions and disjunctions of arbitrary sets of formulas, provided only finitely many distinct variables occur among the formulas. Let p(n) be the edge probability of the random graph on n vertices. It is shown that if p(n) ≪ n−1 satisfies certain simple conditions on its growth rate, then for every , the probability that σ holds for the random graph on n vertices converges. In fact, if p(n) = n−α, α > 1, then the probability is either smaller than for some d > 0, or it is asymptotic to cn−d for some c > 0, d ≥ 0. Results on the difficulty of computing the asymptotic probability are given.
On the unification problem for Cartesian closed categories
Authors: Narendran Paliath , Pfenning Frank , Statman Richard
Published: May 2006

Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show that an important subcase, namely unification modulo thelinear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible.

CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming.
Bimodal logics for extensions of arithmetical theories
Authors: Beklemishev Lev D.
Published: May 2006

We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ0 + EXP, PRA); (PRA, IΣn); (IΣm, IΣn) for 1 ≤ m < n; (PA, ACA0); (ZFC, ZFC + CH); (ZFC, ZFC + ¬CH) etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.
Mathias absoluteness and the Ramsey property
Authors: Halbeisen Lorenz , Judah Haim
Published: May 2006

In this article we give a forcing characterization for the Ramsey property of -Sets of reals. This research was motivated by the well-known forcing characterizations for Lebesgue measurability and the Baire property of -sets of reals. Further we will show the relationship between higher degrees of forcing absoluteness and the Ramsey property of projective sets of reals.
The complexity of the modal predicate logic of “true in every transitive model of ZF”
Authors: McGee Vann
Published: May 2006

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕis true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining aninterpretationto be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement thatϕ* is true in every transitive model of ZF, and stipulating that a modal formulaϕisvalidif and only if, for every interpretation *,ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.

In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete.

We also look at a variant notion of validity according to which a formulaϕcounts as valid if and only if, for every interpretation *,ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which isin the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.
On external Scott algebras in nonstandard models of Peano arithmetic
Authors: Kanovei Vladimir
Published: May 2006

We prove that a necessary and sufficient condition for a countable set of sets of integers to be equal to the algebra of all sets of integers definable in a nonstandard elementary extension of ω by a formula of the PA language which may include the standardness predicate but does not contain nonstandard parameters, is as follows: is closed under arithmetical definability and contains 0(ω) the set of all (Gödel numbers of) true arithmetical sentences.

Some results related to definability of sets of integers in elementary extensions of ω are included.
Possible behaviours for the Mitchell ordering II
Authors: Cummings James
Published: May 2006

We analyse the Mitchell ordering in a model where κ is -hypermeasurable and > .
Ideals and combinatorial principles
Authors: Burke Douglas , Matsubara Yo
Published: May 2006

It is well known that if σ is a strongly compact cardinal and λ a regular cardinal ≥ σ, then for every stationary subset X of {α < λ: cof (α) = ω} there is some β < λ such that X ⋂ β is stationary in β. In fact the existence of a uniform, countably complete ultrafilter over λ is sufficient to prove the same conclusion about stationary subsets of {α < λ: cof (α) = ω}. See [13] or [10]. By analyzing the proof of this theorem as presented in [10], we realized the same conclusion will follow from the existence of a certain ideal, not necessarily prime, on . Throughout we will assume that σ is a regular uncountable cardinal and use the word “ideal” to mean fine ideal.
Completeness and decidability of tense logics closely related to logics above K4
Authors: Wolter Frank
Published: May 2006

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness (completeness) and decidability. It is proved that all minimal tense extensions of modal logics of finite width (in the sense of K. Kine) as well as all minimal tense extensions of cofinal subframe logics (in the sense of M. Zakharyaschev) are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions of these results are also presented.
The combinatorics of the splitting theorem
Authors: Kontostathis Kyriakos
Published: May 2006

The complexity of priority proofs in recursion theory has been growing since the first priority proofs in [1] and [11]. Refined versions of classic priority proofs can be found in [18]. To this date, this part of recursion theory is at about the same stage of development as real analysis was in the early days, when the notions of topology, continuity, compactness, vector space, inner product space, etc., were not invented. There were no general theorems involving these concepts to prove results about the real numbers and the proofs were repetitive and lengthy.

The priority method contains an unprecedent wealth of combinatorics which is used to answer questions in recursion theory and is bound to have applications in many other fields as well. Unfortunately, very little progress has been made in finding theorems to formulate the combinatorial part of the priority method so as to answer questions without having to reprove the combinatorics in each case.

Lempp and Lerman in [10] provide an overview of the subject. The entire edifice of definitions and theorems which formulate the combinatorics of the priority method has acquired the name Priority Theory. From a different vein, Groszek and Slaman in [2] have initiated a program to classify priority constructions in terms of how much induction or collection is needed to carry them out. This program studies the complexity of priority proofs and can be called Complexity Theory of Priority Proofs or simply Complexity.
Analytic cell decomposition and the closure of p-adic semianalytic sets
Authors: Liu Nianzheng
Published: May 2006

The p-adic semianalytic sets are defined, locally, as boolean combinations of sets of the form over the p-adic fields ℚp, where f is an analytic function. A well-know example due to Osgood showed the projection of a semianalytic set need not be a semianalytic set. We call those sets that are, locally, the projections of p-adic semianalytic sets p-adic subanalytic sets. The theory of p-adic subanalytic sets was presented by Denef and Van den Dries in [5]. The basic tools are the quantifier elimination techniques together with the ultrametric Weierstrass Preparation Theorem. Simultaneously with their developments of the p-adic subanalytic sets, they established some basic properties of p-adic semianalytic sets.

In this paper, we prove that the closure of any p-adic semianalytic set is also a semianalytic set. The analogous property for real semianalytic sets was proved in [12] and that for rigid semianalytic sets, informed by the referee, has been proved recently by a quite different method in [14] (cf. [9]). The keys to the proof are a separation lemma (Lemma 2) and an analytic cell decomposition theorem (Theorem 2) which is an analytic version of Denef's cell decomposition theorem (see [3, 4]; A total different form of anayltic cells appeared in [13]). The analytic cell decomposition theorem allows us to partition certain kinds of basic subsets into analytic cells that possess the closure property (see §1 for the definition).
Superatomic Boolean algebras constructed from morasses
Authors: Koepke Peter , Martínez Juan Carlos
Published: May 2006

By using the notion of a simplified (κ, 1)-morass, we construct κ-thin-tall, κ-thin-thick and, in a forcing extension, κ-very thin-thick superatomic Boolean algebras for every infinite regular cardinal κ.
Tailoring recursion for complexity
Authors: Grädel Erich , Gurevich Yuri
Published: May 2006

We design functional algebras that characterize various complexity classes of global functions. For this purpose, classical schemata from recursion theory are tailored for capturing complexity. In particular we present a functional analog of first-order logic and describe algebras of the functions computable in nondeterministic logarithmic space, deterministic and nondeterministic polynomial time, and for the functions computable by AC1 -circuits.
Intuitionistic sets and ordinals
Authors: Taylor Paul
Published: May 2006

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.

We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.

Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.

We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.

The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area.

Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy.

Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.
A definable continuous rank for nonmultidimensional superstable theories
Authors: Chowdhury Ambar , Loveys James , Tanović Predrag
Published: May 2006

Pillay studied nonmultidimensional superstable theories in [8], among other things defining a certain hierarchy of regular types in terms of which all other types may be analysed. Using this hierarchy, he showed that after naming a suitable ‘base’ of parameters, there are j-constructible (hence locally atomic) models over arbitrary sets (see Section 2 for definitions). It is asked at the end of [8] whether the parameter set can be removed. On a different note, it has been known for some time that in nonmultidimensional superstable theories, R∞-rank is definable for formulas having finite rank (see for example [9]). Definability of R∞-rank has had various applications in the literature, and so it is natural to ask whether the restriction to finite rank is necessary. In this paper we do not quite answer this question, but instead use Pillay's analysis to establish the existence of a ‘new’ continuous rank (the original idea for which is due to Tanović) which is defined on all complete types, reflects forking as does R∞-rank and satisfies certain definability properties.
Analytic equivalence relations and Ulm-type classifications
Authors: Hjorth Greg , Kechris Alexander S.
Published: May 2006

Our main goal in this paper is to establish a Glimm-Effros type dichotomy for arbitrary analytic equivalence relations.

The original Glimm-Effros dichotomy, established by Effros [Ef], [Ef1], who generalized work of Glimm [G1], asserts that if an Fσ equivalence relation on a Polish space X is induced by the continuous action of a Polish group G on X, then exactly one of the following alternatives holds:

(I) Elements of X can be classified up to E-equivalence by “concrete invariants” computable in a reasonably definable way, i.e., there is a Borel function f: X → Y, Y a Polish space, such that xEy ⇔ f(x) = f(y), or else

(II) E contains a copy of a canonical equivalence relation which fails to have such a classification, namely the relation xE0y ⇔ ∃n∀m ≥ n(x(n) = y(n)) on the Cantor space 2ω (ω = {0,1,2, …}), i.e., there is a continuous embedding g: 2ω → X such that xE0y ⇔ g(x)Eg(y).

Moreover, alternative (II) is equivalent to:

(II)′ There exists an E-ergodic, nonatomic probability Borel measure on X, where E-ergodic means that every E-invariant Borel set has measure 0 or 1 and E-nonatomic means that every E-equivalence class has measure 0.
On a generalization of distributivity
Authors: Kanai Yasuo
Published: May 2006

In this paper, we generalize the notion of distributivity and consider some properties of distributive ideals, that is, ideals I such that the algebra P(κ)/I is distributive in our sense.

Our notation and terminology is explained in §1, while the main results of this paper begin in §2. We shall show here some relations of the distributivity and the ideal theoretic partitions. In §3, we shall study the class of distributive ideals over κ whose existence is equivalent to the ineffability of κ, and other classes. Finally, in §4, we shall consider the equivalence of the Boolean prime ideal theorem and show that the existence of certain distributive ideals characterizes several large cardinals. As a byproduct, we can give a simple proof of Ketonen's theorem that κ is strongly compact if and only if for any regular cardinal λ ≥ κ there exists a nontrivial κ-complete prime ideal over λ.
Cut-elimination for simple type theory with an axiom of choice
Authors: Mints G.
Published: May 2006

We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.
Generalized cohesiveness
Authors: Hummel Tamara , Jockusch Carl G.
Published: May 2006

We study some generalized notions of cohesiveness which arise naturally in connection with effective versions of Ramsey's Theorem. An infinite set A of natural numbers is n-cohesive (respectively, n-r-cohesive) if A is almost homogeneous for every computably enumerable (respectively, computable) 2-coloring of the n-element sets of natural numbers. (Thus the 1-cohesive and 1-r-cohesive sets coincide with the cohesive and r-cohesive sets, respectively.) We consider the degrees of unsolvability and arithmetical definability levels of n-cohesive and n-r-cohesive sets. For example, we show that for all n ≥ 2, there exists a n-cohesive set. We improve this result for n = 2 by showing that there is a 2-cohesive set. We show that the n-cohesive and n-r-cohesive degrees together form a linear, non-collapsing hierarchy of degrees for n ≥ 2. In addition, for n ≥ 2 we characterize the jumps of n-cohesive degrees as exactly the degrees ≥ 0(n+1) and also characterize the jumps of the n-r-cohesive degrees.
Unions of rectifiable curves in Euclidean space and the covering number of the meagre ideal
Authors: Steprāns Juris
Published: May 2006

To any metric space it is possible to associate the cardinal invariant corresponding to the least number of rectifiable curves in the space whose union is not meagre. It is shown that this invariant can vary with the metric space considered, even when restricted to the class of convex subspaces of separable Banach spaces. As a corollary it is obtained that it is consistent with set theory that any set of reals of size ℵ1 is meagre yet there are ℵ1 rectifiable curves in ℝ3 whose union is not meagre. The consistency of this statement when the phrase “rectifiable curves” is replaced by “straight lines” remains open.
A finite basis theorem for residually finite, congruence meet-semidistributive varieties
Authors: Willard Ross
Published: May 2006

We derive a Mal'cev condition for congruence meet-semidistributivity and then use it to prove two theorems. Theorem A: if a variety in a finite language is congruence meet-semidistributive and residually less than some finite cardinal, then it is finitely based. Theorem B: there is an algorithm which, given m < ω and a finite algebra in a finite language, determines whether the variety generated by the algebra is congruence meet-semidistributive and residually less than m.
Arithmetical representations of Brownian motion I
Authors: Fouché Willem
Published: May 2006

We discuss ways in which a typical one-dimensional Brownian motion can be approximated by oscillations which are encoded by finite binary strings of high descriptive complexity. We study the recursive properties of Brownian motions that can be thus obtained.
Doughnuts, floating ordinals, square brackets, and ultraflitters
Authors: Prisco Carlos A. Di , Henle James M.
Published: May 2006

In this paper, we study partition properties of the set of real numbers. The meaning of “set of real numbers” will vary, referring at times to the collection of sequences of natural numbers, ωω; the collection of infinite sets of natural numbers [ω]ω; the collection of infinite sequences of zeroes and ones, 2ω; or (ω), the power set of ω.

The archetype for the relations is the property: “all sets of reals are Ramsey,” in the notation of Erdős and Hajnal, ω → (ω)ω. This states that for every partition F : [ω]ω → 2, there is an infinite set H ∈ [ω]ω such that F is constant on [H]ω. Like virtually all of the properties we will discuss, it contradicts the Axiom of Choice but is compatible with the principle of dependent choices (DC). DC will be used throughout the paper wihtout further mention.

The properties discussed in this paper will vary in two respects. Some, like ω → (ω)ω, will be incompatible with the existence of an ultrafilter on ω (UF) and some will not. Some are known to be consistent relative to ZF alone, and for some, such as ω → (ω)ω, the question is still open. All properties, however, are true in Solovay's model and hence are consistent relative to Con(ZF + “there exists an inaccessible cardinal”).
Laver sequences for extendible and super-almost-huge cardinals
Authors: Corazza Paul
Published: May 2006

Versions of Laver sequences are known to exist for supercompact and strong cardinals. Assuming very strong axioms of infinity, Laver sequences can be constructed for virtually any globally defined large cardinal not weaker than a strong cardinal; indeed, under strong hypotheses. Laver sequences can be constructed for virtually any regular class of embeddings. We show here that if there is a regular class of embeddings with critical point κ, and there is an inaccessible above κ, then it is consistent for there to be a regular class that admits no Laver sequence. We also show that extendible cardinals are Laver-generating, i.e., that assuming only that κ is extendible, there is an extendible Laver sequence at κ. We use the method of proof to answer a question about Laver-closure of extendible cardinals at inaccessibles. Finally, we consider Laver sequences for super-almost-huge cardinals. Assuming slightly more than super-almost-hugeness, we show that there are super-almost-huge Laver sequences, improving the previously known upper bound for such Laver sequences. We also describe conditions under which the canonical construction of a Laver sequence fails for super-almost-huge cardinals.
Flat Morley sequences
Authors: Newelski Ludomir
Published: May 2006

AssumeTis a small superstable theory. We introduce the notion of a flat Morley sequence, which is a counterpart of the notion of an infinite Morley sequence in a typep, in case whenpis a complete type over a finite set of parameters. We show that for any flat Morley sequenceQthere is a modelMofTwhich isτ-atomic over {Q}. When additionallyThas few countable models and is 1-based, we prove that withinMthere is an infinite Morley sequenceI, withI⊂ dcl(Q), such thatMis prime overI.
Finite powers of strong measure zero sets
Authors: Scheepers Marion
Published: May 2006

In a previous paper—[17]—we characterized strong measure zero sets of reals in terms of a Ramseyan partition relation on certain subspaces of the Alexandroff duplicate of the unit interval. This framework gave only indirect access to the relevant sets of real numbers. We now work more directly with the sets in question, and since it costs little in additional technicalities, we consider the more general context of metric spaces and prove:

1. If a metric space has a covering property of Hurewicz and has strong measure zero, then its product with any strong measure zero metric space is a strong measure zero metric space (Theorem 1 and Lemma 3).

2. A subspaceXof a σ-compact metric spaceYhas strong measure zero if, and only if, a certain Ramseyan partition relation holds forY(Theorem 9).

3. A subspaceXof a σ-compact metric spaceYhas strong measure zero in all finite powers if, and only if, a certain Ramseyan partition relation holds forY(Theorem 12).

Then 2 and 3 yield characterizations of strong measure zeroness for σ-totally bounded metric spaces in terms of Ramseyan theorems.
Rectangular games
Authors: Venema Yde
Published: May 2006

We prove that every rectangularly dense diagonal-free cylindric algebra is representable. As a corollary, we give finite, sound and complete axiomatizations for the finite-variable fragments of first order logic without equality and for multi-dimensional modal S5-logic.
Undecidability of the real-algebraic structure of models of intuitionistic elementary analysis
Authors: Erdélyi-Szabó Miklós
Published: May 2006

We show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.
On quantification with a finite universe
Authors: Shelah Saharon
Published: May 2006

We consider a finite universe (more exactly—a family of them), second order quantifiers QK, where for each this means quantifying over a family of n(K)-place relations closed under permuting . We define some natural orders and shed some light on the classification problem of those quantifiers.
Stationary sets and infinitary logic
Authors: Shelah Saharon , Väänänen Jouko
Published: May 2006

Let be the class of structures 〈λ, <, A〉, where A ⊆ λ is disjoint from a club, and let be the class of structures 〈λ, <, A), where A ⊆ λ contains a club. We prove that if λ = λ<κ is regular, then no sentence of Lλ + κ separates and On the other hand, we prove that if λ = μ+ , μ = μ<μ, and a forcing axiom holds (and if μ = ℵ0), then there is a sentence of Lλλ which separates and .
Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic
Authors: Dekkers Wil , Bunder Martin , Barendregt Henk
Published: May 2006

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, [3], we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions.
Effective presentability of Boolean algebras of Cantor-Bendixson rank 1
Authors: Downey Rod , Jockusch Carl G.
Published: May 2006

We show that there is a computable Boolean algebra and a computably enumerable ideal I of such that the quotient algebra /I is of Cantor-Bendixson rank 1 and is not isomorphic to any computable Boolean algebra. This extends a result of L. Feiner and is deduced from Feiner's result even though Feiner's construction yields a Boolean algebra of infinite Cantor-Bendixson rank.
Infinitary properties of valued and ordered vector spaces
Authors: Kuhlmann Salma
Published: May 2006

§1. Introduction.The motivation of this work comes from two different directions: infinite abelian groups, and ordered algebraic structures. A challenging problem in both cases is that of classification. In the first case, it is known for example (cf. [KA]) that the classification of abelian torsion groups amounts to that of reducedp-groups by numerical invariants called theUlm invariants(given by Ulm in [U]). Ulm's theorem was later generalized by P. Hill to the class of totally projective groups. As to the second case, let us consider for instance the class of divisible ordered abelian groups. These may be viewed as ordered ℚ-vector spaces. Their theory being unstable, we cannot hope to classify them by numerical invariants. On the other hand, being o-minimal, the theory enjoys several good model theoretic properties (cf. [P-S]), so the search for some reasonable invariants is well motivated. The common denominator of the two cases, as well as of many others, is valuation theory. Indeed given an ordered vector space, one can consider it as a valued vector space, endowed with the natural valuation. Also, the socleG[p] of a reduced abelianp-groupG, endowed with the height functionhG, is a valued vector space over(the prime field of characteristicp) with values in the ordinals (cf. [F]).
The complexity of decision procedures in relevance logic II
Authors: Urquhart Alasdair
Published: May 2006

In this paper, we show that there is no primitive recursive decision procedure for the implication-conjunction fragments of the relevant logics R, E and T, as well as for a family of related logics. The lower bound on the complexity is proved by combining the techniques of an earlier paper on the same subject [20] with a method used by Lincoln, Mitchell, Scedrov and Shankar in proving that propositional linear logic is undecidable.

The decision problem for the pure implicational fragments of E and R were solved by Saul Kripke in a tour de force of combinatorial reasoning, published only as an abstract [9]. Belnap and Wallace extended Kripke's decision procedure to the implication-negation fragment of E in [3]; an account of their decision method is to be found in [1, pp. 124–139]. The decision method extends immediately to the implication/negation fragment of R. In fact, in the case of R we can go farther: Meyer in his thesis [13] showed how to translate the logic LR, which results from R by omitting the distribution axiom, into R→⋀, so that the decision procedure can be extended to all of LR. This decision procedure has been implemented as a program Kripke by Thistlewaite, McRobbie and Meyer [17]. The program is not simply a straightforward implementation of the decision procedure; finite matrices are used extensively to prune invalid nodes from the search tree.
The logic of recursive equations
Authors: Hurkens A. J. C. , McArthur Monica , Moschovakis Yiannis N. , Moss Lawrence S. , Whitney Glen T.
Published: May 2006

We study logical systems for reasoning about equations involving recursive definitions. In particular, we are interested in “propositional” fragments of the functional language of recursion FLR [18, 17], i.e., without the value passing or abstraction allowed in FLR. The “pure,” propositional fragment FLR0 turns out to coincide with the iteration theories of [1]. Our main focus here concerns the sharp contrast between the simple class of valid identities and the very complex consequence relation over several natural classes of models.
On the strength of Ramsey's theorem for pairs
Authors: Cholak Peter A. , Jockusch Carl G. , Slaman Theodore A.
Published: May 2006

We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RTkndenote Ramsey's theorem fork–colorings ofn–element sets, and let RT<∞ndenote (∀k)RTkn. Our main result on computability is: For anyn≥ 2 and any computable (recursive)k–coloring of then–element sets of natural numbers, there is an infinite homogeneous setXwithX″ ≤T0(n). LetIΣnandBΣndenote the Σninduction and bounding schemes, respectively. Adapting the casen= 2 of the above result (whereXis low2) to models of arithmetic enables us to show that RCA0+IΣ2+ RT22is conservative over RCA0+IΣ2for Π11statements and that RCA0+IΣ3+ RT<∞2is Π11-conservative over RCA0+IΣ3. It follows that RCA0+ RT22does not implyBΣ3. In contrast, J. Hirst showed that RCA0+ RT<∞2does implyBΣ3, and we include a proof of a slightly strengthened version of this result. It follows that RT<∞2is strictly stronger than RT22overRCA0.
Hyperimaginaries and automorphism groups
Authors: Lascar D. , Pillay A.
Published: May 2006

A hyperimaginary is an equivalence class of a type-definable equivalence relation on tuples of possibly infinite length. The notion was recently introduced in [1], mainly with reference to simple theories. It was pointed out there how hyperimaginaries still remain in a sense within the domain of first order logic. In this paper we are concerned with several issues: on the one hand, various levels of complexity of hyperimaginaries, and when hyperimaginaries can be reduced to simpler hyperimaginaries. On the other hand the issue of what information about hyperimaginaries in a saturated structure M can be obtained from the abstract group Aut(M).

In Section 2 we show that if T is simple and canonical bases of Lascar strong types exist in Meq then hyperimaginaries can be eliminated in favour of sequences of ordinary imaginaries. In Section 3, given a type-definable equivalence relation with a bounded number of classes, we show how the quotient space can be equipped with a certain compact topology. In Section 4 we study a certain group introduced in [5], which we call the Galois group of T, develop a Galois theory and make the connection with the ideas in Section 3. We also give some applications, making use of the structure of compact groups. One of these applications states roughly that bounded hyperimaginaries can be eliminated in favour of sequences of finitary hyperimaginaries. In Sections 3 and 4 there is some overlap with parts of Hrushovski's paper [2].
Pure type systems with more liberal rules
Authors: Bunder Martin , Dekkers Wil
Published: May 2006

Pure Type Systems. PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic.

First we consider a simplification of the start and weakening rules of PTSs. which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems.

A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications.
On tarski on models
Authors: Bays Timothy
Published: May 2006

This paper concerns Tarski's use of the term “model” in his 1936 paper “On the Concept of Logical Consequence.” Against several of Tarski's recent defenders. I argue that Tarski employed a non-standard conception of models in that paper. Against Tarski's detractors. I argue that this nonstandard conception is more philosophically plausible than it may appear. Finally, I make a few comments concerning the traditionally puzzling case of Tarski's ω-rule example.
Exchange rules
Authors: Piazza Mario
Published: May 2006

In this paper, we show by a proof-theoretical argument that in a logic without structural rules, that is in noncommutative linear logic with exponentials, every formula A for which exchange rules (and weakening and contraction as well) are admissible is provably equivalent to? A. This property shows that the expressive power of “noncommutative exponentials” is much more important than that of “commutative exponentials”.
On the structures inside truth-table degrees
Authors: Stephan Frank
Published: May 2006

The following theorems on the structure inside nonrecursive truth-table degrees are established: Dëgtev's result that the number of bounded truth-table degrees inside a truth-table degree is at least two is improved by showing that this number is infinite. There are even infinite chains and antichains of bounded truth-table degrees inside every truth-table degree. The latter implies an affirmative answer to the following question of Jockusch: does every truth-table degree contain an infinite antichain of many-one degrees? Some but not all truth-table degrees have a least bounded truth-table degree. The technique to construct such a degree is used to solve an open problem of Beigel, Gasarch and Owings: there are Turing degrees (constructed as hyperimmune-free truth-table degrees) which consist only of 2-subjective sets and therefore do not contain any objective set. Furthermore, a truth-table degree consisting of three positive degrees is constructed where one positive degree consists of enumerable semirecursive sets, one of coenumerable semirecursive sets and one of sets, which are neither enumerable nor coenumerable nor semirecursive. So Jockusch's result that there are at least three positive degrees inside a truth-table degree is optimal. The number of positive degrees inside a truth-table degree can also be some other odd integer as for example nineteen, but it is never an even finite number.
A model complete theory of valued D-fields
Authors: Scanlon Thomas
Published: May 2006

The notion of a D-ring, generalizing that of a differential or a differenee ring, is introduced, Quantifier elimination and a version of the Ax—Kochen—Eršov principle is proven for a theory of valued D-fields of residual characteristic zero.
Interpreting classical theories in constructive ones
Authors: Avigad Jeremy
Published: May 2006

A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
Number systems with simplicity hierarchies: a generalization of Conway's theory of surreal numbers
Authors: Ehrlich Philip
Published: May 2006

Introduction. In his monograph On Numbers and Games [7], J. H. Conway introduced a real-closed field containing the reals and the ordinals as well as a great many other numbers including ω, ω, /2, 1/ω, and ω − π to name only a few. Indeed, this particular real-closed field, which Conway calls No, is so remarkably inclusive that, subject to the proviso that numbers—construed here as members of ordered “number” fields—be individually definable in terms of sets of von Neumann-Bernays-Gödel set theory with Global Choice, henceforth NBG [cf. 21, Ch. 4], it may be said to contain “All Numbers Great and Small.” In this respect, No bears much the same relation to ordered fields that the system of real numbers bears to Archimedean ordered fields. This can be made precise by saying that whereas the ordered field of reals is (up to isomorphism) the unique homogeneous universal Archimedean ordered field, No is (up to isomorphism) the unique homogeneous universal orderedfield [14]; also see [10], [12], [13].

However, in addition to its distinguished structure as an ordered field, No has a rich hierarchical structure that (implicitly) emerges from the recursive clauses in terms of which it is defined. This algebraico-tree-theoretic structure, or simplicity hierarchy, as we have called it [15], depends upon No's (implicit) structure as a lexicographically ordered binary tree and arises from the fact that the sums and products of any two members of the tree are the simplest possible elements of the tree consistent with No's structure as an ordered group and an ordered field, respectively, it being understood that x is simpler than y just in case x is a predecessor of y in the tree.
Forbidden subgraphs and forbidden substructures
Authors: Cherlin Gregory , Shi Niandong
Published: May 2006

The problem of the existence of a universal structure omitting a finite set of forbidden substructures is reducible to the corresponding problem in the category of graphs with a vertex coloring by two colors. It is not known whether this problem reduces further to the category of ordinary graphs. It is also not known whether these problems are decidable.
Expansion of a model of a weakly o-minimal theory by a family of unary predicates
Authors: Baizhanov Bektur Sembiuly
Published: May 2006

A subsetA⊆Mof a totally ordered structureMis said to beconvex, if for anya, b∈A: [a<b→ ∀t(a<tb→t∈A)]. A complete theory of first order isweakly o-minimal(M. Dickmann [D]) if any modelMis totally ordered by some ∅-definable formula and any subset ofMwhich is definable with parameters fromMis a finite union of convex sets. We prove here that for any modelMof a weakly o-minimal theoryT. any expansionM+ofMby a family of unary predicates has a weakly o-minimal theory iff the set of all realizations of each predicate is a union of a finite number of convex sets (Theorem 63). that solves the Problem of Cherlin-Macpherson-Marker-Steinhorn [MMS] for the class of weakly o-minimal theories.
Understanding theChallengerDisaster: Organizational Structure and the Design of Reliable Systems
Authors: Heimann C. F. Larry
Published: May 2006

The destruction of the space shuttleChallengerwas a tremendous blow to American space policy. To what extent was this loss the result of organizational factors at the National Aeronautics and Space Administration? To discuss this question analytically, we need a theory of organizational reliability and agency behavior. Martin Landau's work on redundancy and administrative performance provides a good starting point for such an effort. Expanding on Landau's work, I formulate a more comprehensive theory of organizational reliability that incorporates both type I and type II errors. These principles are then applied in a study of NASA and its administrative behavior before and after theChallengeraccident.
The Measurement and Motivation of Atypical Opinion in a Certain Group
Authors: Allport Floyd H. , Hartman D. A.
Published: May 2006

Terms denoting political attitudes, such as ‘conservative,’ ‘liberal,’ ‘radical,’ and ‘reactionary,’ have long been familiar both in popular usage and in the language of political science. Though sufficiently understood for ordinary discourse, their use is likely to lead to a confusion between a political opinion and the type of person who holds the opinion. There is considerable agreement as to what is meant by a radical view; but is there such a thing as a radical type of personality? If there is, we need a method for the measurement and identification of such individuals. If not (and psychologists are becoming increasingly suspicious of type classifications), we must ask what psychological characteristics in individuals are the most likely to produce a radical trend in political and social convictions. The same observation holds for the other familiar attitudes upon public questions.

A logical procedure would seem to be, first, to measure the distribution of public opinion in a representative sample, and secondly, to select from the various regions of this distribution (conservative, radical, and the like) a sufficient number of individuals for detailed study of the motives and traits of their personalities which give rise to the opinions they hold. This paper will be devoted to a preliminary report on the results of such a study.
Enhancing Democracy Through Legislative Redistricting
Authors: Gelman Andrew , King Gary
Published: May 2006

We demonstrate the surprising benefits of legislative redistricting (including partisan gerrymandering) for American representative democracy. In so doing, our analysis resolves two long-standing controversies in American politics. First, whereas some scholars believe that redistricting reduces electoral responsiveness by protecting incumbents, others, that the relationship is spurious, we demonstrate that both sides are wrong: redistricting increases responsiveness. Second, while some researchers believe that gerrymandering dramatically increases partisan bias and others deny this effect, we show both sides are in a sense correct. Gerrymandering biases electoral systems in favor of the party that controls the redistricting as compared to what would have happened if the other party controlled it, but any type of redistricting reduces partisan bias as compared to an electoral system without redistricting. Incorrect conclusions in both literatures resulted from misjudging the enormous uncertainties present during redistricting periods, making simplified assumptions about the redistricters' goals, and using inferior statistical methods.
The Nature of Congressional Committee Jurisdictions
Authors: King David C.
Published: May 2006

Jurisdictions are the defining characteristics of committee systems, and they are central in any discussions about the U. S. Congress; yet we know little about them. Where do committee property rights come from? Are they rigid? Are they flexible? I introduce a distinction between statutory jurisdictions (which are written in the House and Senate Rules) and common law jurisdictions (which emerge through bill referral precedents). Turf is gained through common law advances, not through formal rules changes (like the “reforms” passed by the House in 1946, 1974, and 1980). Jurisdictional change is ongoing and incremental. The analysis draws on an examination of hearings held by the House Commerce Committee from 1947 through 1990.
The Presthus Debacle: Intraparty Politics and Bargaining Failure in Norway
Authors: Strøm Kaare
Published: May 2006

Bargaining failure has been neglected in the study of interparty coalitions. I examine the unsuccessful attempt by three Norwegian nonsocialist parties to defeat a Labor party minority government in June 1987 when the majority opposition twice failed to agree on a simple vote to that end. This failure of coalition bargaining was facilitated by incomplete information, intraparty constraints and misdelegation of authority, and by anticipation of the impending parliamentary recess. Despite these complexities, simple noncooperative games like the war of attrition can shed considerable light on this and other unsuccessful negotiations. The “Presthus debacle” demonstrates that political parties bring many different objectives to the bargaining table and that the trade-offs between these objectives vary according to organizational and institutional conditions.
Individual and Contextual Variations in Political Candidate Appraisal
Authors: Rahn Wendy M. , Aldrich John H. , Borgida Eugene
Published: May 2006

In this note we elaborate on the conditions under which on-line and memory-based strategies of political candidate evaluation can be implemented. We suggest that the structure of information may be an important contextual variable affecting the voter's choice of these strategies. In addition, we propose that citizens with less political sophistication are particularly sensitive to structural differences in the political information environment. We use an experimental design that manipulates the information-processing context to test these ideas. Our results suggest that the context in which information is presented plays a critical role in moderating the influence of individual differences in political sophistication.