Arithmetic Without the Exponential

Gödel's Incompleteness Theorems ◽

10.1093/oso/9780195046724.003.0007 ◽

1992 ◽

Author(s):

Raymond M. Smullyan

Keyword(s):

Recursive Function ◽

Function Theory ◽

Axiom System ◽

Peano Arithmetic ◽

Recursively Enumerable

§1. By an arithmetic term or formula, we mean a term or formula in which the exponential symbol E does not appear, and by an arithmetic relation (or set), we mean a relation (set) expressible by an arithmetic formula. By the axiom system P.A. (Peano Arithmetic), we mean the system P.E. with axiom schemes N10 and N11 deleted, and in the remaining axiom schemes, terms and formulas are understood to be arithmetic terms and formulas. The system P.A. is the more usual object of modern study (indeed, the system P.E. is rarely considered in the literature). We chose to give the incompleteness proof for P.E. first since it is the simpler. In this chapter, we will prove the incompleteness of P.A. and establish several other results that will be needed in later chapters. The incompleteness of P.A. will easily follow from the incompleteness of P.E., once we show that the relation xy = z is not only Arithmetic but arithmetic (definable from plus and times alone). We will first have to show that certain other relations are arithmetic, and as we are at it, we will show stronger results about these relations that will be needed, not for the incompleteness proof of this chapter, but for several chapters that follow—we will sooner or later need to show that certain key relations are not only arithmetic, but belong to a much narrower class of relations, the Σ1-relations, which we will shortly define. These relations are the same as those known as recursively enumerable. Before defining the Σ1-relations, we turn to a still narrower class, the Σ0-relations, that will play a key role in our later development of recursive function theory. §2. We now define the classes of Σ0-formulas and Σ0-relations and then the Σ1-formulas and relations. By an atomic Σ0-formula, we shall mean a formula of one of the four forms c1 + c2 = c3, c1 · c2 =c3, c1 = c2 or c1 ≤ c2, where each of c1, c2 or c3 is either a variable or a numeral (but some may be variables and others numerals).

Download Full-text

Shepherdson’s Representation Theorems

Gödel's Incompleteness Theorems ◽

10.1093/oso/9780195046724.003.0010 ◽

1992 ◽

Author(s):

Raymond M. Smullyan

Keyword(s):

Representation Theorem ◽

Recursive Function ◽

Function Theory ◽

Peano Arithmetic ◽

Alternative Proof ◽

Binary Relations ◽

Representation Theorems ◽

Strong Separation ◽

Weak Separation ◽

Th 1

We have already remarked that at the time of Gödel’s proof, the only known way of showing the set P* of Peano Arithmetic to be representable in P.A. involved the assumption of ω-consistency. Well, in 1960, A. Ehrenfeucht and S. Feferman showed that all Σ1-sets can be represented in all simply consistent axiomatizable extensions of the system (R). Hence, all Σ1-sets can be shown to be representable in P.A. under the weaker assumption that P.A. is simply consistent. Their proof combined a Rosser-type argument with a celebrated result in recursive function theory due to John Myhill which goes beyond the scope of this volume. Very shortly after, however, John Shepherdson [1961] found an extremely ingenious alternative proof that is more direct and which we study in this chapter. [In our sequel to this volume, we compare Shepherdson’s proof with the original one. The comparison is of interest in that the two methods are very different and the proofs generalize in different directions which are apparently incomparable in strength.] We recall that for each n > 1, a system S is called a Rosser system for n-ary relations if for any Σ1-relations R1(x1,..., xn) and R2(X1, ..., xn), the relation R1 — R2 is separable from R2 — R1 in S. We wish to prove the following theorem and its corollary (Th. 1 below). Theorem S1—Shepherdson’s Representation Theorem. If S is a simply consistent axiomatizable Rosser system for binary relations (n-ary relations for n = 2), then all Σ1-sets are representable in S. Theorem 1—Ehrenfeucht, Feferman. All Σ1-sets are representable in every consistent axiomatizable extension of the system (R). Shepherdson’s Lemma and Weak Separation For emphasis, we will now sometimes write “strongly separates” for “separates”. We will say that a formula F(v1) weakly separates A from B in S if F(v1) represents some superset of A disjoint from B, We showed in the last chapter (Lemma 1) that strong separation implies weak separation provided that the system S is consistent. We also say that a formula F(v1,. .. ,vn) weakly separates a relation R I (x1 , . .. ,xn) from .R2(x1,... ,xn) if F(v1, ..., vn) represents some relation R’(x1,. .. ,xn) such that R1 ⊆ R1’ and R1 is disjoint from -R2.

Download Full-text

Pseudo-complements and ordinal logics based on consistency statements

Journal of Symbolic Logic ◽

10.2307/2270451 ◽

1966 ◽

Vol 31 (3) ◽

pp. 359-364 ◽

Cited By ~ 1

Author(s):

Robert A. Di Paola

Keyword(s):

Recursive Function ◽

Peano Arithmetic ◽

Additional Property ◽

Primitive Recursive Function ◽

Recursively Enumerable ◽

Primitive Recursive

Following [1] we write {n} for the nth recursively enumerable (re) set; that is, {n} = {x|VyT(n, x, y)}. By a “pair (T, α)” we mean a consistent re extension T of Peano arithmetic P and an RE-formula α which numerates the non-logical axioms of T in P [4]. Given a pair (T, α) and a particular formula which binumerates the Kleene T predicate in P, there can be defined a primitive recursive function Nα such that and which has the additional property that {Nα(Nα(n))} = ø for all n.

Download Full-text

Recursive Enumerability and Recursivity

Recursion Theory for Metamathematics ◽

10.1093/oso/9780195082326.003.0005 ◽

1993 ◽

Author(s):

Raymond M. Smullyan

Keyword(s):

Recursive Function ◽

Function Theory ◽

Closure Properties ◽

Recursive Enumerability ◽

Recursively Enumerable ◽

Special Cases ◽

Mechanical Procedure ◽

The Subject ◽

Definition Of ◽

Intuitive Sense

Having proved that Peano Arithmetic is incomplete, we can ask another question about the system. Is there any algorithm (mechanical procedure) by which we can determine which sentences are provable in the system and which are not? This brings us to the subject of recursive function theory, to which we now turn. we are denning a relation (or set) to be r.e. (recursively enumerable) iff it is Σ1, and to be recursive iff it and its complement are r.e. An equivalent definition of recursive enumerability is represent ability in some finitely axiomatizable system (as we will prove). Many other characterizations of recursive enumerability and recursivity can be found in the literature (cf., e.g., Kleene [1952], Turing [1936], Post [1944], Smullyan [1961], Markov [1961]), but the Σ1-characterization fits in best with the overall plan of this volume. The fact that so many different and independently formulated definitions turn out to be equivalent adds support to a thesis proposed by Church—namely that any function that is effectively calculable in the intuitive sense is a recursive function. Interesting discussions of Church’s thesis can be found in Kleene [1952] and Rogers [1967]. In this chapter, we establish a few basic properties of recursive enumerability that will be needed in just about all the chapters that follow. §1. Some Closure Properties. It will be convenient to regard sets as special cases of relations (sets are thus relations of one argument or relations of degree 1). It will be convenient to use the l-notation “λx1,...,xn : (...)”, read “the set of all n-tuples (x1,..., xn) such that (...)”. For example, for any relation λ(x1, x2, x3), the relation λx1x2x3: R(x2 x2, x3) is the set of all triples (x1,x2,x3) (of natural numbers) such that R(x2,x2,x1) holds. we sometimes write “x: (. . . )” for “λx: ( . . . ) ”.

Download Full-text

Torre models in the isols

Journal of Symbolic Logic ◽

10.2307/2275256 ◽

1994 ◽

Vol 59 (1) ◽

pp. 140-150 ◽

Cited By ~ 1

Author(s):

Joseph Barback

Keyword(s):

Number Theory ◽

Structural Property ◽

Recursive Function ◽

Peano Arithmetic ◽

The Other ◽

Close Connection ◽

New Variety ◽

Nonstandard Model ◽

Recursively Enumerable ◽

Recursively Enumerable Sets

AbstractIn [14] J. Hirschfeld established the close connection of models of the true AE sentences of Peano Arithmetic and homomorphic images of the semiring of recursive functions. This fragment of Arithmetic includes most of the familiar results of classical number theory. There are two nice ways that such models appear in the isols. One way was introduced by A. Nerode in [20] and is referred to in the literature as Nerode Semirings. The other way is called a tame model. It is very similar to a Nerode Semiring and was introduced in [6]. The model theoretic properties of Nerode Semirings and tame models have been widely studied by T. G. McLaughlin ([16], [17], and [18]).In this paper we introduce a new variety of tame model called a torre model. It has as a generator an infinite regressive isol with a nice structural property relative to recursively enumerable sets and their extensions to the isols. What is then obtained is a nonstandard model in the isols of the fragment of Peano Arithmetic with the following property: Let T be a torre model. Let f be any recursive function, and let fΛ be its extension to the isols. If there is an isol A with fΛ(A) ϵ T, then there is also an isol B ϵ T with fΛ(B) = fΛ(A).

Download Full-text

Interpretability over peano arithmetic

Journal of Symbolic Logic ◽

10.2307/2586787 ◽

1999 ◽

Vol 64 (4) ◽

pp. 1407-1425

Author(s):

Claes Strannegård

Keyword(s):

Modal Logic ◽

Completeness Theorem ◽

Peano Arithmetic ◽

Embedding Theorem ◽

Compactness Theorem ◽

Partial Answer ◽

Recursively Enumerable ◽

Recursively Enumerable Sets ◽

Interpretability Logic

AbstractWe investigate the modal logic of interpretability over Peano arithmetic. Our main result is a compactness theorem that extends the arithmetical completeness theorem for the interpretability logic ILMω. This extension concerns recursively enumerable sets of formulas of interpretability logic (rather than single formulas). As corollaries we obtain a uniform arithmetical completeness theorem for the interpretability logic ILM and a partial answer to a question of Orey from 1961. After some simplifications, we also obtain Shavrukov's embedding theorem for Magari algebras (a.k.a. diagonalizable algebras).

Download Full-text