Incompleteness along paths in progressions of theories

1962 ◽  
Vol 27 (4) ◽  
pp. 383-390 ◽  
Author(s):  
S. Feferman ◽  
C. Spector
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Order Number ◽  
Basic Logic ◽  
Natural Numbers ◽  
Logical Deduction ◽  
First Order ◽  
Primitive Recursive Function ◽  
Primitive Recursive ◽  
Recursive Definitions

We deal in the following with certain theories S, by which we mean sets of sentences closed under logical deduction. The basic logic is understood to be the classical one, but we place no restriction on the orders of the variables to be used. However, we do assume that we can at least express certain notions from classical first-order number theory within these theories. In particular, there should correspond to each primitive recursive function ξ a formula φ(χ), where ‘x’ is a variable ranging over natural numbers, such that for each numeral ñ, φ(ñ) expresses in the language of S that ξ(η) = 0. Such formulas, when obtained say by the Gödel method of eliminating primitive recursive definitions in favor of arithmetical definitions in +. ·. are called PR-formulas (cf. [1] §2 (C)).

Arithmetical representation of recursively enumerable sets

1956 ◽  
Vol 21 (2) ◽  
pp. 162-186 ◽  
Author(s):  
Raphael M. Robinson
Keyword(s):  
Recursive Function ◽  
Natural Numbers ◽  
General Recursive Function ◽  
Recursively Enumerable Set ◽  
Integer Coefficients ◽  
Primitive Recursive Function ◽  
Recursively Enumerable ◽  
Image Position ◽  
The Right ◽  
Primitive Recursive

A set S of natural numbers is called recursively enumerable if there is a general recursive function F(x, y) such thatIn other words, S is the projection of a two-dimensional general recursive set. Actually, it is no restriction on S to assume that F(x, y) is primitive recursive. If S is not empty, it is the range of the primitive recursive functionwhere a is a fixed element of S. Using pairing functions, we see that any non-empty recursively enumerable set is also the range of a primitive recursive function of one variable.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, except as otherwise noted.Martin Davis has shown that every recursively enumerable set S of natural numbers can be represented in the formwhere P(y, b, w, x1 …, xλ) is a polynomial with integer coefficients. (Notice that this would not be correct if we replaced ≤ by <, since the right side of the equivalence would always be satisfied by b = 0.) Conversely, every set S represented by a formula of the above form is recursively enumerable. A basic unsolved problem is whether S can be defined using only existential quantifiers.

scholarly journals About the proof-theoretic ordinals of weak fixed point theories

1992 ◽  
Vol 57 (3) ◽  
pp. 1108-1119 ◽  
Author(s):  
Gerhard Jäger ◽  
Barbara Primo
Keyword(s):  
Fixed Point ◽  
Number Theory ◽  
Second Order ◽  
Order Number ◽  
Natural Numbers

AbstractThis paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.

A derivation of number theory from ancestral theory

1952 ◽  
Vol 17 (3) ◽  
pp. 192-197 ◽  
Author(s):  
John Myhill
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Class Inclusion ◽  
First Order ◽  
Free Variables

Martin has shown that the notions of ancestral and class-inclusion are sufficient to develop the theory of natural numbers in a system containing variables of only one type.The purpose of the present paper is to show that an analogous construction is possible in a system containing, beyond the quantificational level, only the ancestral and the ordered pair.The formulae of our system comprise quantificational schemata and anything which can be obtained therefrom by writing pairs (e.g. (x; y), ((x; y); (x; (y; y))) etc.) for free variables, or by writing ancestral abstracts (e.g. (*xyFxy) etc.) for schematic letters, or both.The ancestral abstract (*xyFxy) means what is usually meant by ; and the formula (*xyFxy)zw answers to Martin's (zw; xy)(Fxy).The system presupposes a non-simple applied functional calculus of the first order, with a rule of substitution for predicate letters; over and above this it has three axioms for the ancestral and two for the ordered pair.

A finite arithmetic

1973 ◽  
Vol 38 (2) ◽  
pp. 232-248 ◽  
Author(s):  
Philip T. Shepard
Keyword(s):  
Number Theory ◽  
Natural Number ◽  
Singular Term ◽  
New Method ◽  
Axiomatic System ◽  
Natural Numbers ◽  
Substantial Loss ◽  
First Order ◽  
Finite Arithmetic

In this paper I shall argue that the presumption of infinitude may be excised from the area of mathematics known as natural number theory with no substantial loss. Except for a few concluding remarks, I shall restrict my concern in here arguing the thesis to the business of constructing and developing a first-order axiomatic system for arithmetic (called ‘FA’ for finite arithmetic) that contains no theorem to the effect that there are infinitely many numbers.The paper will consist of five parts. Part I characterizes the underlying logic of FA. In part II ordering of natural numbers is developed from a restricted set of axioms, induction schemata are proved and a way of expressing finitude presented. A full set of axioms are used in part III to prove working theorems on comparison of size. In part IV an ordinal expression is defined and characteristic theorems proved. Theorems for addition and multiplication are derived in part V from definitions in terms of the ordinal expression of part IV. The crucial final constructions of part V present a new method of replacing recursive characterizations by strict definitions.In view of our resolution not to assume that there are infinitely many numbers, we shall have to deal with the situation where singular arithmetic terms of FA may fail to refer. For I know of no acceptable and systematic way of avoiding such situations. As a further result, singular-term instances of universal generalizations of FA are not to be inferred directly from the generalizations themselves. Nevertheless, (i) (x)(y)(x + y = y + x), for example, and all its instances are provable in FA.

Solution of a problem of Leon Henkin

1955 ◽  
Vol 20 (2) ◽  
pp. 115-118 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Formal System ◽  
Free Variable ◽  
Formal Proof ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Order Predicate Calculus

If Σ is any standard formal system adequate for recursive number theory, a formula (having a certain integer q as its Gödel number) can be constructed which expresses the proposition that the formula with Gödel number q is provable in Σ. Is this formula provable or independent in Σ? [2].One approach to this problem is discussed by Kreisel in [4]. However, he still leaves open the question whether the formula (Ex)(x, a), with Gödel-number a, is provable or not. Here (x, y) is the number-theoretic predicate which expresses the proposition that x is the number of a formal proof of the formula with Gödel-number y.In this note we present a solution of the previous problem with respect to the system Zμ [3] pp. 289–294, and, more generally, with respect to any system whose set of theorems is closed under the rules of inference of the first order predicate calculus, and satisfies the subsequent five conditions, and in which the function (k, l) used below is definable.The notation and terminology is in the main that of [3] pp. 306–326, viz. if is a formula of Zμ containing no free variables, whose Gödel number is a, then ({}) stands for (Ex)(x, a) (read: the formula with Gödel number a is provable in Zμ); if is a formula of Zμ containing a free variable, y say, ({}) stands for (Ex)(x, g(y)}, where g(y) is a recursive function such that for an arbitrary numeral the value of g() is the Gödel number of the formula obtained from by substituting for y in throughout. We shall, however, depart trivially from [3] in writing (), where is an arbitrary numeral, for (Ex){x, ).

Sign in / Sign up

Export Citation Format

Share Document