Relating Kripke models and realizability
James Lipton · Medical Entomology and Zoology · 1990
The principal undertaking of this thesis is to investigate, as constructively as possible some of the connections between two fundamental paradigms of intuitionistic semantics: Kripke-Beth models, and generalizations thereof, and realizability interpretations. The former captures truth-value semantics for constructive reasoning, the latter semantics based on evidence: codes, proofs, or recursive indices that attest to the truth of logical statements. Connections between these two ideas have been investigated by Hyland in the realizability to Kripke model direction, and by Lauchli in the other direction. Here we explore alternatives to the former, and more constructive versions of the latter. In chapter one we construct a Kripke model for syntactic realizability for Heyting Arithmetc. In the second chapter we describe an abstract realizability interpretation (along the lines of Beeson, Feferman, Troelstra-van Dalen) and construct an elementarily equivalent Kripke model. In chapter three, using a translation of the intuitionistic completeless theorem for Beth semantics due to Veldman, de Swart, van Dalen and others, we build a family of completely constructive Beth models for a general family of realizabilities. In chapter four, a partial converse to these results is established. We show that to every countable Kripke model there corresponds an elementarily equivalent realizability notion, in which the realizers are a collection of functions which include the partial recursive functions, but are no more complex than the partial recursive functions relativized to the diagram of the Kripke model as an oracle.