bluuebunny/crossref_metadata_2025_split huggingface dataset:
Digital simulation of analog computation and Church's thesis
Authors: Rubel Lee A. 
Published: May 2006

Church's thesis, that all reasonable definitions of “computability” are equivalent, is not usually thought of in terms of computability by acontinuouscomputer, of which the general-purpose analog computer (GPAC) is a prototype. Here we prove, under a hypothesis of determinism, that the analytic outputs of aC∞GPAC are computable by a digital computer.In [POE, Theorems 5, 6, 7, and 8], Pour-El obtained some related results. (The proof there of Theorem 7 depends on her Theorem 2, for which the proof in [POE] is incorrect, but for which a correct proof is given in [LIR]. Also, the proof in [POE] of Theorem 8 depends on the unproved assertion that a solution of an algebraic differential equation must be analytic on an open subset of its domain. However, this assertion was later proved in [BRR].) As in [POE], we reduce the problem to a problem about solutions of certain systems of algebraic differential equations (ADE's). If such a system is nonsingular (i.e. if the “separant” does not vanish along the given solution), then the argument is very easy (see [VSD] for an even simpler situation), so that the essential difficulties arise fromsingularsystems. Our main tools in handling these difficulties are drawn from the excellent (and difficult) paper [DEL] by Denef and Lipshitz. The author especially wants to thank Leonard Lipshitz for his kind help in the preparation of the present paper.We emphasize here that our proof of the simulation result applies only to the GPAC as described below. The GPAC's form a natural subclass of the class of all analog computers, and are based on certain idealized components (“black boxes”), mostly associated with the technology of past decades. One can easily envisage other kinds of black boxes of an input-output character that would lead to different kinds of analog computers. (For example, one could incorporate delays, or spatial integrators in addition to the present temporal integrators, etc.) Whether digital simulation is possible for these “extended” analog computers poses a rich and challenging set of research questions.
A first approach to abstract modal logics
Authors: Font Josep M. , Verdú Ventura 
Published: May 2006

AbstractThe object of this paper is to make a study of four systems of modal logic (S4, S5, and their intuitionistic analogues IM4 and IM5) with the techniques of the theory of abstract logics set up by Suszko, Bloom, Brown, Verdú and others. The abstract concepts corresponding to such systems are defined as generalizations of the logics naturally associated to their algebraic models (topological Boolean or Heyting algebras, general or semisimple). By considering new suitably defined connectives and by distinguishing between having the rule of necessitation only for theorems or as a full inference rule (which amounts to dealing with all filters or with open filters of the algebras) we are able to reduce the study of a modal (abstract) logic L to that of two nonmodal logics L− and L+ associated with L. We find that L is “of IM4 type” if and only if L− and L+ are both intuitionistic and have the same theorems, and logics of type S4, IM5 or S5 are obtained from those of type IM4 simply by making classical L−, L+ or both. We compare this situation with that found in recent approaches to intuitionistic modal logic using birelational models or using higher-level sequent-systems. The treatment of modal systems with abstract logics is rather new, and in our way to it we find several general constructions and results which can also be applied to other modal systems weaker than those we study in detail.
Groups of finite Morley rank with transitive group automorphisms
Authors: Nesin Ali 
Published: May 2006

The aim of this short note is to prove the following result:Theorem. Let G be a group of finite Morley rank with Aut G acting transitively on G/{1}. Then G is either abelian or a bad group.Bad groups were first defined by Cherlin [Ch]: these are groups of finite Morley rank without solvable and nonnilpotent connected subgroups. They have been investigated by the author [Ne 1], Borovik [Bo], Corredor [Co], and Poizat and Borovik [Bo-Po]. They are not supposed to exist, but we are far from proving their nonexistence. This is one of the major obstacles to proving Cherlin's conjecture: infinite simple groups of finite Morley rank are algebraic groups.If the group G of the theorem is finite, then it is well known that G ≈ ⊕Zp for some prime p: clearly all elements of G have the same order, say p, a prime. Thus G is a finite p-group, so has a nontrivial center. But Aut G acts transitively; thus G is abelian. Since it has exponent p, G ≈ ⊕Zp.The same proof for infinite G does not work even if it has finite Morley rank, for the following reasons:1) G may not contain an element of finite order.2) Even if G does contain an element of finite order, i.e. if G has exponent p, we do not know if G must have a nontrivial center.
Near-equational and equational systems of logic for partial functions. II
Authors: Craig William 
Published: May 2006

