Herbrandized modified realizability

Ferreira, Gilda; Firmino, Paulo

Publication

Herbrandized modified realizability

2024-04-04Journal article

datacite.subject.sdg	04:Educação de Qualidade	pt_PT
dc.contributor.author	Ferreira, Gilda
dc.contributor.author	Firmino, Paulo
dc.date.accessioned	2024-04-11T10:29:40Z
dc.date.available	2024-04-11T10:29:40Z
dc.date.issued	2024-04-04
dc.description.abstract	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.	pt_PT
dc.description.sponsorship	The authors are grateful to Fernando Ferreira for interesting discussions on the topic. They extend their gratitude to the anonymous referee for providing valuable suggestions, which inspired the addition of Sect. 4.3 to the manuscript. Both authors acknowledge the support of Fundação para a Ciência e a Tecnologia under the Projects: UIDB/04561/2020, UIDB/00408/2020 and UIDP/00408/2020 and are also grateful to Centro de Matemática, Aplicações Fundamentais e Investigação Operacional (Universidade de Lisboa). The first author is also grateful to LASIGE - Computer Science and Engineering Research Centre Herbrandized modified realizability (Universidade de Lisboa). The second author also benefitted from Fundação para a Ciência e a Tecnologia doctoral Grant 2022.12585.BD.	pt_PT
dc.description.version	info:eu-repo/semantics/publishedVersion	pt_PT
dc.identifier.citation	Ferreira, G., Firmino, P. Herbrandized modified realizability. Arch. Math. Logic (2024). https://doi.org/10.1007/s00153-024-00917-6	pt_PT
dc.identifier.doi	10.1007/s00153-024-00917-6	pt_PT
dc.identifier.uri	http://hdl.handle.net/10400.2/15924
dc.language.iso	eng	pt_PT
dc.peerreviewed	yes	pt_PT
dc.publisher	Springer	pt_PT
dc.relation.publisherversion	https://rdcu.be/dDJK8	pt_PT
dc.rights.uri	http://creativecommons.org/licenses/by/4.0/	pt_PT
dc.subject	Realizability	pt_PT
dc.subject	Star combinatory calculus	pt_PT
dc.subject	Finite sets	pt_PT
dc.subject	Intuitionisticlogic	pt_PT
dc.subject	Heyting arithmetic	pt_PT
dc.title	Herbrandized modified realizability	pt_PT
dc.type	journal article
dspace.entity.type	Publication
oaire.citation.title	Archive for Mathematical Logic	pt_PT
person.familyName	Ferreira
person.givenName	Gilda
person.identifier.ciencia-id	0B1A-81E7-88B1
person.identifier.orcid	0000-0003-1447-9764
person.identifier.rid	H-9953-2013
person.identifier.scopus-author-id	14037466100
rcaap.rights	openAccess	pt_PT
rcaap.type	article	pt_PT
relation.isAuthorOfPublication	fd3a6c7d-42b2-4434-834f-fb161900c938
relation.isAuthorOfPublication.latestForDiscovery	fd3a6c7d-42b2-4434-834f-fb161900c938