bluuebunny/crossref_metadata_2025_split huggingface dataset:
Randomness and Computability: Open Questions
Authors: Miller Joseph S. , Nies André 
Published: December 2007

It is time for a new paper about open questions in the currently very active area of randomness and computability. Ambos-Spies and Kučera presented such a paper in 1999 [1]. All the question in it have been solved, except for one: is KL-randomness different from Martin-Löf randomness? This question is discussed in Section 6.Not all the questions are necessarily hard—some simply have not been tried seriously. When we think a question is a major one, and therefore likely to be hard, we indicate this by the symbol ▶, the criterion being that it is of considerable interest and has been tried by a number of researchers. Some questions are close contenders here; these are marked by ▷. With few exceptions, the questions are precise. They mostly have a yes/no answer. However, there are often more general questions of an intuitive or even philosophical nature behind. We give an outline, indicating the more general questions.All sets will be sets of natural numbers, unless otherwise stated. These sets are identified with infinite strings over {0, 1}. Other terms used in the literature are sequence and real.
Calibrating Randomness
Authors: Downey Rod , Hirschfeldt Denis R. , Nies André , Terwijn Sebastiaan A. 
Published: December 2007

We report on some recent work centered on attempts to understand when one set is more random than another. We look at various methods of calibration by initial segment complexity, such as those introduced by Solovay [125], Downey, Hirschfeldt, and Nies [39], Downey, Hirschfeldt, and LaForte [36], and Downey [31]; as well as other methods such as lowness notions of Kučera and Terwijn [71], Terwijn and Zambella [133], Nies [101, 100], and Downey, Griffiths, and Reid [34]; higher level randomness notions going back to the work of Kurtz [73], Kautz [61], and Solovay [125]; and other calibrations of randomness based on definitions along the lines of Schnorr [117].These notions have complex interrelationships, and connections to classical notions from computability theory such as relative computability and enumerability. Computability figures in obvious ways in definitions of effective randomness, but there are also applications of notions related to randomness in computability theory. For instance, an exciting by-product of the program we describe is a more-or-less naturalrequirement-freesolution to Post's Problem, much along the lines of the Dekker deficiency set.
Internal Consistency and the Inner Model Hypothesis
Authors: Friedman Sy-David 
Published: December 2007

