Ferreira, GildaFirmino, Paulo2024-04-112024-04-112024-04-04Ferreira, G., Firmino, P. Herbrandized modified realizability. Arch. Math. Logic (2024). https://doi.org/10.1007/s00153-024-00917-6http://hdl.handle.net/10400.2/15924Realizability notions in mathematical logic have a long history, which can be tracedback to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations ofintuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticatednotions such as Kreisel’s modified realizability and various modern approaches. Inthis context, our work aligns with the lineage of realizability strategies that emphasizethe accumulation, rather than the propagation of precise witnesses. In this paper, weintroduce a new notion of realizability, namely herbrandized modified realizability.This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, whichenables the gathering of witnesses into nonempty finite sets. We also show that theprevious analysis can be extended from logic to (Heyting) arithmetic.engRealizabilityStar combinatory calculusFinite setsIntuitionisticlogicHeyting arithmeticjournal article10.1007/s00153-024-00917-6