Browsing by Author "Ferreira, Gilda"
Now showing 1 - 10 of 19
Results Per Page
Sort Options
- Analysis in weak systemsPublication . Fernandes, António M.; Ferreira, Fernando; Ferreira, GildaThe authors survey and comment their work on weak analysis. They describe the basic set-up of analysis in a feasible second-order theory and consider the impact of adding to it various forms of weak Konig's lemma. A brief discussion of the Baire categoricity theorem follows. It is then considered a strengthening of feasibility obtained (fundamentally) by the addition of a counting axiom and showed how it is possible to develop Riemann integration in the stronger system. The paper finishes with three questions in weak analysis.
- Atomic polymorphismPublication . Ferreira, Fernando; Ferreira, GildaIt has been known for six years that the restriction of Girard’s polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait’s method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to η-conversions.
- Atomic polymorphism and the existence propertyPublication . 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.
- Bounded theories for polyspace computabilityPublication . Bianconi, Ricardo; Ferreira, Gilda; Silva, EmmanuelWe present theories of bounded arithmetic and weak analysis whose provably total functions (with appropriate graphs) are the polyspace computable functions. More precisely, inspired in Ferreira’s systems PTCA, Sigma^b_1-NIA and BTFA in the polytime framework, we propose analogue theories concerning polyspace computability. Since the techniques we employ in the characterization of PSPACE via formal systems (e.g. Herbrand’s theorem, cut-elimination theorem and the expansion of models) are similar to the ones involved in the polytime setting, we focus on what is specific of polyspace and explains the lift from PTIME to PSPACE.
- Elementary proof of strong normalization for Atomic FPublication . Ferreira, Fernando; Ferreira, GildaWe give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus Fat (a predicative restriction of Girard’s system F).
- A herbrandized functional interpretation of classical first-order logicPublication . Ferreira, Fernando; Ferreira, GildaWe introduce a new typed combinatory calculus with a type constructor that, to each type σ, associates the star type σ^∗ of the nonempty finite subsets of elements of type σ. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements.
- Herbrandized modified realizabilityPublication . 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 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.
- Instantiation overflowPublication . Dinis, Bruno; Ferreira, GildaThe well-known embedding of full intuitionistic propositional calculus into the atomic polymorphic system Fat is possible due to the intriguing phenomenon of instantiation overflow. Instantiation overflow ensures that (in Fat) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in Fat were identi ed with such property: the types that result from the Prawitz translation of the propositional connectives (\bot,\wedge, \vee) into Fat (or Girard's system F). Are there other types in Fat with instantiation overflow? In this paper we show that the answer is yes and we isolate a class of formulas with such property.
- Interpretability in Robinson's QPublication . Ferreira, Fernando; Ferreira, GildaEdward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is an impassable barrier in the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson’s theory of arithmetic Q. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted in Q but also what cannot be so interpreted. We explain some of these results and rely on them to discuss Nelson’s position.
- Lisbon young mathematicians conference 2023: book of abstractsPublication . 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