bluuebunny/crossref_metadata_2025_split huggingface dataset:
How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
Authors: Weiermann Andreas 
Published: May 2006

AbstractInspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε0-recursive function []0: T → ω so that a reduces to b implies [a]0 > [b]0. The construction of [ ]0 is based on a careful analysis of the Howard-Schütte treatment of Gödel's T and utilizes the collapsing function ψ: ε0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [ ]0 is also crucially based on ideas developed in the 1995 paper “A proof of strongly uniform termination for Gödel's T by the method of local predicativity” by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper.Indeed, for given n let Tn be the subsystem of T in which the recursors have type level less than or equal to n + 2. (By definition, case distinction functionals for every type are also contained in Tn.) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the Tn-derivation lengths in terms of ω+2-descent recursive functions. The derivation lengths of type one functionals from Tn (hence also their computational complexities) are classified optimally in terms of <ωn+2 -descent recursive functions.In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T0 is primitive recursive, thus any type one functional a in T0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T1 in terms of multiple recursion.As proof-theoretic corollaries we reobtain the classification of the IΣn+1-provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO(ε0) ⊢ Π20 − Refl(PA) and PRA + PRWO(ωn+2) ⊢ Π20 − Refl(IΣn+1), hence PRA + PRWO(ε0) ⊢ Con(PA) and PRA + PRWO(ωn+2) ⊢ Con(IΣn+1).For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity.
Basic logic: reflection, symmetry, visibility
Authors: Sambin Giovanni , Battilotti Giulia , Faggian Claudia 
Published: May 2006

AbstractWe introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube.
Hierarchies of monadic generalized quantifiers
Authors: Luosto Kerkko 
Published: May 2006

AbstractA combinatorial criterium is given when a monadic quantifier is expressible by means of universe-independent monadic quantifiers of width n. It is proved that the corresponding hierarchy does not collapse. As an application, it is shown that the second resumption (or vectorization) of the Härtig quantifier is not definable by monadic quantifiers. The techniques rely on Ramsey theory.
On central extensions of algebraic groups
Authors: Altinel Tuna , Cherlin Gregory 
Published: May 2006

In this paper the following theorem is proved regarding groups of finite Morley rank which are perfect central extensions of quasisimple algebraic groups.Theorem1.Let G be a perfect group of finite Morley rank and let C0be a definable central subgroup of G such that G/C0is a universal linear algebraic group over an algebraically closed field; that is G is a perfect central extension of finite Morley rank of a universal linear algebraic group. Then C0= 1.Contrary to an impression which exists in some circles, the center of the universal extension of a simple algebraic group, as an abstract group, is not finite in general. Thus the finite Morley rank assumption cannot be omitted.Corollary1.Let G be a perfect group of finite Morley rank such that G/Z(G) is a quasisimple algebraic group. Then G is an algebraic group. In particular, Z(G) is finite([4],Section27.5).An understanding of central extensions of quasisimple linear algebraic groups which are groups of finite Morley rank is necessary for the classification oftamesimpleK*-groupsof finite Morley rank, which constitutes an approach to the Cherlin-Zil’ber conjecture. For this reason the theorem above and its corollary were proven in [1] (Theorems 4.1 and 4.2) under the assumption oftameness, which simplifies the argument considerably. The result of the present paper shows that this assumption can be dropped. The main line of argument is parallel to that in [1]; the absence of the tameness assumption will be countered by a model-theoretic result and results fromK-theory. The model-theoretic result places limitations on definability in stable fields, and may possibly be relevant to eliminating certain other uses of tameness.
Similar but not the same: various versions of ♣ do not coincide
Authors: Džamonja Mirna , Shelah Saharon 
Published: May 2006

AbstractWe consider various versions of the ♣ principle. This principle is a known consequence of ◊. It is well known that ◊ is not sensitive to minor changes in its definition, e.g., changing the guessing requirement form “guessing exactly” to “guessing modulo a finite set”. We show however, that this is not true for ♣. We consider some other variants of ♣ as well.
Separation and Weak König's Lemma
Authors: Humphreys A. James , Simpson Stephen G. 
Published: May 2006

