Abstract:
The notion of primitive recursive realizability was introduced
by S. Salehi as a kind of semantics for the language of basic arithmetic
using primitive recursive functions. It is of interest to study
the corresponding predicate logic. D. A. Viter proved that the predicate
logic of primitive recursive realizability by Salehi is not arithmetical.
The technically complex proof combines the methods used by the author
of this article in the study of predicate logics of constructive arithmetic
theories and the results of M. Ardeshir on the translation of
the intuitionistic predicate logic into the basic predicate logic.
The purpose of this article is to present another proof of Viter's result
by directly transferring the methods used earlier in proving
the nonarithmeticity of the predicate logic of recursive realizability.
Fulltext:
PDF file (734 kB)
