Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Realizability and Kripke Forcing

Realizability and Kripke Forcing

File(s)
90-1163.pdf (2.73 MB)
90-1163.ps (642.94 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7003
Collections
Computer Science Technical Reports
Author
Lipton, James
Abstract

Realizability, developed by Stephen Kleene, is a type-free device for extracting computations from logical specifications. Realizability analyzes the computational content of reasoning: it models the universe of recursive mathematics. Kripke and associated Categorical interpretations give a broader, topological/algebraic semantics for constructive reasoning which is complete for intuitionistic logic. They are, therefore, a powerful and indispensable tool for modelling computationally meaningful formal systems. How are the two semantical paradigms related ? In this paper, we construct several Kripke and Categorical Models which are elementarily equivalent to Syntactic Realizability. By merging the two approaches we provide a new class of models and a framework for reasoning about computational evidence and the process of term extraction itself.

Date Issued
1990-10
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1163
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance