TY - JOUR AU - Oosten, Jaap van PY - 1996/01/03 Y2 - 2024/03/28 TI - The Modified Realizability Topos JF - BRICS Report Series JA - BRICS VL - 3 IS - 3 SE - Articles DO - 10.7146/brics.v3i3.19966 UR - https://tidsskrift.dk/brics/article/view/19966 SP - AB - The modified realizability topos is the semantic (and higher order) counterpart of a variant of Kreisel's modified realizability (1957). These years, this realizability has been in the limelight again because of its possibilities for modelling type theory (Streicher, Hyland-Ong-Ritter) and strong normalization. <br />In this paper this topos is investigated from a general logical and topostheoretic point of view. It is shown that Mod (as we call the topos) is the closed complement of the effective topos inside another one; this turns out to have some logical consequences. Some important subcategories of Mod are described, and a general logical principle is derived, which holds in the larger topos and implies the well-known Independence of Premiss principle. ER -