22 documents found, page 1 of 3
Herbrandized modified realizability
Ferreira, Gilda; Firmino, PauloRealizability 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 strateg...
Lisbon young mathematicians conference 2023: book of abstracts
Serranho, Pedro; Cipriano, Fernanda; Ferreira, Gilda; Gonçalves, Carlota; Grossinho, M. Rosário; Oliveira, M. Rosário; Ramos, Maria do RosárioBook of Abstracts of the Lisbon Young Mathematicians Conference 2023, held in Universidade Aberta at April 14-15, 2023
Typability and type inference in atomic polymorphism
Protin, M. Clarence; Ferreira, GildaIt is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fa...
The Russell-Prawitz embedding and the atomization of universal instantiation
Espírito Santo, José; Ferreira, GildaGiven the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (i) they help achieving strict simulation of proof reduction by means of the Russell–Prawitz embedding of ...
Impact of chronic use of antimalarials on SARS-CoV-2 infection in patients with...
Gomides, Ana; Ferreira, Gilda; Kakehasi, Adriana; Lacerda, Marcus; Marques, Cláudia; Mota, Licia Maria Henrique da; Paiva, Eduardo; Pileggi, GecilmaraBackground: COVID-19, caused by the virus SARS-CoV-2, has brought extensive challenges to the scientific community in recent months. Several studies have been undertaken in an attempt to minimize the impact of the disease worldwide. Although new knowledge has been quickly disseminated, including viral mechanisms, pathophysiology, and clinical findings, there is a lack of information on the effective pharmacolog...
A refined interpretation of intuitionistic logic by means of atomic polymorphism
Espírito Santo, José; Ferreira, GildaWe study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell–Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at t...
The Russell-Prawitz embedding and the atomization of universal instantiation
Espírito Santo, José; Ferreira, GildaGiven the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of ...
A refined interpretation of intuitionistic logic by means of atomic polymorphism
Espírito Santo, José; Ferreira, GildaWe study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell- Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at ...
The computational content of atomic polymorphism
Ferreira, Gilda; Vasconcelos, Vasco TWe show that the number-theoretic functions de nable in the atomic polymorphic system (Fat) are exactly the extended polynomials. Two proofs of the above result are presented: one reducing the functions' de n- ability problem in Fat to de nability in the simply typed lambda-calculus and other directly adapting Helmut Schwichtenberg's strategy for de nability in the simply typed lambda-calculus to the atomic pol...
Atomic polymorphism and the existence property
Ferreira, GildaWe present a purely proof-theoretic proof of the existence property for the full intuitionistic first-order predicate calculus, via natural deduction, in which commuting conversions are not needed. Such proof illustrates the potential of an atomic polymorphic system with only three generators of formulas – conditional and first and second-order universal quantifiers – as a tool for proof-theoretical studies.