nLab realizer

Idea

A formula is true in a model if it has a realizer in the model, and a formula is valid if it has a realizer in every model.

References

  • Steven Cole Kleene, on the interpretation of intuitionistic number theory, JSL, 10:109-124, 1945

  • Igor Privara, Branislav Rovan, Peter Ruzicka (eds.), lecture notes in computer science, 841, google books, chapter 5 realizability models, p.93

  • Thomas Streicher, Realizability Models for CZF+¬PowCZF + \neg Pow, unpublished note. In this note WISC is called TTCA fTTCA_f (TTCATTCA stands for “type-theoretic collection axiom).

Created on May 12, 2012 at 15:23:57. See the history of this page for a list of all contributions to it.