Browsing by Author "Ferreira, Fernando"
Now showing 1 - 10 of 10
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.
- 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.
- 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.
- Matemática finitaPublication . André, Carlos; Ferreira, Fernando
- Matemática finita : combinatória enumerativaPublication . Ferreira, Fernando; Esteves, Lucinda; Cartaxo, Paulo; Cabral, MargaridaApresentação / Exploração de conceitos matemáticos; a partir de animações gráficas e de encenações são apresentados em seis sequências, respetivamente, os conceitos de: Correspondências Biunívocas, Princípio de Indução Matemática, Coeficientes Binomiais, Expansão Fatorial e Conceito de Infinito.
- Techniques in weak analysis for conservation resultsPublication . Fernandes, António; Ferreira, Fernando; Ferreira, GildaWe review and describe the main techniques for setting up systems of weak analysis, i.e. formal systems of second-order arithmetic related to subexponential classes of computational complexity. These involve techniques of proof theory (e.g., Herbrand’s theorem and the cut-elimination theorem) and model theoretic techniques like forcing. The techniques are illustrated for the particular case of polytime computability. We also include a brief section where we list the known results in weak analysis.
- The faithfulness of atomic polymorphismPublication . Ferreira, Fernando; Ferreira, GildaIt 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.
- The faithfulness of Fat: a proof-theoretic proofPublication . Ferreira, Fernando; Ferreira, GildaIt is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system Fat, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the intuitionistic propositional logic in which commuting conversions are not needed.