THE NONARITHMETICITY OF THE PREDICATE LOGIC OF STRICTLY PRIMITIVE RECURSIVE REALIZABILITY

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.