Confined modified realizability
Gilda Ferreira, Paulo B. Oliva · Mathematical logic quarterly · 2010
Abstract We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with (a weak version of) our interpretation in the case when least elements exist (e.g. natural numbers). The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well‐founded (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)