bluuebunny/crossref_metadata_2025_split huggingface dataset:
The unsolvability of the uniform halting problem for two state
Turing machines
Authors: Herman Gabor T. 
Published: May 2006

The uniform halting problem (UH) can be stated as follows:Give a decision procedure which for any given Turing machine (TM) will
decide whether or not it has an immortal instantaneous description (ID).An ID is called immortal if it has no terminal successor. As it is generally
the case in the literature (see e.g. Minsky [4, p. 118]) we assume that in
an ID the tape must be blank except for some finite number of squares. If we
remove this restriction the UH becomes the immortality problem (IP).
Connexive class logic
Authors: McCall Storrs 
Published: May 2006

Student. I've been studying the logic of classes, and can't see how any class can be included in its own complement.Teacher. Surely you've heard of the null class, which is included in every class, and hence in its own complement?Student. That also strikes me as somehow implausible. How do you define ‘inclusion’?Teacher. In the usual way. a is included in b if and only if the intersection of a with the complement of b is null.
Analytic cut
Authors: Smullyan Raymond M. 
Published: May 2006

The real importance of cut-free proofs is not the elimination of cuts per se, but rather that such proofs obey the subformula principle. In this paper we accomplish this latter objective in a different manner.In the usual formulations of Gentzen systems, there is only one axiom scheme; all the other postulates are inference rules. By contrast, we consider here some Gentzen type axiom systems for propositional logic and Quantification Theory in which there is only one inference rule; all the other postulates are axiom schemes. This admits of an unusually elegant axiomatization of logic.
A class of decidable intermediate propositional logics
Authors: McKay C. G. 
Published: May 2006

For the terminology and motivation of this note, my earlier paper [3] should be consulted. Here I make a slight change by requiring the Intuitionist Propositional Logic H to be given in terms of axiom schemata rather than axioms.Definition. An axiom schema F is essentially negative iff each schematic letter appearing in F is negated.Thus the schemata (¬P ∨ ¬¬P), (¬¬(¬P ∨ ¬Q)→(¬P ∨ ¬Q)) are essentially negative, whereas (¬P ∨ P) and (¬¬P→P) are not.Lemma. Let F be an essentially negative axiom schema. Then F yields at most finitely many intuitionistically nonequivalent axioms whose atoms are chosen from a fixed finite set.
“Helping”: several formalizations
Authors: Lynch Nancy 
Published: May 2006

Much recent work in the theory of computational complexity ([Me], [FR]. [SI]) is concerned with establishing “the complexity” of various recursive functions, as measured by the time or space requirements of Turing machines which compute them. In the above work, we also observe another phenomenon: knowing the values of certain functions makes certain other functions easier to compute than they would be without this knowledge. We could say that the auxiliary functions “help” the computation of the other functions.For example, we may conjecture that the “polynomial-complete” problems of Cook [C] and Karp [K] and Stockmeyer [S2], such as satisfiability of propositional formulas or 3-colorability of planar graphs, in fact require time proportional to nlog2n to be computed on a deterministic Turing machine. Then since the time required to decide if a planar graph with n nodes is 3-colorable can be lowered to a polynomial in n if we have a precomputed table of the satisfiable formulas in the propositional calculus, it is natural to say that the satisfiability problem “helps” the computation of the answers to the 3-coloring problem. Similar remarks may be made for any pair of polynomial-complete problems.As a further illustration, Meyer and Stockmeyer [MS] have shown that, for a certain alphabet Σ, recognition of the set of regular expressions with squaring which are equivalent to Σ* requires Turing machine space cn for some constant c, on an infinite set of arguments. We also know that this set of regular expressions, which we call RSQ, may actually be recognized in space dn for some other constant d. Theorem 6.2 in [LMF] implies that there is some problem (not necessarily an interesting one) of complexity approximately equal to that of RSQ, which does not reduce the complexity of RSQ below cn. It does not “help” the computation of RSQ.
Two forms of the axiom of choice for an elementary topos
Authors: Penk Anna Michaelides 
Published: May 2006

