Degrees of formal systems

1958 ◽  
Vol 23 (4) ◽  
pp. 389-392 ◽  
Author(s):  
J. R. Shoenfield
Keyword(s):  
Sufficient Conditions ◽  
Formal System ◽  
Independent Interest ◽  
Recursively Enumerable Set ◽  
First Order ◽  
Formal Systems ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Axiomatizable Theory

In this paper we answer some of the questions left open in [2]. We use the terminology of [2]. In particular, a theory will be a formal system formulated within the first-order calculus with identity. A theory is identified with the set of Gödel numbers of the theorems of the theory. Thus Craig's theorem [1] asserts that a theory is axiomatizable if and only if it is recursively enumerable.In [2], Feferman showed that if A is any recursively enumerable set, then there is an axiomatizable theory T having the same degree of unsolvability as A. (This result was proved independently by D. B. Mumford.) We show in Theorem 2 that if A is not recursive, then T may be chosen essentially undecidable. This depends on Theorem 1, which is a result on recursively enumerable sets of some independent interest.Our second result, given in Theorem 3, gives sufficient conditions for a theory to be creative. These conditions are more general than those given by Feferman. In particular, they show that the system of Kreisel described in [2] is creative.

Degrees of unsolvability associated with classes of formalized theories

1957 ◽  
Vol 22 (2) ◽  
pp. 161-175 ◽  
Author(s):  
Solomon Feferman
Keyword(s):  
Formal System ◽  
Point Of View ◽  
Wide Sense ◽  
Recursively Enumerable Set ◽  
Formal Systems ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
The Difference ◽  
Degrees Of Unsolvability ◽  
Order Predicate Calculus

In his well-known paper [11], Post founded a general theory of recursively enumerable sets, which had its metamathematical source in questions about the decision problem for deducibility in formal systems. However, in centering attention on the notion of degree of unsolvability, Post set a course for his theory which has rarely returned to this source. Among exceptions to this tendency we may mention, as being closest to the problems considered here, the work of Kleene in [8] pp. 298–316, of Myhill in [10], and of Uspenskij in [15]. It is the purpose of this paper to make some further contributions towards bridging this gap.From a certain point of view, it may be argued that there is no real separation between metamathematics and the theory of recursively enumerable sets. For, if the notion of formal system is construed in a sufficiently wide sense, by taking as ‘axioms’ certain effectively found members of a set of ‘formal objects’ and as ‘proofs’ certain effectively found sequences of these objects, then the set of ‘provable statements’ of such a system may be identified, via Gödel's numbering technique, with a recursively enumerable set; and conversely, each recursively enumerable set is identified in this manner with some formal system (cf. [8] pp. 299–300 and 306). However, the pertinence of Post's theory is no longer clear when we turn to systems formalized within the more conventional framework of the first-order predicate calculus. It is just this restriction which serves to clarify the difference in spirit of the two disciplines.

On the completeness of some transfinite recursive progressions of axiomatic theories

1968 ◽  
Vol 33 (1) ◽  
pp. 69-76 ◽  
Author(s):  
Jens Erik Fenstad
Keyword(s):  
Recursively Enumerable Set ◽  
First Order ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Closing The Gap ◽  
Order Arithmetic

The well-known incompleteness results of Gödel assert that there is no recursively enumerable set of sentences of formalized first order arithmetic which entails all true statements of that theory. It is equally well known that by introducing sufficiently nonconstructive rules, such as the ω-rule of induction, completeness can be re-established.Starting from the work of Turing [4] Feferman in [1] developed another method, viz. the study of transfinite recursive progressions of theories, for closing the gap between Gödel (recursively enumerable sets of axioms yield incompleteness) and Tarski (number-theoretic truth is not arithmetically definable).

Types of simple α-recursively enumerable sets

1976 ◽  
Vol 41 (2) ◽  
pp. 419-426
Author(s):  
Manuel Lerman
Keyword(s):  
Lattice Theory ◽  
Regular Cardinal ◽  
Finite Sets ◽  
First Order ◽  
Recursively Enumerable ◽  
Regular Cardinals ◽  
Constructible Sets ◽  
Set Inclusion ◽  
Order Language ◽  
Recursively Enumerable Sets

