The relation of A to Prov ˹A˺ in the Lindenbaum sentence algebra

1973 ◽  
Vol 38 (2) ◽  
pp. 295-298 ◽  
Author(s):  
C. F. Kent
Keyword(s):  
Boolean Algebra ◽  
Normal Forms ◽  
Order Relation ◽  
Mathematical Induction ◽  
Axiomatic Theory ◽  
Recursive Functions ◽  
Primitive Recursive

Let U be a consistent axiomatic theory containing Robinson's Q [TMRUT, p. 51]. In order for the results below to be of interest, U must be powerful enough to carry out certain arguments involving versions of the “derivability conditions,” DC(i) to DC(iii) below, of [HBGM, p. 285], [F60, Theorem 4.7], or [L55]. Thus it must contain, at least, mathematical induction for formulas whose prenex normal forms contain at most existential quantifiers. For convenience, U is assumed also to contain symbols for primitive recursive functions and relations, and their defining equations. One of these is used to form the standard provability predicate, Prov ˹A˺, “there exists a number which is the Gödel number of a proof of A.” Upper corners denote numerals for Gödel numbers for the enclosed sentences, and parentheses are often omitted in their presence.This paper contains some results concerning the relation between the sentence A, and the sentence Prov ˹A˺ in the Lindenbaum Sentence Algebra (LSA) for U, the Boolean algebra induced by the pre-order relation A ≤ B ⇔ ⊦A → B. Half of the answer is provided by a theorem of Löb [L55], which states that ⊦Prov ˹A˺ → A ⇔ ⊦A. Hence, in the presence of DC(iii), below, it is never true that Prov ˹A˺ < A in the LSA. However, there is a large and interesting set of sentences, denoted here by Γ, for which A < Prov ⌜A⌝.

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

DECIDABILITY AND UNIVERSALITY IN THE AXIOMATIC THEORY OF COMPUTABILITY AND ALGORITHMS

2012 ◽  
Vol 23 (07) ◽  
pp. 1465-1480
Author(s):  
MARK BURGIN
Keyword(s):  
Axiomatic Theory ◽  
Proved Theorem ◽  
Recursive Functions ◽  
Natural Context ◽  
Algorithmic Problems ◽  
Weaker Conditions ◽  
Primitive Recursive

In this paper, we study to what extent decidability is connected to universality. A natural context for such a study is provided by the axiomatic theory of computability, automata and algorithms. In Section 2, we introduce necessary concepts, constructions, axioms, postulates, conditions and problems. Section 3 contains the main results of the paper. In particular, it is demonstrated (Theorems 1 and 2) that undecidability of algorithmic problems does not depend on existence of universal algorithms and may be caused by weaker conditions. At the same time, results of Theorems 2 and 3 demonstrate that decidability is incompatible with universality. It is also proved (Theorem 5) that sufficiently big classes of total algorithms/automata, such as the class of all primitive recursive functions, cannot have universal algorithms/automata.

scholarly journals Primitive recursive functions. II

1955 ◽  
Vol 6 (4) ◽  
pp. 663-663 ◽  
Author(s):  
Raphael M. Robinson
Keyword(s):  
Recursive Functions ◽  
Primitive Recursive

Universal recursion theoretic properties of r.e. preordered structures

1985 ◽  
Vol 50 (2) ◽  
pp. 397-406 ◽  
Author(s):  
Franco Montagna ◽  
Andrea Sorbi
Keyword(s):  
Equivalence Relation ◽  
Point Of View ◽  
Main Concern ◽  
Natural Numbers ◽  
Axiomatic Theory ◽  
Recursive Functions ◽  
Theoretic Point

When dealing with axiomatic theories from a recursion-theoretic point of view, the notion of r.e. preordering naturally arises. We agree that an r.e. preorder is a pair = 〈P, ≤P〉 such that P is an r.e. subset of the set of natural numbers (denoted by ω), ≤P is a preordering on P and the set {〈;x, y〉: x ≤Py} is r.e.. Indeed, if is an axiomatic theory, the provable implication of yields a preordering on the class of (Gödel numbers of) formulas of .Of course, if ≤P is a preordering on P, then it yields an equivalence relation ~P on P, by simply letting x ~Py iff x ≤Py and y ≤Px. Hence, in the case of P = ω, any preordering yields an equivalence relation on ω and consequently a numeration in the sense of [4]. It is also clear that any equivalence relation on ω (hence any numeration) can be regarded as a preordering on ω. In view of this connection, we sometimes apply to the theory of preorders some of the concepts from the theory of numerations (see also Eršov [6]).Our main concern will be in applications of these concepts to logic, in particular as regards sufficiently strong axiomatic theories (essentially the ones in which recursive functions are representable). From this point of view it seems to be of some interest to study some remarkable prelattices and Boolean prealgebras which arise from such theories. It turns out that these structures enjoy some rather surprising lattice-theoretic and universal recursion-theoretic properties.After making our main definitions in §1, we examine universal recursion-theoretic properties of some r.e. prelattices in §2.

A Hierarchy on the Class of Primitive Recursive Ordinal Functions

1976 ◽  
Vol 28 (6) ◽  
pp. 1205-1209
Author(s):  
Stanley H. Stahl
Keyword(s):  
Natural Numbers ◽  
Recursive Functions ◽  
Set Functions ◽  
Primitive Recursive ◽  
Class Of Functions ◽  
Recursive Set

The class of primitive recursive ordinal functions (PR) has been studied recently by numerous recursion theorists and set theorists (see, for example, Platek [3] and Jensen-Karp [2]). These investigations have been part of an inquiry concerning a larger class of functions; in Platek's case, the class of ordinal recursive functions and in the case of Jensen and Karp, the class of primitive recursive set functions. In [4] I began to study PR in depth and this paper is a report on an attractive analogy between PR and its progenitor, the class of primitive recursive functions on the natural numbers (Prim. Rec).

A Macro Program for the Primitive Recursive Functions

1991 ◽  
Vol 37 (8) ◽  
pp. 121-124
Author(s):  
Hilbert Levitz ◽  
Warren Nichols ◽  
Robert F. Smith
Keyword(s):  
Recursive Functions ◽  
Primitive Recursive
Sign in / Sign up

Export Citation Format

Share Document