The concept of a topos as a system, or world in which mathematics could be defined and interpreted, was developed by F. W. Lawvere and M. Tierney. Much of their work is embodied in the lecture notes Elementary toposes by A. Kock and G. C. Wraith [6].In an early paper Lawvere set forth a set of axioms for approximately such a system [8]. The topos constructed there is a set-like category that includes among its axioms an axiom of infinity and an axiom of choice.In its final form an elementary topos is freed from any such axioms.The most prominent example of an elementary topos is a set theory with the usual Zermelo-Fraenkel or Godel-Bernays set of axioms.In this paper I have tried to determine what, if any, is the effect of an axiom of choice introduced in a topos, and how are some of the set-theoretic equivalents of such an axiom related in topos theory.Since the set-theoretic membership relation ∈, the notions of an “empty” set and a “power” set are definable in topos theory, it makes sense to talk about a “choice map” that picks a single element out of every nonempty object, provided that these objects can be somehow collected into a single object or “family.” In other words, an analogue of the usual choice axiom can be formulated in elementary topos language; this is axiom AC2 of the text.
First steps in intuitionistic model theory
Authors: de Swart H. 
Published: May 2006

In this paper we will do some model theory with respect to the models, defined in [7] and, as in [7], we will work again in intuitionistic metamathematics.In this paper we will only consider models M = ‹S, TM›, where S is one fixed spreadlaw for all models M, namely the universal spreadlaw. That we can restrict ourselves to this class of models is a consequence of the completeness proof, which is sketched in [7, §3].The main tools in this paper will be two model-constructions:(i) In §1 we will consider, under a certain condition C(M0, M, s), the construction of a model R(M0, M, s) from two models M0 and M with respect to the finite sequence s.(ii) In §2 we will construct from an infinite sequence M0, M1, M2, … of models a new model Σi∈INMi.Syntactic proofs of the disjunction property and the explicit definability theorem are well known.C. Smorynski [8] gave semantic proofs of these theorems with respect to Kripke models, however using classical metamathematics. In §1 we will give intuitionistically correct, semantic proofs with respect to the models, defined in [7] using Brouwer's continuity principle.Let W be the fan of all models (see [7, Theorem 2.7]) and let Γ be a countably infinite sequence of sentences.
Rings which admit elimination of quantifiers
Authors: Rose Bruce I. 
Published: May 2006

AbstractWe say that a ring admits elimination of quantifiers, if in the language of rings, {0, 1, +, ·}, the complete theory of R admits elimination of quantifiers.Theorem 1. Let D be a division ring. Then D admits elimination of quantifiers if and only if D is an algebraically closed or finite field.A ring is prime if it satisfies the sentence: ∀x∀y∃z (x =0 ∨ y = 0∨ xzy ≠ 0).Theorem 2. If R is a prime ring with an infinite center and R admits elimination of quantifiers, then R is an algebraically closed field.Let be the class of finite fields. Let be the class of 2 × 2 matrix rings over a field with a prime number of elements. Let be the class of rings of the form GF(pn)⊕GF(pk) such that either n = k or g.c.d. (n, k) = 1. Let be the set of ordered pairs (f, Q) where Q is a finite set of primes and such that the characteristic of the ring f(q) is q. Finally, let be the class of rings of the form ⊕q ∈ Qf(q), for some (f, Q) in .Theorem 3. Let R be a finite ring without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R belongs to.Theorem 4. Let R be a ring with the descending chain condition of left ideals and without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R is an algebraically closed field or R belongs to.In contrast to Theorems 2 and 4, we haveTheorem 5. If R is an atomless p-ring, then R is finite, commutative, has no nonzero trivial ideals and admits elimination of quantifiers, but is not prime and does not have the descending chain condition.We also generalize Theorems 1, 2 and 4 to alternative rings.
A proof of the cut-elimination theorem in simple type theory
Authors: Titani Satoko 
Published: May 2006

In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style.Inductive definition of types.0 and 1 are types.If τ1, …, τn are types, then (τ1, …, τn) is a type.Basic symbols.a1τ, a2τ, … for free variables of type τ.x1τ, x2τ, … for bound variables of type τ.An arbitrary number of constants of certain types.An arbitrary number of function symbols with certain argument places.
An interpretation of “finite” modal first-order languages in classical second-order languages
Authors: Lehmann Scott K. 
Published: May 2006

