General Recursive Realizability and Basic Logic
- PDF / 292,458 Bytes
- 18 Pages / 594 x 792 pts Page_size
- 0 Downloads / 190 Views
Algebra and Logic, Vol. 59, No. 5, November, 2020 (Russian Original Vol. 59, No. 5, September-October, 2020)
GENERAL RECURSIVE REALIZABILITY AND BASIC LOGIC A. Yu. Konovalov∗
UDC 510.64
Keywords: realizability, absolute realizability, subrecursive realizability, basic logic. The notion of general recursive realizability is defined based on using indices of general recursive functions as a constructive way of obtaining some realizations from others. The soundness of basic logic with respect to the semantics of general recursive realizability is proved.
INTRODUCTION The notion of recursive realizability goes back to Kleene [1], who suggested an interpretation of some specific intuitionistic notions based on the algorithm theory concept. Propositional and predicate logics of Kleene’s recursive realizability have been studied since the 1950s. Behind recent versions of realizability are different kinds of subrecursive realizability. These are primitive recursive realizability [2, 3] and minimal realizability [4]. The respective predicate logics can be found in [5-8]. Other kinds of subrecursive realizability are also of interest. In this paper, the notion of general recursive realizability is being developed based on using indices of general recursive functions as a constructive way of obtaining some realizations from others. The soundness of basic logic [9] with respect to the semantics of general recursive realizability is proved. Previously, a similar result was obtained for primitive recursive realizability [10] and realizability cases based on arithmetic [11, 12] and hyperarithmetic computability [13]. ∗
Supported by RFBR, project No. 20-01-00670.
Lomonosov Moscow State University, Moscow, Russia; [email protected]. Translated from Algebra i Logika, Vol. 59, No. 5, pp. 542-566, September-October, 2020. Russian DOI: 10.33048/ alglog.2020.59.503. Original article submitted August 21, 2019; accepted November 27, 2020.
c 2020 Springer Science+Business Media, LLC 0002-5232/20/5905-0367
367
1. NUMBERING OF GENERAL RECURSIVE FUNCTIONS Let us fix a computable numbering of all n-ary partial recursive functions: ϕn1 , ϕn2 , . . . for every natural number n. Consider the corresponding numbering of general recursive functions, defining the set of indices In {e | ϕne is a general recursive function}. Thus, if z ∈ In , then ϕnz is an n-ary general recursive function, and conversely, every n-ary general recursive function coincides with ϕnz for some z ∈ In . In what follows, we will omit the superscript of the function ϕnz if it is clear from the context. PROPOSITION 1. A set of general recursive functions together with the above numbering has the following properties: —all primitive recursive functions are general recursive functions (PRF); —if ψ is an n-ary general recursive function and s is a permutation on the set {1, . . . , n}, then the function ψ defined by the conditional equality ψ (x1 , . . . , xn ) ψ(xs(1) , . . . , xs(n) ) is a general recursive function (PV); —if ψ is an n-ary general recursiv
Data Loading...