There are two standard ways to establish consistency in set theory. One is to prove consistency using inner models, in the way that Gödel proved the consistency of GCH using the inner model L. The other is to prove consistency using outer models, in the way that Cohen proved the consistency of the negation of CH by enlarging L to a forcing extension L[G].But we can demand more from the outer model method, and we illustrate this by examining Easton's strengthening of Cohen's result:Theorem 1 (Easton's Theorem). There is a forcing extensionL[G] of L in which GCH fails at every regular cardinal.Assume that the universe V of all sets is rich in the sense that it contains inner models with large cardinals. Then what is the relationship between Easton's model L[G] and V? In particular, are these models compatible, in the sense that they are inner models of a common third model? If not, then the failure of GCH at every regular cardinal is consistent only in a weak sense, as it can only hold in universes which are incompatible with the universe of all sets. Ideally, we would like L[G] to not only be compatible with V, but to be an inner model of V.We say that a statement is internally consistent iff it holds in some inner model, under the assumption that there are innermodels with large cardinals.
Inner Models and Ultrafilters In L(ℝ)
Authors: Neeman Itay 
Published: December 2007

AbstractWe present a characterization of supercompactness measures for ω1 in L(ℝ), and of countable products of such measures, using inner models. We give two applications of this characterization, the first obtaining the consistency of with ZFC+ADL(ℝ), and the second proving the uniqueness of the supercompactness measure over in L(ℝ) for .
Fragment of Nonstandard Analysis with a Finitary Consistency Proof
Authors: Rössler Michal , Jeřábek Emil 
Published: December 2007

AbstractWe introduce a nonstandard arithmetic NQA− based on the theory developed by R. Chuaqui and P. Suppes in [2] (we will denote it by NQA+), with a weakened external open minimization schema. A finitary consistency proof for NQA− formalizable in PRA is presented. We also show interesting facts about the strength of the theories NQA−and NQA+; NQA−is mutually interpretable with IΔ0 + EXP, and on the other hand, NQA+interprets the theories IΣ1 and WKL0.
On the Equimorphism Types of Linear Orderings
Authors: Montalbán Antonio 
Published: December 2007

§1. Introduction. A linear ordering (also known astotal ordering) embedsinto another linear ordering if it is isomorphic to a subset of it. Two linear orderings are said to beequimorphicif they can be embedded in each other. This is an equivalence relation, and we call the equivalence classesequimorphism types. We analyze the structure of equimorphism types of linear orderings, which is partially ordered by the embeddability relation. Our analysis is mainly fromthe viewpoints of Computability Theory and Reverse Mathematics. But we also obtain results, as the definition of equimorphism invariants for linear orderings, which provide a better understanding of the shape of this structure in general.This study of linear orderings started by analyzing the proof-theoretic strength of a theorem due to Jullien [Jul69]. As is often the case in Reverse Mathematics, to solve this problem it was necessary to develop a deeper understanding of the objects involved. This led to a variety of results on the structure of linear orderings and the embeddability relation on them. These results can be divided into three groups.
In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
Authors: von Plato Jan 
Published: December 2007

AbstractThe Löwenheim–Skolem theorem was published in Skolem's long paper of 1920, with the first section dedicated to the theorem. The second section of the paper contains a proof-theoretical analysis of derivations in lattice theory. The main result, otherwise believed to have been established in the late 1980s, was a polynomial-time decision algorithm for these derivations. Skolem did not develop any notation for the representation of derivations, which makes the proofs of his results hard to follow. Such a formal notation is given here by which these proofs become transparent. A third section of Skolem's paper gives an analysis for derivations in plane projective geometry. To clear a gap in Skolem's result, a new conservativity property is shown for projective geometry, to the effect that a proper use of the axiom that gives the uniqueness of connecting lines and intersection points requires a conclusion with proper cases (logically, a disjunction in a positive part) to be proved.The forgotten parts of Skolem's first paper on the Löwenheim–Skolem theorem are the perhaps earliest combinatorial analyses of formal mathematical proofs, and at least the earliest analyses with profound results.
Local Definitions in Degree Structures: The Turing Jump, Hyperdegrees and Beyond
Authors: Shore Richard A. 
Published: December 2007

AbstractThere are Π5 formulas in the language of the Turing degrees, D, with ≤, ⋁ and ⋀, that define the relations x″ ≤ y″, x″ = y″ and so x ∈ L2(y) = {x ≥ y ∣ x″ = y″} in any jump ideal containing 0(ω). There are also Σ6 & Π6 and Π8 formulas that define the relations w = x″ and w = x′, respectively, in any such ideal I. In the language with just ≤ the quantifier complexity of each of these definitions increases by one. On the other hand, no Π2 or Σ2 formula in the language with just ≤ defines L2 or x ∈ L2(y). Our arguments and constructions are purely degree theoretic without any appeals to absoluteness considerations, set theoretic methods or coding of models of arithmetic. As a corollary, we see that every automorphism of I is fixed on every degree above 0″ and every relation on I that is invariant under double jump or joining with 0″ is definable over I if and only if it is definable in second order arithmetic with set quantification ranging over sets whose degrees are in I. Similar direct coding arguments show that every hyperjump ideal I is rigid and biinterpretable with second order arithmetic with set quantification ranging over sets with hyperdegrees in I. Analogous results hold for various coarser degree structures.
Relating First-Order Set Theories and Elementary Toposes
Authors: Awodey Steve , Butz Carsten , Simpson Alex , Streicher Thomas 
Published: December 2007

AbstractWe show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo–Fraenkel set theory (IZF).
The cost of a cycle is a square
Authors: Carbone A. 
Published: December 2007

AbstractThe logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with (kn+1) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search.
An algebraic approach to categories of partial morphisms
Authors: Stefani S. T. 
Published: December 2007

AbstractIn the study of categories whose morphisms display a behaviour similar to that of partial functions, the concept of morphism domain is, obviously, central. In this paper an operation defined on morphisms describes those properties which are related to morphisms being regarded as abstractions of partial functions. This operation allows us to characterise the morphism domains directly, and gives rise to an algebra defined by a simple set of identities. No product-like categorical structures are needed therefore. We also develop the construction of topologies together with the notion of continuous morphism, in order to test the effectiveness of this approach. It is interesting to see how much of the computational character of the morphisms is translated into continuity.
A maximal bounded forcing axiom
Authors: Asperó David 
Published: December 2007

AbstractAfter presenting a general setting in which to look at forcing axioms, we give a hierarchy of generalized bounded forcing axioms that correspond level by level, in consistency strength, with the members of a natural hierarchy of large cardinals below a Mahlo. We give a general construction of models of generalized bounded forcing axioms. Then we consider the bounded forcing axiom for a class of partially ordered sets Γ1 such that, letting Γ0 be the class of all stationary-set-preserving partially ordered sets, one can prove the following:(a) Γ0 ⊆ Γ1,(b) Γ0 = Γ1 if and only if NSω1 is ℵ1-dense.(c) If P ∉ Γ1, then BFA({P}) fails.We call the bounded forcing axiom for Γ1Maximal Bounded Forcing Axiom (MBFA). Finally we prove MBFA consistent relative to the consistency of an inaccessible Σ2-correct cardinal which is a limit of strongly compact cardinals.
SN and CR for free-style LKtq: linear decorations and simulation of normalization
Authors: Joinet Jean-Baptiste , Schellinx Harold , De Falco Lorenzo Tortora 
Published: December 2007

AbstractThe present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.
On essentially low, canonically well-generated Boolean algebras
Authors: Bonnet Robert , Rubin Matatyahu 
Published: December 2007

AbstractLet B be a superatomic Boolean algebra (BA). The rank of B (rk(B)). is defined to be the Cantor Bendixon rank of the Stone space of B. If a ∈ B − {0}, then the rank of a in B (rk(a)). is defined to be the rank of the Boolean algebra . The rank of 0B is defined to be −1. An element a ∈ B − {0} is a generalized atom , if the last nonzero cardinal in the cardinal sequence of B ↾ a is 1. Let a, b ∈ . We denote a ˜ b, if rk(a) = rk(b) = rk(a · b). A subset H ⊆ is a complete set of representatives (CSR) for B, if for every a there is a unique h ∈ H such that h ~ a. Any CSR for B generates B. We say that B is canonically well-generated (CWG), if it has a CSR H such that the sublattice of B generated by H is well-founded. We say that B is well-generated, if it has a well-founded sublattice L such that L generates B.Theorem 1. Let B be a Boolean algebra with cardinal sequence . If B is CWG, then every subalgebra of B is CWG.A superatomic Boolean algebra B is essentially low (ESL), if it has a countable ideal I such that rk(B/I) ≤ 1.Theorem 1 follows from Theorem 2.9. which is the main result of this work. For an ESL BA B we define a set FB of partial functions from a certain countably infinite set to ω (Definition 2.8). Theorem 2.9 says that if B is an ESL Boolean algebra, then the following are equivalent.(1) Every subalgebra of B is CWG: and(2) FB is bounded.Theorem 2. If an ESL Boolean algebra is not CWG, then it has a subalgebra which is not well-generated.
Complexity of interpolation and related problems in positive calculi
Authors: Maksimova Larisa 
Published: December 2007

AbstractWe consider the problem of recognizing important properties of logical calculi and find complexity bounds for some decidable properties. For a given logical systemL, a property P of logical calculi is called decidable overLif there is an algorithm which for any finite setAxof new axiom schemes decides whether the calculusL+Axhas the property P or not. In [11] the complexity of tabularity, pre-tabularity. and interpolation problems over the intuitionistic logic Int and over modal logic S4 was studied, also we found the complexity of amalgamation problems in varieties of Heyting algebras and closure algebras.In the present paper we deal with positive calculi. We prove NP-completeness of tabularity, DP-hardness of pretabularity and PSPACE-completeness of interpolation problem over Int+. In addition to above-mentioned properties, we consider Beth's definability properties. Also we improve some complexity bounds for properties of superintuitionistic calculi.
Pfaffian differential equations over exponential o-minimal structures
Authors: Miller Chris , Speissegger Patrick 
Published: December 2007

In this paper, we continue investigations into the asymptotic behavior of solutions of differential equations over o-minimal structures.Let ℜ be an expansion of the real field (ℝ, +, ·).A differentiable mapF= (F1,…,F1): (a, b) → ℝiisℜ-Pfaffianif there existsG: ℝ1+l→ ℝldefinable in ℜ such thatF′(t) =G(t, F(t)) for allt∈ (a, b) and each component functionGi: ℝ1+l→ ℝ is independent of the lastl−ivariables (i= 1, …,l). If ℜ is o-minimal andF: (a, b) → ℝlis ℜ-Pfaffian, then (ℜ,F) is o-minimal (Proposition 7). We say thatF: ℝ → ℝlis ultimately ℜ-Pfaffian if there existsr∈ ℝ such that the restrictionF↾(r, ∞) is ℜ-Pfaffian. (In general,ultimatelyabbreviates “for all sufficiently large positive arguments”.)The structure ℜ isclosed under asymptotic integrationif for each ultimately non-zero unary (that is, ℝ → ℝ) functionfdefinable in ℜ there is an ultimately differentiable unary functiongdefinable in ℜ such that limt→+∞[g′(t)/f(t)] = 1- If ℜ is closed under asymptotic integration, then ℜ is o-minimal and definesex: ℝ → ℝ (Proposition 2).Note that the above definitions make sense for expansions of arbitrary ordered fields.
Congruence relations on lattices of recursively enumerable sets
Authors: Hammond Todd 
Published: December 2007

Let {We}e∈ω be a standard enumeration of the recursively enumerable (r. e.) subsets of ω = {0, 1, 2, …}. The lattice of recursively enumerable sets, is the structure ({We}e∈ω, ∪, ∩). is the sublattice of consisting of the recursive sets.Suppose is a lattice of subsets of ω. ≡ is said to be a congruence relation on if ≡ is an equivalence relation on and if for all U, U′ ∈ and V, V ∈ , if U ≡ U′ and V ≡ V′ then U ∪ U′ ≡ V ∪ V′ and U ∩ U′ ≡ V ∩ V′. [U] = {V ∈ | V ≡ U} is the equivalence class of U. If ≡ is a congruence relation on , the elements of the quotient lattice / ≡ are the equivalence classes of ≡. [U] ∪ [V] is defined as [U ∪ V], and [U] ∩ [V] is defined as [U ∩ V].The quotient lattices of (or of some sublattice ) correspond naturally with the congruence relations which give rise to them, and in turn the congruence relations of sublattices of can be characterized in part by their computational complexity. The aim of the present paper is to characterize congruence relations in some of the most important complexity classes.
Monoid based semantics for linear formulas (corrected republication)
Authors: Mitchell W. P. R. , Simmons H. 
Published: December 2007

AbstractEach Girard quantale (i.e., commutative quantale with a selected dualizing element) provides a support for a semantics for linear propositional formulas (but not for linear derivations). Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group (both commutative). In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of handling duality.
Splitting properties of n-c.e. enumeration degrees
Authors: Kalimullin I. SH. 
Published: December 2007

AbstractIt is proved that if 1 < m < 2p ≤ n for some integer p then the elementary theories of posets of m-c.e. and n-c.e. e-degrees are distinct. It is proved also that the structures 〈2n, ≤, 〉 and 〈2n, ≤. P〉 are not elementary equivalent where P is the predicate P(a) = “a is a e-degree”.
Groundwork for weak analysis
Authors: Fernandes António M. , Ferreira Fernando 
Published: December 2007

AbstractThis paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q.
Coding with ladders a well ordering of the reals
Authors: Abraham Uri , Shelah Saharon 
Published: December 2007

AbstractAny model of ZFC + GCH has a generic extension (made with a poset of size ℵ2) in which the following hold: there exists a-well ordering of the reals, The proof consists in iterating posets designed to change at will the guessing properties of ladder systems on ω1. Therefore, the study of such ladders is a main concern of this article.
Interpolation for first order S5
Authors: Fitting Melvin 
Published: December 2007

AbstractAn interpolation theorem holds for many standard modal logics, but first order S5 is a prominent example of a logic for which it fails. In this paper it is shown that a first order S5 interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.
Multiplication complexe et équivalence élémentaire dans le langage des corps (Complex multiplication and elementary equivalence in the language of fields)
Authors: Vidaux Xavier 
Published: December 2007

AbstractLet K and K′ be two elliptic fields with complex multiplication over an algebraically closed field k of characteristic 0. non k-isomorphic, and let C and C′ be two curves with respectively K and K′ as function fields. We prove that if the endomorphism rings of the curves are not isomorphic then K and K′ are not elementarily equivalent in the language of fields expanded with a constant symbol (the modular invariant). This theorem is an analogue of a theorem from David A. Pierce in the language of k-algebras.
On orbits, of prompt and low computably enumerable sets
Authors: Wald Kevin 
Published: December 2007

AbstractThis paper concerns automorphisms of the computably enumerable sets. We prove two results relating semilow sets and prompt degrees via automorphisms, one of which is complementary to a recent result of Downey and Harrington. We also show that the property of effective simplicity is not invariant under automorphism, and that in fact every promptly simple set is automorphic to an effectively simple set. A major technique used in these proofs is a modification of the Harrington-Soare version of the method of Harrington-Soare and Cholak for constructing Δ30 automorphisms; this modification takes advantage of a recent result of Soare on the extension of “restricted” automorphisms to full automorphisms.
Definable incompleteness and Friedberg splittings
Authors: Miller Russell 
Published: December 2007

AbstractWe define a property R(A0, A1) in the partial order of computably enumerable sets under inclusion, and prove that R implies that A0 is noncomputable and incomplete. Moreover, the property is nonvacuous. and the A0 and A1 which we build satisfying R form a Friedberg splitting of their union A, with A1 prompt and A promptly simple. We conclude that A0 and A1 lie in distinct orbits under automorphisms of , yielding a strong answer to a question previously explored by Downey, Stob, and Soare about whether halves of Friedberg splittings must lie in the same orbit.