It is proved in this paper that the predicate logic of each complete constructive arithmetic theory T having the existential property is Π1T-complete. In this connection, the techniques of a uniform partial truth definition for intuitionistic arithmetic theories is used. The main theorem is applied to the characterization of the predicate logic corresponding to certain variant of the notion of realizable predicate formula. Namely, it is shown that the set of irrefutable predicate formulas is recursively isomorphic to the complement of (...) the set ︀. The notion of Σn-realizability is defined on the basis of the notion of Σn-function. It is proved that the predicate logic of Σn-realizability is Πω+1-hard. (shrink)

The study of propositional realizability logic was initiated in the 50th of the last century. Some interesting results were obtained in the 60-70th. but many important problems in this area are still open. Now interest to these problems from new generation of researchers is observed. This survey contains an exposition of the results on propositional realizability logic and corresponding techniques. Thus reading this paper can be the start point in exploring and development of constructive logic.

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. (shrink)