Polynomially and superexponentially shorter proofs in fragments of arithmetic

1992 ◽  
Vol 57 (3) ◽  
pp. 844-863 ◽  
Author(s):  
Franco Montagna
Keyword(s):  
Fixed Points ◽  
Recursive Function ◽  
Peano Arithmetic ◽  
Modal Language ◽  
Primitive Recursive Function ◽  
Consistent Extension ◽  
Image Position ◽  
Primitive Recursive ◽  
Increasing Function

In Parikh [71] it is shown that, if T is an r.e. consistent extension of Peano arithmetic PA, then, for each primitive recursive function g, there is a formula φ of PA such that(In the following, Proof T(z, φ) and Prov T(φ) denote the metalinguistic assertions that z codes a proof of φ in T and that φ is provable in T respectively, where ProofT(z, ┌φ┐) and ProvT(┌φ┐) are the formalizations of Proof T(z,φ) and ProvT(φ) respectively in the language of PA, ┌φ┐ denotes the Gödel number of φ and ┌φ┐ denotes the corresponding numeral. Also, for typographical reasons, subscripts will not be made boldface.) If g is a rapidly increasing function, we express (1) by saying that ProvT(┌φ┐) has a much shorter proof modulo g than φ. Parikh's result is based on the fact that a suitable formula A(x), roughly asserting that (1) holds with x in place of φ, has only provable fixed points. In de Jongh and Montagna [89], this situation is generalized and investigated in a modal context. There, a characterization is given of arithmetical formulas arising from modal formulas of a suitable modal language which have only provable fixed points, and Parikh's result is obtained as a particular case.

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.

Pseudo-complements and ordinal logics based on consistency statements

1966 ◽  
Vol 31 (3) ◽  
pp. 359-364 ◽  
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.

PROVABILITY LOGICS RELATIVE TO A FIXED EXTENSION OF PEANO ARITHMETIC

2018 ◽  
Vol 83 (3) ◽  
pp. 1229-1246
Author(s):  
TAISHI KURAHASHI
Keyword(s):  
Peano Arithmetic ◽  
Provability Logic ◽  
Consistent Extension ◽  
Image Position ◽  
Computably Enumerable

AbstractLet T and U be any consistent theories of arithmetic. If T is computably enumerable, then the provability predicate $P{r_\tau }\left( x \right)$ of T is naturally obtained from each ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of T. The provability logic $P{L_\tau }\left( U \right)$ of τ relative to U is the set of all modal formulas which are provable in U under all arithmetical interpretations where □ is interpreted by $P{r_\tau }\left( x \right)$. It was proved by Beklemishev based on the previous studies by Artemov, Visser, and Japaridze that every $P{L_\tau }\left( U \right)$ coincides with one of the logics $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α and β are subsets of ω and β is cofinite.We prove that if U is a computably enumerable consistent extension of Peano Arithmetic and L is one of $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α is computably enumerable and β is cofinite, then there exists a ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of some extension of $I{{\rm{\Sigma }}_1}$ such that $P{L_\tau }\left( U \right)$ is exactly L.

The recursive irrationality of π

1954 ◽  
Vol 19 (4) ◽  
pp. 267-274 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Real Number ◽  
Recursive Function ◽  
Present Note ◽  
Rational Numbers ◽  
Negative Integer ◽  
Exponential Series ◽  
General Recursive Function ◽  
Recursive Sequence ◽  
Image Position ◽  
Primitive Recursive

A primitive-recursive sequence of rational numbers sn is said to be primitive-recursively irrational, if there are primitive recursive functions n(k), i(p, q) > 0 and N(p, q) such that:1. (k)(n ≥ n(k) → ∣sn – sn(k)∣ < 2−k).2. (p)(q)(q > 0 & n ≥ N(p, q) → ∣sn ± p/q∣ > 1/i(p, q)).The object of the present note is to establish the primitive-recursive irrationality of a sequence which converges to π. In a previous paper we proved the primitive-recursive irrationality of the exponential series Σxn/n!, for all rational values of x, and showed that a primitive-(general-) recursively irrational sequence sn is strongly primitive-(general-)recursive convergent in any scale, where a recursive sequence sn is said to be strongly primitive-(general-)recursive convergent in the scale r (r ≥ 2), if there is a non-decreasing primitive-(general-) recursive function r(k) such that,where [x] is the greatest integer contained in x, i.e. [x] = i if i ≤ x < i + 1, [x] = —i if i ≤ —x < i+1, where i is a non-negative integer.A rational recursive sequence sn is said to be recursive convergent, if there is a recursive function n(k) such that.If a sequence sn is strongly recursive convergent in a scale r, then it is recursive convergent and its limit is the recursive real number where, for any k ≥ 0,.

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

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.

scholarly journals Non-primitive Recursive Function Definitions

1995 ◽  
Vol 2 (36) ◽  
Author(s):  
Sten Agerholm
Keyword(s):  
Recursive Function ◽  
Higher Order ◽  
Order Logic ◽  
Domain Theory ◽  
Higher Order Logic ◽  
Primitive Recursive Function ◽  
Primitive Recursive

This paper presents an approach to the problem of introducing<br />non-primitive recursive function definitions in higher order logic. A<br />recursive specification is translated into a domain theory version, where<br />the recursive calls are treated as potentially non-terminating. Once we<br />have proved termination, the original specification can be derived easily.<br />A collection of algorithms are presented which hide the domain theory<br />from a user. Hence, the derivation of a domain theory specification<br />has been automated completely, and for well-founded recursive function<br />specifications the process of deriving the original specification from the<br />domain theory one has been automated as well, though a user must<br />supply a well-founded relation and prove certain termination properties<br />of the specification. There are constructions for building well-founded<br />relations easily.

Sign in / Sign up

Export Citation Format

Share Document