AbstractWe continue the work of [14, 3, 1, 19, 16, 4, 12, 11, 20] investigating the strength of set existence axioms needed for separable Banach space theory. We show that the separation theorem for open convex sets is equivalent to WKL0 over RCA0. We show that the separation theorem for separably closed convex sets is equivalent to ACA0 over RCA0. Our strategy for proving these geometrical Hahn–Banach theorems is to reduce to the finite-dimensional case by means of a compactness argument.
Intuitionistic completeness for first order classical logic
Authors: Berardi Stefano 
Published: May 2006

AbstractIn the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic.All results included here, but a part of the proposition (a) below, are new. This work is, ideally, a continuation of a paper by McCarty, who considered intuitionistic completeness mostly for first order intuitionistic logic.
A model with no magic set
Authors: Ciesielski Krzysztof , Shelah Saharon 
Published: May 2006

AbstractWe will prove that there exists a model of ZFC+“c =” in which every M ⊆ ℝ of cardinality less than continuum c is meager, and such that for every X ⊆ ℝ of cardinality c there exists a continuous function f : ℝ → ℝ with f[X] = [0, 1].In particular in this model there is no magic set, i.e., a set M ⊆ ℝ such that the equation f[M] = g[M] implies f = g for every continuous nowhere constant functions f,g: ℝ → ℝ.
Some two-cardinal results for O-minimal theories
Authors: Bays Timothy 
Published: May 2006

AbstractWe examine two-cardinal problems for the class of O-minimal theories. We prove that an O-minimal theory which admits some (κ, λ) must admit every (κ′, λ′). We also prove that every “reasonable” variant of Chang's Conjecture is true for O-minimal structures. Finally, we generalize these results from the two-cardinal case to the δ-cardinal case for arbitrary ordinals δ.
A strong version of Herbrand's theorem for introvert sentences
Authors: Langholm Tore 
Published: May 2006

A version of Herbrand's theorem tells us that a universal sentence of a first-order language with at least one constant is satisfiable if and only if the conjunction of all its ground instances is. In general the set of such instances is infinite, and arbitrarily large finite subsets may have to be inspected in order to detect inconsistency. Essentially, the reason that every member of such an infinite set may potentially matter, can be traced back to sentences like(1) Loosely put, such sentences effectively sabotage any attempt to build a model from below in a finite number of steps, since new members of the Herbrand universe are constantly brought to attention. Since they cause an indefinite expansion of the relevant part of the Herbrand universe, such sentences could quite appropriately be called expanding.When such sentences are banned, stronger versions of Herbrand's theorem can be stated. Define a clause (disjunction of literals) to be non-expanding if every non-ground term occurring in a positive literal also occurs (possibly as an embedded subterm) in a negative literal of the same clause. Written as a disjunction of literals, the matrix of (1) clearly fails this criterion. Moreover, say that a sentence is non-expanding if it is a universal sentence with a quantifier-free matrix that is a conjunction of non-expanding clauses. Such sentences do in a sense never reach out beyond themselves, and the relevant part of the Herbrand universe is therefore drastically reduced.
Syntactical truth predicates for second order arithmetic
Authors: Colson Loïc , Grigorieff Serge 
Published: May 2006

AbstractWe introduce a notion ofsyntactical truth predicate(s.t.p.) for the second order arithmeticPA2. An s.t.p. is a setTof closed formulas such that:(i)T(t=u) if and only if the closed first order termstanduare convertible, i.e., have the same value in the standard interpretation(ii)T(A→B) if and only if (T(A) ⇒T(B))(iii)T(∀xA) if and only if (T(A[x←t]) for any closed first order termt)(iv)T(∀X A) if and only if (T(A[X← ∆]) for any closed set definition ∆ = {x∣D(x)}).S.t.p.'s can be seen as a counterpart to Tarski's notion of (model-theoretical)validityand have main model properties. In particular, their existence is equivalent to the existence of anω-model ofPA2, this fact being provable inPA2with arithmetical comprehension only.
The Jensen Covering Property
Authors: Schimmerling E. , Woodin W. H. 
Published: May 2006