Let α be an admissible ordinal, and let (α) denote the lattice of α-r.e. sets, ordered by set inclusion. An α-r.e. set A is α*-finite if it is α-finite and has ordertype less than α* (the Σ1 projectum of α). An a-r.e. set S is simple if (the complement of S) is not α*-finite, but all the α-r.e. subsets of are α*-finite. Fixing a first-order language ℒ suitable for lattice theory (see [2, §1] for such a language), and noting that the α*-finite sets are exactly those elements of (α), all of whose α-r.e. subsets have complements in (α) (see [4, p. 356]), we see that the class of simple α-r.e. sets is definable in ℒ over (α). In [4, §6, (Q22)], we asked whether an admissible ordinal α exists for which all simple α-r.e. sets have the same 1-type. We were particularly interested in this question for α = ℵ1L (L is Gödel's universe of constructible sets). We will show that for all α which are regular cardinals of L (ℵ1L is, of course, such an α), there are simple α-r.e. sets with different 1-types.The sentence exhibited which differentiates between simple α-r.e. sets is not the first one which comes to mind. Using α = ω for intuition, one would expect any of the sentences “S is a maximal α-r.e. set”, “S is an r-maximal α-r.e. set”, or “S is a hyperhypersimple α-r.e. set” to differentiate between simple α-r.e. sets. However, if α > ω is a regular cardinal of L, there are no maximal, r-maximal, or hyperhypersimple α-r.e. sets (see [4, Theorem 4.11], [5, Theorem 5.1] and [1,Theorem 5.21] respectively). But another theorem of (ω) points the way.

scholarly journals Formalization of the MRDP Theorem in the Mizar System

2019 ◽  
Vol 27 (2) ◽  
pp. 209-221
Author(s):  
Karol Pąk
Keyword(s):  
Normal Form ◽  
Linear Equations ◽  
Negative Solution ◽  
Recursively Enumerable Set ◽  
Pell’S Equation ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Finite Products ◽  
Special Case ◽  
Martin Davis

Summary This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem. In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form x2 − (a2 − 1)y2 = 1 [8] and its solutions considered as two sequences $\left\{ {{x_i}(a)} \right\}_{i = 0}^\infty ,\left\{ {{y_i}(a)} \right\}_{i = 0}^\infty$ . We showed in [1] that the n-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation x = yi(a) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function y = xz is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9]. In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that every recursively enumerable set is Diophantine, where recursively enumerable sets have been defined by the Martin Davis normal form. The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].

Π10 classes and Boolean combinations of recursively enumerable sets

1974 ◽  
Vol 39 (1) ◽  
pp. 95-96 ◽  
Author(s):  
Carl G. Jockusch
Keyword(s):  
Turing Machine ◽  
Peano Arithmetic ◽  
Binary Sequences ◽  
First Order ◽  
Recursive Tree ◽  
Recursively Enumerable ◽  
Private Correspondence ◽  
Recursively Enumerable Sets ◽  
Binary Input

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

Σ2-collection and the infinite injury priority method

1988 ◽  
Vol 53 (1) ◽  
pp. 212-221 ◽  
Author(s):  
Michael E. Mytilinaios ◽  
Theodore A. Slaman
Keyword(s):  
Turing Degree ◽  
Recursively Enumerable Set ◽  
First Order ◽  
Recursively Enumerable ◽  
Standard Application ◽  
Priority Method ◽  
Order Arithmetic ◽  
Bounded Fragment

AbstractWe show that the existence of a recursively enumerable set whose Turing degree is neither low nor complete cannot be proven from the basic axioms of first order arithmetic (P−) together with Σ2-collection (BΣ2). In contrast, a high (hence, not low) incomplete recursively enumerable set can be assembled by a standard application of the infinite injury priority method. Similarly, for each n, the existence of an incomplete recursively enumerable set that is neither lown nor highn-1, while true, cannot be established in P− + BΣn+1. Consequently, no bounded fragment of first order arithmetic establishes the facts that the highn and lown jump hierarchies are proper on the recursively enumerable degrees.

Recursion theory and formal deducibility

1970 ◽  
Vol 35 (4) ◽  
pp. 556-558
Author(s):  
E. M. Kleinberg
Keyword(s):  
Recursion Theory ◽  
Order Logic ◽  
Negative Integer ◽  
Predicate Calculus ◽  
First Order Logic ◽  
Recursively Enumerable Set ◽  
First Order ◽  
Recursively Enumerable ◽  
Order Predicate Calculus