This note describes a simple interpretation * of modal first-order languages K with but finitely many predicates in derived classical second-order languages L(K) such that if Γ is a set of K-formulae, Γ is satisfiable (according to Kripke's 55 semantics) iff Γ* is satisfiable (according to standard (or nonstandard) second-order semantics).The motivation for the interpretation is roughly as follows. Consider the “true” modal semantics, in which the relative possibility relation is universal. Here the necessity operator can be considered a universal quantifier over possible worlds. A possible world itself can be identified with an assignment of extensions to the predicates and of a range to the quantifiers; if the quantifiers are first relativized to an existence predicate, a possible world becomes simply an assignment of extensions to the predicates. Thus the necessity operator can be taken to be a universal quantifier over a class of assignments of extensions to the predicates. So if these predicates are regarded as naming functions from extensions to extensions, the necessity operator can be taken as a string of universal quantifiers over extensions.The alphabet of a “finite” modal first-order language K shall consist of a non-empty countable set Var of individual variables, a nonempty finite set Pred of predicates, the logical symbols ‘¬’ ‘∧’, and ‘∧’, and the operator ‘◊’. The formation rules of K generate the usual Polish notations as K-formulae. ‘ν’, ‘ν1’, … range over Var, ‘P’ over Pred, ‘A’ over K-formulae, and ‘Γ’ over sets of K-formulae.
Descending sequences of degrees
Authors: Steel John 
Published: May 2006

Our unexplained notation is that of Rogers [4]. Let P ⊆ 2N × 2N. We call a sequence <An: n ∈ N> of subsets of N a P-sequence iff ∀n(An+1 = the unique B such that P(An, B)).Theorem. Let P ⊆ 2N × 2N be arithmetical. Then there is no P-sequence <An: n ∈ N> such that ∀n(A′n+1 ≤T An).This theorem improves a result of Friedman [2] who showed that for no arithmetical P is there a P-sequence <An: n ∈ N> such that An + 1 is a code for an ω-model of the relative arithmetic comprehension schema, and An + 1 is present in the model coded by An, for all n. Other related results are those of Harrison [3], who showed there is a sequence <An: n ∈ N> such that ∀n<A′n + 1 ≤T An>, and of Enderton and Putnam [1], who showed there is no sequence <An: n ∈ N> with ∀n(A′n + 1 ≤T An) and A0 hyperarithmetic.Our theorem is closely connected to Gödel's second incompleteness theorem. Its proof is a recursion theoretic parallel to the proof of Gödel's theorem. In §2 we draw a version of Gödel's theorem as a corollary to ours.
Skolem reduction classes
Authors: Goldfarb Warren D. , Lewis Harry R. 
Published: May 2006

Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form ∀···∀∃···∃ is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the ∀∀∀∃ class is a reduction class, for Gödel [3], Kalmár [4], and Schütte [6] showed the ∀∀∃···∃ class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.Let x, y1, y2, be distinct variables (we shall use v1, v2, ··· and w1, w2, ··· as metavariables ranging over these variables), and for each i ≥ 1 let Y(i) be the set {y1, ···, yi}. An atomic formula Pv1 ··· vk will be said to be {v1, ···, vk}-based. For any n ≥ 1, p ≥ 1, and any subsets Y1, ··· Yp of Y(n), let C(n, Y1, ···, Yp) be the class of all those closed formulas with prefix ∀y1 ··· ∀yn∃x such that each atomic subformula not containing the variable x is Yi-based for some i, 1 ≤ i ≤ p.
A sequent calculus for type assignment
Authors: Seldin Jonathan P. 
Published: May 2006

The sequent calculus formulation (L-formulation) of the theory of functionality without the rules allowing for conversion of subjects of [3, §14E6] fails because the (cut) elimination theorem (ET) fails. This can be most easily seen by the fact that it is easy to prove in the systemandbut not (as is obvious if α is an atomic type [an F-simple])The error in the “proof” of ET in [14, §3E6], [3, §14E6], and [7, §9C] occurs in Stage 3, where it is implicitly assumed that if [x]X ≡ [x] Y then X ≡ Y. In the above counterexample, we have [x]x ≡ ∣ ≡ [x](∣x) but x ≢ ∣x. Since the formulation of [2, §9F] is not really satisfactory (for reasons stated in [3, §14E]), a new seguent calculus formulation is needed for the case in which the rules for subject conversions are not present. The main part of this paper is devoted to presenting such a formulation and proving it equivalent to the natural deduction formulation (T-formulation). The paper will conclude in §6 with some remarks on the result that every ob (term) with a type (functional character) has a normal form.The conventions and definitions of [3], especially of §12D and Chapter 14, will be used throughout the paper.
A note on the number of zeros of polynomials and exponential polynomials
Authors: Smorynski C. 
Published: May 2006

The negative solution of Hilbert's Tenth Problem brought with it a number of unsolvable Diophantine problems. Moreover, by actually providing a Diophantine characterization of recursive enumerability, the proof of the negative solution opened the door to the techniques of recursion theory. In this note, we wish to apply several recursion-theoretic facts and an improvement on the exponential Diophantine representation to refine the exponential case of a result of Davis [1972] regarding the difficulty of determining the number of zeros of a polynomial.P, Q, etc. will denote polynomials or exponential polynomials–exactly which will be clear from the context. Let # (P) denote the number of distinct nonnegative zeros of P. Further, let C = {0,1, …,ℵ0} be the set of possible values of # (P). For A ⊆ C, we define A * to beWith this notation, Davis' result reads:Theorem 0.1 (DAVIS). A* is recursive iff A = ∅ or A = C.The refinement we will prove is:Theorem 0.2 (Exponential Case). A * is r.e. iff A = ∅ or A = {c: c ≥ a: m} for some finite m.
Beth definability in infinitary languages
Authors: Gregory John 
Published: May 2006

Some negative results will be proved concerning the following for certain infinitary languages ℒ1 and ℒ2.Definition. Beth(ℒ1, ℒ2) iff, for every sentence ϕ(R) of ℒ1, and n-place relation symbols R and S such that S does not occur in ϕ(R), ifthen there is an ℒ2 formula θ(x1, …, xn) such thatand θ is built up using only those constant and relation symbols of ϕ other than R.That is, Beth(ℒ1, ℒ2) iff for every implicit ℒ1 definition ϕ(R) of relations, there is a corresponding explicit ℒ2 definition θ. Beth(ℒωω, ℒωω) was proved by Beth.Malitz proved that not Beth(ℒω1 ω1, ℒ∞∞) (hence not Beth (ℒ∞∞, ℒ∞∞)), but Beth (ℒ∞ω, ℒ∞∞). In §1, it is shown that Beth(ℒ∞ω, ℒ∞ω) is false. In §2, we strengthen this by showing that, for every cardinal κ, not Beth(ℒ∞ω, ℒ∞κ). In fact, not Beth (ℒκ+ω, ℒ∞κ) follows from property A(κ) defined in §2, and A(κ) is known for regular κ > ω (unpublished result of Morley).More information on infinitary Beth and Craig theorems is given in [2] and [3]. We assume that the reader is acquainted with the languages ℒκλ which allow conjunctions over ≺κ formulas and quantifiers over ≺λ variables. Thus, we assume that the reader is acquainted with the back and forth argument for showing that two structures are ≡∞κ (ℒ∞κ-elementarily equivalent). Our notation is fairly standard.
A formalization of Essenin-Volpin's proof theoretical studies by means of nonstandard analysis
Authors: Geiser James R. 
Published: May 2006

This paper constitutes a short report on the proof theory which developed in the course of an investigation of Essenin-Volpin's foundational studies (see his paper in Infinitistic methods.) The Infinitistic methods paper is primarily concerned with proving the consistency of ZF. His arguments employ some very unusual ideas, especially that of the possibility of different length natural number series. The modal setting which he uses for these ideas and which is really all important is not reflected in the present paper. Only a simple representation of this idea is considered, namely, the use of *N, the nonstandard natural numbers, together with N, the standard natural numbers, to play the roles of a “long” and a “short” number series.It will be useful to make a few general remarks before beginning on the technical details. These remarks are especially directed towards those people who have read Essenin-Volpin's work, the above-mentioned paper in particular and the one appearing in the proceedings of the 1968 Conference on Intuitionism and Proof Theory at Buffalo, New York.I want to draw a comparison between the ultra-intuitionistic position of Essenin-Volpin on the one hand with the intuitionistic and realistic positions on the foundations of mathematics on the other hand. Intuitionism makes a transition from the traditional mathematical position (realism) that the rules of mathematical reasoning must be constructed so as to preserve truth (as known by an omniscient being about “the real world” of abstract mathematical objects) to the position that the rules of mathematical reasoning must be in accord with the process of knowing (performed by the “ideal mathematician” or “creative subject”) about the world of mental constructions. Ultra-intuitionism deepens and extends this transition to the position that the fundamental rules of mathematical reasoning must be in accord with processes of knowing accessible to human beings.
Π10 classes and Boolean combinations of recursively enumerable sets
Authors: Jockusch Carl G. 
Published: May 2006

Let be the collection of all sets which are finite Boolean combinations of recursively enumerable (r.e.) sets of numbers. Dale Myers asked [private correspondence] whether there exists a nonempty class of sets containing no member of . In this note we construct such a class. The motivation for Myers' question was his observation (reported in [1]) that the existence of such a class is equivalent to the assertion that there is a finite consistent set of tiles which has no m-trial tiling of the plane for any m (obeying the “origin constraint”). (For explanations of these terms and further results on tilings of the plane, cf. [1] and [5].) In addition to the application to tilings, the proof of our results gives some information on bi-immune sets and on complete extensions of first-order Peano arithmetic.A class of sets may be roughly described as the class of infinite binary input tapes for which a fixed Turing machine fails to halt, or alternatively as the class of infinite branches of a recursive tree of finite binary sequences. (In these definitions, sets of numbers are identified with the corresponding binary sequences.) Precise definitions, as well as many results concerning such classes, may be found in [3] and [4].
ZF ⊦ Σ40 determinateness
Authors: Paris J. B. 
Published: May 2006

In this paper we show that in Zermelo-Fraenkel set theory (ZF) sets of reals are determinate.Before proceeding to the proof it will be helpful to consider some previous work in this area. The first major result was obtained by Gale and Stewart [3] who showed that in ZF open games are determinate. This was then successively improved by Wolfe [4] to (and so of course ) and then by Morton Davis [1] to . The results of Morton Davis further showed that countable unions of sufficiently ‘simple’ determinate sets are also determinate. At this time, however, sets did not appear sufficiently simple for this method to be applied in order to get determinacy.The next major advance was made by D. A. Martin who showed, using indiscernibles, that with large cardinal assumptions games are equivalent to certain open games (i.e., player I (II) has a winning strategy for the game iff I (II) has a winning strategy for the open game). Thus, by the Gale–Stewart result, games are determinate. Martin's result also showed that under these large cardinal assumptions sets are sufficiently simple for the Morton Davis method to be applied to them.
On order-types of models
Authors: Hodges Wilfrid 
Published: May 2006

Let T be a theory in a first-order language L. Let L have a predicate ν0 ≺ ν1 such that in every model of T, the interpretation of ≺ is a linear ordering with infinite field. The order-type of this ordering will be called the order-type of the model .Several recent theorems have the following form: if T has a model of order-type ξ then T has a model of order-type ζ (see [1]). We shall add one to the list. The new feature of our result is that the order-type ζ may be in a sense “opposite” to ξ. Silver's Theorem 2.24 of [3] is a corollary of Theorem 1 below.Theorem 1. Let κ be a strong limit number (i.e. μ < κ implies 2μ < κ). Suppose λ < κ, and suppose that for every cardinal μ < κ, T has a model with where the order-type of contains no descending well-ordered sequences of length λ. Then for every cardinal μ ≥ the cardinality ∣L∣ of the language L, T has models and such that(a) the field of is the union of ≤ ∣L∣ well-ordered (inversely well-ordered) parts;(b) .The proof is by Ehrenfeucht-Mostowski models; we presuppose [2].