The Jensen covering lemma says that either L has a club class of indiscernibles, or else, for every uncountable set A of ordinals, there is a set B ∈ L with A ⊆ B and card (B) = card(A). One might hope to extend Jensen's covering lemma to richer core models, which for us will mean to inner models of the form L[] where is a coherent sequence of extenders of the kind studied in Mitchell-Steel [8], The papers [8], [12], [10] and [1] show how to construct core models with Woodin cardinals and more. But, as Prikry forcing shows, one cannot expect too direct a generalization of Jensen's covering lemma to core models with measurable cardinals.Recall from [8] that if L[] is a core model and α is an ordinal, then either Eα = ∅, or else Eα is an extender over As in [8], we assume here that if Eα is an extender, then Eα is below superstrong type in the sense that the set of generators of Eα is bounded in (crit(Eα)). Let us say that L[] is a lower-part core model iff for every ordinal α, Eα is not a total extender over L[]. In other words, if L[] is a lower-part core model, then no cardinal in L[] is measurable as witnessed by an extender on . Other than the “below superstrong” hypothesis, we impose no bounds on the large cardinal axioms true in the levels of a lower-part core model.
Embedding finite lattices into the ideals of computably enumerable turing degrees
Authors: Calhoun William C. , Lerman Manuel 
Published: May 2006

Abstract.We show that the lattice L20 is not embeddable into the lattice of ideals of computably enumerable Turing degrees (ℐ), We define a structure called a pseudolattice that generalizes the notion of a lattice, and show that there is a Π2 necessary and sufficient condition for embedding a finite pseudolattice into ℐ.
Sequent calculus in natural deduction style
Authors: Negri Sara , von Plato Jan 
Published: May 2006

Abstract.A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.
Definable sets in Boolean-ordered o-minimal structures. I
Authors: Newelski Ludomir , Wencel Roman 
Published: May 2006

Abstract.We prove weak elimination of imaginary elements for Boolean orderings with finitely many atoms. As a consequence we obtain equivalence of the two notions of o-minimality for Boolean ordered structures, introduced by C. Toffalori. We investigate atoms in Boolean algebras induced by algebraically closed subsets of Boolean ordered structures. We prove uniqueness of prime models in strongly o-minimal theories of Boolean ordered structures.
The classification of small types of rankω, Part I
Authors: Buechler Steven , Hoover Colleen 
Published: May 2006

Abstract.Certain basic concepts of geometrical stability theory are generalized to a class of closure operators containing algebraic closure. A specific case of a generalized closure operator is developed which is relevant to Vaught's conjecture. As an application of the methods, we proveTheorem A.Let G be a superstate group of U-rankωsuch that the generics of G are locally modular andTh(G)has few countable models. Let G−be the group of nongeneric elements of G.G+=Go+G−.LetΠ = {q∈S(∅):U(q)<ω}.For any countable model M ofTh(G)there is a finite A⊂M such thai M is almost atomic over A∪ (G+∩M) ∪ ⋃p∈Πp(M).
Disquotational truth and analyticity
Authors: Halbach Volker 
Published: May 2006

Abstract.The uniform reflection principle for the theory of uniform T-sentences is added to PA. The resulting system is justified on the basis of a disquotationalist theory of truth where the provability predicate is conceived as a special kind of analyticity. The system is equivalent to the system ACA of arithmetical comprehension. If the truth predicate is also allowed to occur in the sentences that are inserted in the T-sentences. yet not in the scope of negation, the system with the reflection schema for these T-sentences assumes the strength of the Kripke-Feferman theory KF. and thus of ramified analysis up to ε0.
Some combinatorics of imperfect information
Authors: Cameron Peter , Hodges Wilfrid 
Published: May 2006

We can use the compositional semantics of Hodges [9] to show that any compositional semantics for logics of imperfect information must obey certain constraints on the number of semantically inequivalent formulas. As a corollary, there is no compositional semantics for the ‘independence-friendly’ logic of Hintikka and Sandu (henceforth IF) in which the interpretation in a structure A of each 1 -ary formula is a subset of the domain of A (Corollary 6.2 below proves this and more). After a fashion, this rescues a claim of Hintikka and provides the proof which he lacked:… there is no realistic hope of formulating compositional truth-conditions for [sentences of IF], even though I have not given a strict impossibility proof to that effect.(Hintikka [6] page 110ff.) One curious spinoff is that there is a structure of cardinality 6 on which the logic of Hintikka and Sandu gives nearly eight million inequivalent formulas in one free variable (which is more than the population of Finland).We thank the referee for a sensible change of notation, and Joel Berman and Stan Burris for bringing us up to date with the computation of Dedekind's function (see section 4). Our own calculations, utterly trivial by comparison, were done with Maple V.The paper Hodges [9] (cf. [10]) gave a compositional semantics for a language with some devices of imperfect information. The language was complicated, because it allowed imperfect information both at quantifiers and at conjunctions and disjunctions.
Two variable first-order logic over ordered domains
Authors: Otto Martin 
Published: May 2006