The enumeration, given a first-order sentence , of all sentences deducible from in the first-order predicate calculus, and the enumeration, given a non-negative integer n, of the recursively enumerable set Wn, are two well-known examples of effective processes. But are these processes really distinct? Indeed, might there not exist a Gödel numbering of the sentences of first-order logic such that for each n, if n is the number assigned to the sentence , then Wn is the set of numbers assigned to all sentences deducible from ? If this were the case, the first sort of enumeration would just be a particular instance of the second.

Some representations of Diophantine sets

1972 ◽  
Vol 37 (3) ◽  
pp. 572-578 ◽  
Author(s):  
Raphael M. Robinson
Keyword(s):  
Universal Quantifier ◽  
Natural Numbers ◽  
Recursively Enumerable Set ◽  
Minor Error ◽  
Integer Coefficients ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Image Position ◽  
A Minor

A set D of natural numbers is called Diophantine if it can be defined in the formwhere P is a polynomial with integer coefficients. Recently, Ju. V. Matijasevič [2], [3] has shown that all recursively enumerable sets are Diophantine. From this, it follows that a bound for n may be given.We use throughout the logical symbols ∧ (and), ∨ (or), → (if … then …), ↔ (if and only if), ⋀ (for every), and ⋁ (there exists); negation does not occur explicitly. The variables range over the natural numbers 0,1,2,3, …, except as otherwise noted.It is the purpose of this paper to show that if we do not insist on prenex form, then every Diophantine set can be defined existentially by a formula in which not more than five existential quantifiers are nested. Besides existential quantifiers, only conjunctions are needed. By Matijasevič [2], [3], the representation extends to all recursively enumerable sets. Using this, we can find a bound for the number of conjuncts needed.Davis [1] proved that every recursively enumerable set of natural numbers can be represented in the formwhere P is a polynomial with integer coefficients. I showed in [5] that we can take λ = 4. (A minor error is corrected in an Appendix to this paper.) By the methods of the present paper, we can again obtain this result, and indeed in a stronger form, with the universal quantifier replaced by a conjunction.

On axiomatizability within a system

1953 ◽  
Vol 18 (1) ◽  
pp. 30-32 ◽  
Author(s):  
William Craig
Keyword(s):  
Recursive Function ◽  
Recursive Relation ◽  
Recursively Enumerable Set ◽  
Formal Systems ◽  
Primitive Recursive Function ◽  
Recursively Enumerable ◽  
Primitive Recursive ◽  
Recursive Set

Let C be the closure of a recursively enumerable set B under some relation R. Suppose there is a primitive recursive relation Q, such that Q is a symmetric subrelation of R (i.e. if Q(m, n), then Q(n, m) and R(m, n)), and such that, for each m ϵ B, Q(m, n) for infinitely many n. Then there exists a primitive recursive set A, such that C is the closure under R of A. For proof, note that , where f is a primitive recursive function which enumerates B, has the required properties. For each m ϵ B, there is an n ϵ A, such that Q(m, n) and hence Q(n, m); therefore the closure of A under Q, and hence that under R, includes B. Conversely, since Q is a subrelation of R, A is included in C. Finally, that A is primitive recursive follows from [2] p. 180.This observation can be applied to many formal systems S, by letting R correspond to the relation of deducibility in S, so that R(m, n) if and only if m is the Gödel number of a formula of S, or of a sequence of formulas, from which, together with axioms of S, a formula with the Gödel number n can be obtained by applications of rules of inference of S.

Splitting theorems for speed-up related to order of enumeration

1982 ◽  
Vol 47 (1) ◽  
pp. 1-7 ◽  
Author(s):  
A. M. Dawes
Keyword(s):  
Strong Sense ◽  
Optimal Order ◽  
Recursively Enumerable Set ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Speed Up

AbstractIt is known from work of P. Young that there are recursively enumerable sets which have optimal orders for enumeration, and also that there are sets which fail to have such orders in a strong sense. It is shown that both these properties are widespread in the class of recursively enumerable sets. In fact, any infinite recursively enumerable set can be split into two sets each of which has the property under consideration. A corollary to this result is that there are recursive sets with no optimal order of enumeration.

Sign in / Sign up

Export Citation Format

Share Document