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.

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.

Poetry?

2021 ◽  
pp. 364-380
Author(s):  
Floris Bernard ◽  
Kristoffel Demoen
Keyword(s):  
Social Contexts ◽  
Point Of View ◽  
Wide Sense ◽  
Spiritual Dimension ◽  
The Social ◽  
Moral Point ◽  
Moral Point Of View ◽  
The Difference

This chapter gives an overview of how Byzantines conceptualized “poetry.” It argues that from the Byzantine point of view, poetry only differs from prose in a very formal way, namely that it is written in verse. Both prose and poetry belonged to the category of logoi, the only label that was very frequently used, in contrast to the term “poetry,” which was reserved for the ancient poetry studied at schools. Many authors considered (and exploited) the difference between their own prose texts and poems as a primarily formal one. Nevertheless, poetry did have some functions that set it apart from prose, even if these features are for us less expected. The quality of “bound speech” gained a spiritual dimension, since verse was seen as a restrained form of discourse, also from a moral point of view. Finally, the chapter gives a brief overview of the social contexts for which (learned) poetry was the medium of choice: as an inscription, as paratext in a wide sense, as a piece of personal introspection, as invective, as summaries (often of a didactic nature), and as highly public ceremonial pieces.

Rice Theorems for ∑n-1 Sets

1977 ◽  
Vol 29 (4) ◽  
pp. 794-805 ◽  
Author(s):  
Nancy Johnson
Keyword(s):  
Finite Sets ◽  
Index Set ◽  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
The Difference

In [3] Hay proves generalizations of Rice's Theorem and the Rice-Shapiro Theorem for differences of recursively enumerable sets (d.r.e. sets). The original Rice Theorem [5, p. 3G4, Corollary B] says that the index set of a class C of r.e. sets is recursive if and only if C is empty or C contains all r.e. sets. The Rice-Shapiro Theorem conjectured by Rice [5] and proved independently by McNaughton, Shapiro, and Myhill [4] says that the index set of a class C of r.e. sets is r.e. if and only if C is empty or C consists of all r.e. sets which extend some element of a canonically enumerable class of finite sets. Since a d.r.e. set is a difference of r.e. sets, a d.r.e. set has an index associated with it, namely, the pair of indices of the r.e. sets of which it is the difference.

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

Classes of Recursively Enumerable Sets and Degrees of Unsolvability

1966 ◽  
Vol 12 (1) ◽  
pp. 295-310 ◽  
Author(s):  
Donald A. Martin
Keyword(s):  
Recursively Enumerable ◽  
Recursively Enumerable Sets ◽  
Degrees Of Unsolvability

Non-deterministic structures of computation

2014 ◽  
Vol 25 (6) ◽  
pp. 1295-1338 ◽  
Author(s):  
YUXI FU
Keyword(s):  
Point Of View ◽  
Process Models ◽  
Theory Of Computation ◽  
Recursively Enumerable Set ◽  
Recursively Enumerable ◽  
Abstract Representations ◽  
Finite State ◽  
Model Independent ◽  
Infinite State ◽  
Deterministic Structures

Divergence and non-determinism play a fundamental role in the theory of computation, and their combined effect on computational equality deserves further study. By looking at the issue from the point of view of both computation and interaction, we are led to a canonical equality for non-deterministic computation, revealing its rich algebraic structure. We study this structure in three ways. First, we construct a complete equational system for finite-state non-deterministic computation. The challenge with such a system is to find an equational alternative to fixpoint inductionà laMilner. We establish a negative result in the form of the non-existence of a finite equational system for the canonical equality of non-deterministic computation to support our approach. We then investigate infinite-state non-deterministic computation in the light of definability and show that every recursively enumerable set is generated by an unobservable process. Finally, we prove that, as far as computation is concerned, the effect produced jointly by divergence and non-determinism is model independent for a large class of process models.We use C-graphs, which are interesting in their own right, as abstract representations of the computational objects throughout the paper.

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.

Sign in / Sign up

Export Citation Format

Share Document