Switch to: References

Add citations

You must login to add citations.
  1. Admissible closures of polynomial time computable arithmetic.Dieter Probst & Thomas Strahm - 2011 - Archive for Mathematical Logic 50 (5):643-660.
    We propose two admissible closures $${\mathbb{A}({\sf PTCA})}$$ and $${\mathbb{A}({\sf PHCA})}$$ of Ferreira’s system PTCA of polynomial time computable arithmetic and of full bounded arithmetic (or polynomial hierarchy computable arithmetic) PHCA. The main results obtained are: (i) $${\mathbb{A}({\sf PTCA})}$$ is conservative over PTCA with respect to $${\forall\exists\Sigma^b_1}$$ sentences, and (ii) $${\mathbb{A}({\sf PHCA})}$$ is conservative over full bounded arithmetic PHCA for $${\forall\exists\Sigma^b_{\infty}}$$ sentences. This yields that (i) the $${\Sigma^b_1}$$ definable functions of $${\mathbb{A}({\sf PTCA})}$$ are the polytime functions, and (ii) the $${\Sigma^b_{\infty}}$$ definable (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
    In this paper we study (self)-applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on W = {0, 1} * are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Groundwork for weak analysis.António M. Fernandes & Fernando Ferreira - 2002 - Journal of Symbolic Logic 67 (2):557-578.
    This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Bounded functional interpretation and feasible analysis.Fernando Ferreira & Paulo Oliva - 2007 - Annals of Pure and Applied Logic 145 (2):115-129.
    In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • 1995 European Summer Meeting of the Association for Symbolic Logic.Johann A. Makowsky - 1997 - Bulletin of Symbolic Logic 3 (1):73-147.
    Download  
     
    Export citation  
     
    Bookmark  
  • Strict $${\Pi^1_1}$$ -reflection in bounded arithmetic.António M. Fernandes - 2010 - Archive for Mathematical Logic 49 (1):17-34.
    We prove two conservation results involving a generalization of the principle of strict ${\Pi^1_1}$ -reflection, in the context of bounded arithmetic. In this context a separation between the concepts of bounded set and binary sequence seems to emerge as fundamental.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Interpretability in Robinson's Q.Fernando Ferreira & Gilda Ferreira - 2013 - Bulletin of Symbolic Logic 19 (3):289-317.
    Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin 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. 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 inbut also what cannot be so (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations