The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy intuitionistic logic, however this method was extended by Krivine to produce models which satisfy full classical logic and even Zermelo Fraenkel set theory with choice. The purpose of these notes is to produce a modified formalisation of Krivine's theory of realizability using a class of names for elements of the realizability model. It is also discussed how Krivine's method relates to the notions of intuitionistic realizability, double negation translations and the theory of forcing.

翻译：可实现性方法最初由克林提出，被视为从数学证明中提取计算内容的一种方式。传统上，这些模型仅满足直觉主义逻辑，但克里维纳对此方法进行了扩展，构建出满足完全经典逻辑甚至包含选择公理的策梅洛-弗兰克尔集合论的模型。本文旨在通过引入一类用于表示可实现性模型中元素的名字，对克里维纳的可实现性理论提出改良形式化表述。同时探讨了克里维纳方法如何与直觉主义可实现性、双重否定翻译以及力迫理论等概念相关联。