Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-20T05:18:12.343Z Has data issue: false hasContentIssue false
  • English
  • Français

THE NONARITHMETICITY OF THE PREDICATE LOGIC OF STRICTLY PRIMITIVE RECURSIVE REALIZABILITY

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  19 April 2021

VALERY PLISKO
VALERY PLISKO*
Affiliation:
FACULTY OF MECHANICS AND MATHEMATICS MOSCOW STATE UNIVERSITY GSP-1, 1 LENINSKIYE GORY, MOSCOW, RUSSIAE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A notion of strictly primitive recursive realizability is introduced by Damnjanovic in 1994. It is a kind of constructive semantics of the arithmetical sentences using primitive recursive functions. It is of interest to study the corresponding predicate logic. It was argued by Park in 2003 that the predicate logic of strictly primitive recursive realizability is not arithmetical. Park’s argument is essentially based on a claim of Damnjanovic that intuitionistic logic is sound with respect to strictly primitive recursive realizability, but that claim was disproved by the author of this article in 2006. The aim of this paper is to present a correct proof of the result of Park.

Keywords

constructive semanticsrealizabilityprimitive recursive functionspredicate logicnonarithmeticity

MSC classification

Primary: 03F50: Metamathematics of constructive systems
Type
Research Article
Information
The Review of Symbolic Logic , Volume 15 , Issue 3 , September 2022 , pp. 693 - 721
Copyright
© The Author(s), 2021. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Axt, P. (1963). Enumeration and the Grzegorczyk hierarchy. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 9, 53–65.CrossRefGoogle Scholar
Damnjanovic, Z. (1994). Strictly primitive recursive realizability. I. Journal of Symbolic Logic, 59, 1210–1227.CrossRefGoogle Scholar
Grzegorczyk, A. (1953). Some classes of recursive functions. Rozprawy matematyczne, 4, 1–46.Google Scholar
Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10, 109–124.CrossRefGoogle Scholar
Kleene, S. C. (1952). Introduction to Metamathematics. Bibliotheca Mathematica, Vol. 1. Amsterdam: North-Holland Publishing.Google Scholar
Kleene, S. C. (1958). Extension of an effectively generated class of functions by enumeration. Colloquium Mathematicum, 6, 67–78.CrossRefGoogle Scholar
Park, B. H. (2003). Subrecursive Realizability and Predicate Logic. Ph.D. Thesis, Moscow State University, Russia.Google Scholar
Plisko, V. (2006a). On primitive recursive realizabilities. In Grigoriev, D., Harrison, J., and Hirsch, E. A., editors. Computer Science—Theory and Applications. Lecture Notes in Computer Science, Vol. 3967. Berlin and Heidelberg: Springer, pp. 304–312.CrossRefGoogle Scholar
Plisko, V. (2006b). On the relation between two notions of primitive recursive realizability. Vestnik Moskovskogo Universiteta. Seriya 1. Matematika. Mekhanika, 1, 6–11 (in Russian).Google Scholar
Plisko, V. (2007). Primitive Recursive Realizability and Basic Propositional Logic, Utrecht University. Logic Group Preprint Series, Vol. 261, 1–27.Google Scholar
Plisko, V. E. (1977). The nonarithmeticity of the class of realizable predicate formulas. Soviet Mathematics Izvestija, 11, 453–471.CrossRefGoogle Scholar
Salehi, S. (2003). Provably total functions of basic arithmetic. Mathematical Logic Quarterly, 49(3), 316–322.CrossRefGoogle Scholar