For the reader's convenience, we begin Part II by restating the rules for constructing Sq derivations given in §2:We let R be the set of 14 rules for Sq, R* the set of pure *-rules in R, R≃ the set of pure ≃-rules in R, and R− the set R ∩ − {Exs≃}. The closure of any F ⊆ Sq under R will be denoted by csRF, and the direct image of F under Cut*, for example, by Cut*(F).
Definability in terms of the successor function and the coprimeness predicate in the set of arbitrary integers
Authors: Richard Denis 
Published: May 2006

AbstractUsing coding devices based on a theorem due to Zsigmondy, Birkhoff and Vandiver, we first define in terms of successor S and coprimeness predicate ⊥ a full arithmetic over the set of powers of some fixed prime, then we define in the same terms a restriction of the exponentiation. Hence we prove the main result insuring that all arithmetical relations and functions over prime powers and their opposite are {S, ⊥}-definable over Z. Applications to definability over Z and N are stated as corollaries of the main theorem.
Slow growing versus fast growing
Authors: Wainer S. S. 
Published: May 2006

I falsely claimed, as an aside remark in [8] and also implicitly in the abstract [9], that the slow-growing hierarchy“catches up” with the fast-growing hierarchyat level Γ0, i.e. that, for all x > 0,where x′ is some simple (even linear) function of x.Girard [4] gave the first correct analysis of the deep relationship which exists between G and F, based on his extensive category-theoretic framework for -logic. This analysis indicates that the first point at which G catches up with F is the ordinal of the theory ID<ω(0 of arbitrary finite iterations of an inductive definition. This is very far beyond Γ0! In particular, in order to capture F at level ∣IDn∣ the slow-growing hierarchy must be generated up to ∣IDn+1∣, i.e. one extra iteration of an inductive definition is needed in order to generate sufficient new ordinals.
Ramsey cardinals, α-Erdös cardinals, and the core model
Authors: Schlingmann Dirk R. H. 
Published: May 2006

The core model K was introduced by R. B. Jensen and A. J. Dodd [DoJ]. K is the union of Gödel's constructible universe L together with all mice, i.e., , and K is a transitive model of ZFC + (V = K) + GCH (see [DoJ]). V = K is consistent with the existence of Ramsey cardinals [M], and if cf(α) > ω, V = K is consistent with the existence of α-Erdös cardinals [J]. Let K be Ramsey. Then there is a smallest inner model Wκ of ZFC in which κ is Ramsey. We have Wκ ⊨ V = K and Wκ ⊆ K [M]. The existence of Wκ with is equivalent to the existence of a sharplike mouse on N ⊨ K with N ⊨ κ Ramsey. (A mouse N on is called sharplike provided .) We have , where is the mouse iteration of N. N is the oleast mouse not in Wκ (see [J] and [DJKo]). Here < denotes the mouse order. The context always clarifies whether the mouse order or the usual <-relation is meant.The main result of §1 is that Wκ ⊨ κ is the only Ramsey cardinal. A similar result has been found true in the smallest inner model L[U] of ZFC + “κ is measurable” if U is a normal measure on κ: L[U] ⊨ κ is the only measurable cardinal [Ku].
On analytic filters and prefilters
Authors: Zafrany Samy 
Published: May 2006

AbstractWe show that every analytic filter is generated by a prefilter, every filter is generated by a prefilter, and if is a prefilter then the filter generated by it is also . The last result is unique for the Borel classes, as there is a -complete prefilter P such that the filter generated by it is -complete. Also, no complete coanalytic filter is generated by an analytic prefilter. The proofs use König's infinity lemma, a normal form theorem for monotone analytic sets, and Wadge reductions.
Finite extensions and the number of countable models
Authors: Millar Terrence 
Published: May 2006

An Ehrenfeucht theory is a complete first order theory with exactly n countable models up to isomorphism, 1 < n < ω. Numerous results have emerged regarding these theories ([1]–[15]). A general question in model theory is whether or not the number of countable models of a complete theory can be different than the number of countable models of a complete consistent extension of the theory by finitely many constant symbols. Examples are known of Ehrenfeucht theories that have complete extensions by finitely many constant symbols such that the extensions fail to be Ehrenfeucht ([4], [8], [13]). These examples are easily modified to allow finite increases in the number of countable models.This paper contains examples in the other direction—complete theories that have consistent extensions by finitely many constant symbols such that the extensions have fewer countable models. This answers affirmatively a question raised by, among others, Peretyat'kin [8]. The first example will be an Ehrenfeucht theory with exactly four countable models with an extension by a constant symbol that has only three countable models. The second example will be a complete theory that is not Ehrenfeucht, but which has an extension by a constant symbol that is Ehrenfeucht. The notational conventions for this paper are standard.Peretyat'kin introduced the theory of a dense binary branching tree with a meet operator [7]. Dense ω-branching trees have also proven useful [5], [11]. Both of the Theories that will be constructed make use of dense ω-branching trees.
Relative recursive enumerability of generic degrees
Authors: Kumabe Masahiro 
Published: May 2006

Let ω be the set of natural numbers, i.e. {0, 1, 2, 3, …}. A string is a mapping from an initial segment of ω into {0, 1}. We identify a set A ≤ ω with its characteristic function. A set A ≤ ω is called n-generic if it is Cohen-generic for n-quantifier arithmetic. This is equivalent to saying that for every set of strings S, there is a σ < A such that σ ∈ S or (∀ν ≥ σ)(ν ∉ S). By degree we mean Turing degree (of unsolvability). We call a degree n-generic if it has an n-generic representative. For a degree a, D(≤ a) denotes the set of degrees recursive in a.The relation between generic degrees and minimal degrees has been widely studied. Spector [9] proved the existence of minimal degrees. Shoenfield [8] simplified the proof by using trees. In the construction of a minimal degree, given σ we extend σ to ν so that ν is in the (splitting or nonsplitting) subtree of a given tree. But in the construction of a generic set, given σ we extend σ to ν to meet the given dense set. So these two constructions are quite different. Jockusch [5] showed that any 2-generic degree bounds no minimal degree. Chong and Jockusch [3] showed that any 1-generic degree below 0′ bounds no minimal degree.
Uniqueness of normal proofs of minimal formulas
Authors: Tatsuta Makoto 
Published: May 2006

AbstractA minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.
-stability
Authors: Ben-Arié Dror , Judah Haim 
Published: May 2006

AbstractWe investigate the connection between -stability for random and Cohen forcing notions and the measurability and categoricity of the -sets. We show that Shelah's model for -measurability and categoricity satisfies -random-stability while it does not satisfy -Cohen-stability. This gives an example of measure-category asymmetry. We also present a result concerning finite support iterations of Suslin forcing.
Counting the maximal intermediate constructive logics
Authors: Ferrari Mauro , Miglioli Pierangelo 
Published: May 2006

AbstractA proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise “constructively incompatible constructive logics”. We use a notion of “semiconstructive” logic and define wide sets of “constructive” logics by representing the “constructive” logics as “limits” of decreasing sequences of “semiconstructive” logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, “fitrations over rank formulas” are used to show that any two different logics belonging to a suitable uncountable set of “constructive” logics are “constructively incompatible”.
Learning via queries in [+, <]
Authors: Gasarch William I. , Pleszkoch Mark G. , Solovay Robert 
Published: May 2006

AbstractWe prove that the set of all recursive functions cannot be inferred using first-order queries in the query language containing extra symbols [+ , <]. The proof of this theorem involves a new decidability result about Presburger arithmetic which is of independent interest. Using our machinery, we show that the set of all primitive recursive functions cannot be inferred with a bounded number of mind changes, again using queries in [+, <]. Additionally, we resolve an open question in [7] about passive versus active learning.
Automorphism properties of stationary logic
Authors: Otto Martin 
Published: May 2006

AbstractBy means of an Ehrenfeucht-Mostowski construction we obtain an automorphism theorem for a syntactically characterized class of Laa-theories comprising in particular the finitely determinate ones. Examples of Laa-theories with only rigid models show this result to be optimal with respect to a classification in terms of prenex quantifier type: Rigidity is seen to hinge on quantification of type … ∀ … stat … permitting of the parametrization of families of disjoint stationary systems by the elements of the universe.
Extending the first-order theory of combinators with self-referential truth
Authors: Cantini Andrea 
Published: May 2006

AbstractThe aim of this paper is to introduce a formal system STW of self-referential truth, which extends the classical first-order theory of pure combinators with a truth predicate and certain approximation axioms. STW naturally embodies the mechanisms of generalpredicate application/abstractionona par withfunction application/abstraction; in addition, it allows non-trivial constructions, inspired by generalized recursion theory. As a consequence, STW provides a smooth inner model for Myhill's systems with levels of implication.
The number of proofs for a BCK-formula
Authors: Komori Yuichi , Hirokawa Sachio 
Published: May 2006

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.
Bounds for the closure ordinals of essentially monotonic increasing functions
Authors: Weiermann Andreas 
Published: May 2006

AbstractLet Ω ≔ ℵ1. For any α< εΩ + 1 ≔ min {ξ > Ω: ξ = ωξ} let EΩ(α) be the finite set of ε-numbers below Ω which are needed for the unique representation of α in Cantor-normal form using 0, Ω, +, and ω. Let α* ≔ max(EΩ(α) ∪ {0}). A function f: εΩ + 1 → Ω is called essentially increasing, if for any α < εΩ + 1; f(α) ≥ α*: f is called essentially monotonic, if for any α, β<εΩ + 1;Let be the least set of ordinals which contains 0 as an element and which satisfies the following two conditions:(a)(b)Let be the Howard-Bachmann ordinal, which is, for example, defined in [3]. The following theorem is shown: If f: εΩ + 1 → Ω is essentially monotonic and essentially increasing, then the order type of is less than or equal to .
À propos d'équations génériques
Authors: Wagner Frank O. 
Published: May 2006

AbstractWe prove that a stable solvable group G which satisfies xn = 1 generically is of finite exponent dividing some power of n. Furthermore, G is nilpotent-by-finile.A second result is that in a stable group of finite exponent, involutions either have big centralisers, or invert a subgroup of finite index (which hence has to be abelian).
Constructive set theoretic models of typed combinatory logic
Authors: Knobel Andreas 
Published: May 2006

AbstractWe shall present two novel ways of deriving simply typed combinatory models. These are of interest in a constructive setting. First we look at extension models, which are certain subalgebras of full function space models. Then we shall show how the space of singletons of a combinatory model can itself be made into one. The two and the algebras in between will have many common features. We use these two constructions in proving:There is a model of constructive set theory in which every closed extensional theory of simply typed combinatory logic is the theory of a full function space model.
Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
Authors: Kohlenbach Ulrich 
Published: May 2006

AbstractWe show how to extract effective bounds Φ for ⋀u1⋀v ≤ytu⋁wηG0-sentences which depend on u only (i.e. ⋀u⋀v ≤y, tu⋁w ≤η ΦuG0) from arithmetical proofs which use analytical assumptions of the form(ϒ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ ≤ 2, (*) can be weakened toThis is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.
Relational proof system for relevant logics
Authors: Orlowska Ewa 
Published: May 2006

AbstractA method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.
The genericity conjecture
Authors: Friedman Sy D. 
Published: May 2006

The Genericity Conjecture, as stated in Beller-Jensen-Welch [1], is the following:(*) If O# ∉ L[R], R ⊆ ω, then R is generic over L.We must be precise about what is meant by “generic”.Definition (Stated in Class Theory). A generic extension of an inner model M is an inner model M[G] such that for some forcing notion ⊆ M:(a) 〈M, 〉 is amenable and ⊩ is 〈M, 〉-definable for sentences.(b) G ⊆ is compatible, closed upwards, and intersects every 〈M, 〉-definable dense D ⊆ .A set x is generic over M if it is an element of a generic extension of M. And x is strictly generic over M if M[x] is a generic extension of M.Though the above definition quantifies over classes, in the special case where M = L and O# exists, these notions are in fact first order, as all L-amenable classes are definable over L[O#]. From now on assume that O# exists.Theorem A. The Genericity Conjecture is false.The proof is based upon the fact that every real generic over L obeys a certain definability property, expressed as follows.Fact. If R is generic over L, then for some L-amenable class A, Sat〈L, A〉 is not definable over 〈L[R],A〉, where Sat〈L,A〉 is the canonical satisfaction predicate for 〈L,A〉.
Independence and consistency proofs in quadratic form theory
Authors: Baumgartner James E. , Spinas Otmar 
Published: May 2006

We consider the following properties of uncountable-dimensional quadratic spaces (E, Φ):(*) For all subspaces U ⊆ E of infinite dimension: dim U˔ < dim E.(**) For all subspaces U ⊆ E of infinite dimension: dim U˔ < ℵ0.Spaces of countable dimension are the orthogonal sum of straight lines and planes, so they cannot have (*), but (**) is trivially satisfied.These properties have been considered first in [G/O] in the process of investigating the orthogonal group of quadratic spaces. It has been shown there (in ZFC) that over arbitrary uncountable fields (**)-spaces of uncountable dimension exist.In [B/G], (**)-spaces of dimension ℵ1 (so (*) = (**)) have been constructed over arbitrary finite or countable fields. But this could be done only under the assumption that the continuum hypothesis (CH) holds in the underlying set theory.