bluuebunny/crossref_metadata_2025_split huggingface dataset:
Hilbert's program and the omega-rule
Authors: Ignjatović Aleksandar 
Published: May 2006

AbstractIn 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

AbstractWe 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

AbstractAn 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.
Forcing disabled
Authors: Stanley M. C. 
Published: May 2006

AbstractIt 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

AbstractWe 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

AbstractWe 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].
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

AbstractAn 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

AbstractWe 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.
A construction of superstable ndop-notop groups
Authors: Baudisch Andreas 
Published: May 2006

AbstractThe 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

AbstractIt 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

AbstractIt 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

AbstractThe 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 sequentsConsidering 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

AbstractWe 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

AbstractIn 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, and2. 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 that1′. 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.
The Sacks density theorem and Σ2-bounding
Authors: Groszek Marcia J. , Mytilinaios Michael E. , Slaman Theodore A. 
Published: May 2006

AbstractThe 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.
Canonical forms for definable subsets of algebraically closed and real closed valued fields
Authors: Holly Jan E. 
Published: May 2006

AbstractWe 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.