AbstractThe satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations.It is shown that FO2 over ordered, respectively wellordered. domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO2. namely non-deterministic exponential time.In contrast FO2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings. wellorderings. or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO2 and computation tree logic CTL.
The covering numbers of Mycielski ideals are all equal
Authors: Shelah Saharon , Steprāns Juris 
Published: May 2006

AbstractThe Mycielski idealis defined to consist of all setsA⊆ℕksuch that {f↾X:f∈A} ≠Xkfor all. It will be shown that the covering numbers for these ideals are all equal. However, the covering numbers of the closely associated Rosłanowski ideals will be shown to be consistently different.
Existence of some sparse sets of nonstandard natural numbers
Authors: Jin Renling 
Published: May 2006

AbstractAnswers are given to two questions concerning the existence of some sparse subsets of ℋ = {0, 1 … ., H – 1} ⊆ *ℕ. where H is a hyperfinite integer. In §1. we answer a question of Kanovei by showing that for a given cut U in ℋ, there exists a countably determined set X ⊆ ℋ which contains exactly one element in each U-monad, if and only if U = a · ℕ for some a Є ℋ ∖ {0}. In §2, we deal with a question of Keisler and Leth in [6]. We show that there is a cut V ⊆ ℋ such that for any cut U, (i) there exists a U-discrete set X ⊆ ℋ with X + X = ℋ (mod H) provided , (ii) there does not exist any U-discrete set X ⊆ ℋ with X + X = ℋ (mod H) provided . We obtain some partial results for the case U = V.
Inconsistent models of arithmetic Part II: the general case
Authors: Priest Graham 
Published: May 2006

AbstractThe paper establishes the general structure of the inconsistent models of arithmetic of [7]. It is shown that such models are constituted by a sequence of nuclei. The nuclei fall into three segments: the first contains improper nuclei: the second contains proper nuclei with linear chromosomes: the third contains proper nuclei with cyclical chromosomes. The nuclei have periods which are inherited up the ordering. It is also shown that the improper nuclei can have the order type of any ordinal, of the rationals, or of any other order type that can be embedded in the rationals in a certain way.
All intermediate logics with extra axioms in one variable, except eight, are not strongly ω-complete
Authors: Fiorentini Camillo 
Published: May 2006

AbstractIn [8] it is proved that all the intermediate logics axiomatizable by formulas in one variable, except four of them, are not strongly complete. We considerably improve this result by showing that all the intermediate logics axiomatizable by formulas in one variable, except eight of them, are not strongly ω-complete. Thus, a definitive classification of such logics with respect to the notions of canonicity, strong completeness, ω-canonicity and strong ω-completeness is given.
Le problème des grandes puissances et celui des grandes racines
Authors: Portier Natacha 
Published: May 2006

RésuméSoit f une fonction de N dans N qui ne soit pas calculable en temps polynomial, et a un élément d'un corps differentiel K de caractéristique nulle. Nous appelons probleme des grandes puissances l'ensembledes uples = (x1…..xn) de K telsque x1 = af(n) et problème des grandes racines l'ensemble des uples de K tels que . Ce sont deux exemples de problèmes que l'utilisation de la dérivée ne permet pas de résoudre plus rapidement. Nous montrons que le problème des grandes racines n'est pas polynomial au sens des corps differentiels, même si nous autorisons un nombre polynomial de paramètres. et que le problème des grandes puissances n'est pas polynomial au sens des corps differentiels. même au niveau non uniforme. Les démonstrations utilisent la stabilité polynomial de la théorie des corps de caractéristique nulle. montrée par L. Blum, F. dicker. M. Shub et S. Smale, ainsi que le lemme de réduction qui permet de ramener un polynôme differentiel des variables a un polynôme des variables et de leurs dérivées.