TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS
Makoto Tatsuta · International Journal of Foundations of Computer Science · 1994
Realizability of monotone inductive definitions is studied to construct a logical system in which recursive data structures and recursive control structures of programs are naturally formalized by using inductive definitions and programs can be produced from constructive proofs by using realizability. Two q-realizability interpretations of monotone inductive definitions are presented. One interpretation is defined so that a realizer of an inductively defined predicate is the same as a realizer of its expansion. It is proved that the interpretation of restricted monotone inductive definitions is sound and that the interpretation of full monotone inductive definitions is not sound, though the interpretation seems very natural. Another interpretation is presented by using the higher order coding and q-realizability for the second order logic. The soundness of this interpretation of full monotone inductive definitions is also proved. To prove this result, greatest-lower-bound inductive definitions are introduced.