Herbrandized modified realizability

Ferreira, Gilda; Firmino, Paulo

http://hdl.handle.net/10400.2/15924

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
Ferreira_et_al-2024-Archive_for_Mathematical_Logic.pdf		301.49 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Gilda

Firmino, Paulo

Abstract(s)

Realizability 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.