Arithmetical realizability and basic logic

Absolute arithmetical realizability of predicate formulas is introduced. It is proved that the intuitionistic logic is not correct with this semantics, but the basic logic is correct.     

Continued fractions of primitive recursive real numbers

A theorem, proven in the present author's Master's thesis 2 states that a real number is ‐computable, whenever its continued fraction is in (the third Grzegorczyk class). The aim of this paper is to settle the matter with the converse of this theorem. It turns out that there exists a real number, which is ‐computable, but its continued fraction is not primitive recursive, let alone in . A question arises, whether some other natural condition on the real number can be combined with ‐computability, so that its continued fraction has low complexity. We give two such conditions. The first is ‐irrationality, based on a notion of Péter, and the second is polynomial growth of the terms of the continued fraction. Any of these two conditions, combined with ‐computability gives an (elementary) continued fraction. We conclude that all irrational algebraic real numbers and the number π have continued fractions in . All these results are generalized to higher levels of Grzegorczyk's hierarchy as well.     

Class of algebras of primitive recursive functions

In this paper Robinson's algebra is embedded in a countable class of algebras of primitive recursive functions. Each algebra of this class contains the operations of addition and composition of functions and also one of the operations i_a which are defined as follows: g(x)= i _a f(x) (a=0, 1, 2, ...) if g(x) satisfies the equations g(0)=a and g(x+1)=f[g(x)]. In this paper we study the properties possessed by all or almost all the algebras of this class.Translated from Matematicheskie Zametki, Vol. 14, No. 1, pp. 143–156, July, 1973.     

The first example of a recursive function which is not primitive recursive

The first example of a recursive function which is not primitive recursive is usually attributed to W. Ackermann. The authors of the present paper show that such an example can also be found in a paper by G. Sudan, published concomitantly with Ackermann's paper.     

Sharp thresholds for the phase transition between primitive recursive and Ackermannian Ramsey numbers

We compute the sharp thresholds on g at which g-large and g-regressive Ramsey numbers cease to be primitive recursive and become Ackermannian.We also identify the threshold below which g-regressive colorings have usual Ramsey numbers, that is, admit homogeneous, rather than just min-homogeneous sets.     

A restricted computation model on Scott domains and its partial primitive recursive functionals

The paper builds on both a simply typed term system and a computation model on Scott domains via so-called parallel typed while programs (PTWP). The former provides a notion of partial primitive recursive functional on Scott domains supporting a suitable concept of parallelism. Computability on Scott domains seems to entail that Kleene's schema of higher type simultaneous course-of-values recursion (scvr) is not reducible to partial primitive recursion. So extensions and PTWP are studied that are closed under scvr. The twist are certain type 1 G?del recursors for simultaneous partial primitive recursion. Formally, denotes a function , however, is modelled such that is finite, or in other words, a partial sequence. As for PTWP, the concept of type writable variables is introduced, providing the possibility of creating and manipulating partial sequences. It is shown that the PTWP-computable functionals coincide with those definable in plus a constant for sequential minimisation. In particular, the functionals definable in denoted can be characterised by a subclass of PTWP-computable functionals denoted . Moreover, hierarchies of strictly increasing classes in the style of Heinermann and complexity classes are introduced such that . These results extend those for and PTWP [Nig94]. Finally, scvr is employed to define for each type the enumeration functional of all finite elements of . Received January 30, 1996     

Proof-functional connectives and realizability

The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a type assignment system, a realizability semantics, and a completeness theorem. This form of completeness implies the semantic completeness of the type assignment system.     

On hyperarithmetical realizability

The notion of hyperarithmetical realizability is introduced for various extensions of the language of formal arithmetic. The correctness of classical, intuitionistic, and basic logic with respect to the semantics based on hyperarithmetical realizability is studied.     

Confined modified realizability

We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with (a weak version of) our interpretation in the case when least elements exist (e.g. natural numbers). The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well‐founded (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A recursive basis for primitive forms in symplectic spaces and applications to Heisenberg groups

This paper is divided in two parts: in Section 2, we define recursively a privileged basis of the primitive forms in a symplectic space(V~(2n), ω). Successively, in Section 3, we apply our construction in the setting of Heisenberg groups H~n, n ≥ 1, to write in coordinates the exterior differential of the so-called Rumin's complex of differential forms in H~n.     

How to prove that two classes of simple primitive recursive functions are distinct

Let X, Y be classes of primitive recursive functions (for short PRF) and let it be required to prove the following statement: (I) It is not true that every function of class X belongs to class Y. Such an assertion is usually proved by exhibiting a PRF of class X which grows faster than any PRF of class Y, or by constructing some simple PRF's, e.g., x(x + 1); xy(x + y), from class X, which do not belong to class Y. A method is proposed which gives a proof of an assertion of type (I) for some classes of PRF's X and Y such that first, functions of class X do not increase faster than functions of class Y, and second, the class Y contains simple PRF's such as xy(x + y), xy(x–y), etc. The proposed method is as follows. We choose some class of PRF's Z and for each PRF f we construct an operation _f on the functions of the class Z such that for every f in Y, the class Z is closed with respect to the operation f, but on the other hand it is not true that for every f of X the class Z is closed with respect to _f. We describe one of the possible applications of the method. We shall not distinguish between word and number PRF's and predicates, bearing in mind the following one-to-one correspondence between words in the alphabet {1, 2} and natural numbers: the word a_na_n–1... a₁a₀ in the alphabet {1, 2} corresponds to the number . Let (x, i) equal the i-th letter in the word x (the last letter-is taken to be the 0-th sign), ¦x¦ is the length of x; con(x, y) is the result of concatenating the word y to the right of the word x; , ¯ are the characteristic functions of equality and inequality. Let RF be a class of PRF's obtained from the PRF's , ¯, con, x0, , I _k ⁿ , by the operation of bounded minimalization and composition of functions. We note that the class of relations of the class RF is equal to the class of rudimentary relations. Let R_sF(f₁, ..., f_l) be a class of PRF's obtained from the PRF's f₁, ..., f_l by the operation of composition and the operation of putting into correspondence with the function g an f such that , where tPy t is the subword y. We note that the characteristic function of every s-rudimentary predicate belongs to R_sF(, , con, x0, , I _k ⁿ ). We take as Z the class of such in RF which have the values 0, 1, 2 and if then . The operation _f is such that . Assertions of type (I) can be proved by the proposed method if for X we take RF, and as Y we take , where f and g belong to the class RF.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 68, pp. 115–122, 1977.     

A non-well-founded primitive recursive tree provably well-founded for co-r.e. sets

 We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ₁ ⁰. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ₁ ⁰, equals the limit of all recursive ordinals ω₁ ^ck . RID="ID=" <E5>Mathematics Subject Classification (2000):&ensp;03B30</E5>, 03F15 RID="ID=" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium f&uuml;r Bildung, Wissenschaft, Forschung und Technologie. RID="ID=" I would like to thank A. SETZER for his hospitality during my stay in Uppsala in December 1998 &ndash; these investigations are inspired by a discussion with him; S. BUSS for his hospitality during my stay at UCSD and for valuable remarks on a previous version of this paper; and M. M&Ouml;LLERFELD for remarks on a previous title. Received: 27 July 2000 / Published online: 25 February 2002 RID=" ID=" <E5>Mathematics Subject Classification (2000):&ensp;03B30</E5>, 03F15 RID=" ID=" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium f&uuml;r Bildung, Wissenschaft, Forschung und Technologie. RID=" ID=" I would like to thank A. SETZER for his hospitality during my stay in Uppsala in December 1998 &ndash; these investigations are inspired by a discussion with him; S. BUSS for his hospitality during my stay at UCSD and for valuable remarks on a previous version of this paper; and M. M&Ouml;LLERFELD for remarks on a previous title.