Untitled

Funder

Organizational Unit

Publications

Publication . Ferreira, Fernando; Ferreira, Gilda

It is known that the full intuitionistic propositional calculus can be embedded into the atomic polymorphic system Fat, a calculus with only two connectives: the conditional and the second-order universal quantifier. The embedding uses a translation of formulas due to Prawitz and relies on the so-called property of instantiation overflow. In this paper, we show that the previous embedding is faithful i.e., if a translated formula is derivable in Fat, then the original formula is already derivable in the propositional calculus.

2014Journal article

Open access

Atomic polymorphism

Publication . Ferreira, Fernando; Ferreira, Gilda

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

2013Journal article

Open access

Interpretability in Robinson's Q

Publication . Ferreira, Fernando; Ferreira, Gilda

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

2013Journal article

Open access

Bounded theories for polyspace computability

Publication . Bianconi, Ricardo; Ferreira, Gilda; Silva, Emmanuel

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

2013Journal article

Open access