Switch to: Citations

Add references

You must login to add references.
  1. Subsystems of Second Order Arithmetic.Stephen G. Simpson - 1999 - Studia Logica 77 (1):129-129.
    Download  
     
    Export citation  
     
    Bookmark   236 citations  
  • Factorization of polynomials and °1 induction.S. G. Simpson - 1986 - Annals of Pure and Applied Logic 31:289.
    Download  
     
    Export citation  
     
    Bookmark   36 citations  
  • (2 other versions)Introduction to Metamathematics.H. Rasiowa - 1954 - Journal of Symbolic Logic 19 (3):215-216.
    Download  
     
    Export citation  
     
    Bookmark   220 citations  
  • (2 other versions)Introduction to Metamathematics.Ann Singleterry Ferebee - 1968 - Journal of Symbolic Logic 33 (2):290-291.
    Download  
     
    Export citation  
     
    Bookmark   170 citations  
  • Why a Little Bit Goes a Long Way: Logical Foundations of Scientifically Applicable Mathematics.Solomon Feferman - 1992 - PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1992:442 - 455.
    Does science justify any part of mathematics and, if so, what part? These questions are related to the so-called indispensability arguments propounded, among others, by Quine and Putnam; moreover, both were led to accept significant portions of set theory on that basis. However, set theory rests on a strong form of Platonic realism which has been variously criticized as a foundation of mathematics and is at odds with scientific realism. Recent logical results show that it is possible to directly formalize (...)
    Download  
     
    Export citation  
     
    Bookmark   29 citations  
  • Introduction to metamathematics.Stephen Cole Kleene - 1952 - Groningen: P. Noordhoff N.V..
    Stephen Cole Kleene was one of the greatest logicians of the twentieth century and this book is the influential textbook he wrote to teach the subject to the next generation. It was first published in 1952, some twenty years after the publication of Godel's paper on the incompleteness of arithmetic, which marked, if not the beginning of modern logic. The 1930s was a time of creativity and ferment in the subject, when the notion of computable moved from the realm of (...)
    Download  
     
    Export citation  
     
    Bookmark   551 citations  
  • Subrecursion: functions and hierarchies.H. E. Rose - 1984 - New York: Oxford University Press.
    Download  
     
    Export citation  
     
    Bookmark   35 citations  
  • Constructive mathematics.Douglas Bridges - 2008 - Stanford Encyclopedia of Philosophy.
    Download  
     
    Export citation  
     
    Bookmark   31 citations  
  • Weak theories of nonstandard arithmetic and analysis.Jeremy Avigad - manuscript
    A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • (1 other version)Constructive mathematics in theory and programming practice.Douglas Bridges & Steeve Reeves - 1999 - Philosophia Mathematica 7 (1):65-104.
    The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Constructivism in Mathematics, An Introduction.A. Troelstra & D. Van Dalen - 1991 - Tijdschrift Voor Filosofie 53 (3):569-570.
    Download  
     
    Export citation  
     
    Bookmark   65 citations  
  • Foundations of Constructive Mathematics.Michael J. Beeson - 1932 - Springer Verlag.
    Download  
     
    Export citation  
     
    Bookmark   48 citations  
  • A mathematical incompleteness in Peano arithmetic.Jeff Paris & Leo Harrington - 1977 - In Jon Barwise (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 90--1133.
    Download  
     
    Export citation  
     
    Bookmark   63 citations  
  • Subsystems of Second Order Arithmetic.Stephen George Simpson - 1998 - Springer Verlag.
    Stephen George Simpson. with definition 1.2.3 and the discussion following it. For example, taking 90(n) to be the formula n §E Y, we have an instance of comprehension, VYEIXVn(n€X<—>n¢Y), asserting that for any given set Y there exists a ...
    Download  
     
    Export citation  
     
    Bookmark   131 citations  
  • Kreisel's 'Unwinding Program'.Solomon Feferman - 1996 - In Piergiorgio Odifreddi (ed.), Kreiseliana: About and Around Georg Kreisel. A K Peters. pp. 247--273.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Finitism.W. W. Tait - 1981 - Journal of Philosophy 78 (9):524-546.
    Download  
     
    Export citation  
     
    Bookmark   118 citations  
  • (1 other version)Herbrand-analysen zweier beweise Des satzes Von Roth: Polynomiale anzahlschranken.H. Luckhardt - 1989 - Journal of Symbolic Logic 54 (1):234-263.
    A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs of Σ 2 -finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • (1 other version)Formalizing forcing arguments in subsystems of second-order arithmetic.Jeremy Avigad - 1996 - Annals of Pure and Applied Logic 82 (2):165-191.
    We show that certain model-theoretic forcing arguments involving subsystems of second-order arithmetic can be formalized in the base theory, thereby converting them to effective proof-theoretic arguments. We use this method to sharpen the conservation theorems of Harrington and Brown-Simpson, giving an effective proof that WKL+0 is conservative over RCA0 with no significant increase in the lengths of proofs.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman. edited by Wilfred Sieg, Richard Sommer, and Carolyn Talcott, Lecture Notes in Logic, vol. 15. A. K. Peters, Ltd., Natick, MA, 2002, viii + 440 pp.David Charles McCarty - 2005 - Bulletin of Symbolic Logic 11 (2):239-241.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Kreiseliana: About and around Georg Kreisel.Piergiorgio Odifreddi - 1999 - Studia Logica 63 (3):422-426.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Foundations of Constructive Mathematics.Michael J. Beeson - 1987 - Studia Logica 46 (4):398-399.
    Download  
     
    Export citation  
     
    Bookmark   94 citations  
  • (1 other version)Constructive Mathematics in Theory and Programming Practice.Douglas Bridges & Steeve Reeves - 1998 - Philosophia Mathematica 6 (3):65-104.
    The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics. it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • (1 other version)Grundlagen der Mathematik.S. C. Kleene - 1940 - Journal of Symbolic Logic 5 (1):16-20.
    Download  
     
    Export citation  
     
    Bookmark   82 citations  
  • On the interpretation of non-finitist proofs—Part I.G. Kreisel - 1951 - Journal of Symbolic Logic 16 (4):241-267.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • A feasible theory for analysis.Fernando Ferreira - 1994 - Journal of Symbolic Logic 59 (3):1001-1011.
    We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with Σ b 1 -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof.Rolando Chuaqui & Patrick Suppes - 1995 - Journal of Symbolic Logic 60 (1):122-159.
    In treatises or advanced textbooks on theoretical physics, it is apparent that the way mathematics is used is very different from what is to be found in books of mathematics. There is, for example, no close connection between books on analysis, on the one hand, and any classical textbook in quantum mechanics, for example, Schiff, [11], or quite recent books, for example Ryder, [10], on quantum field theory. The differences run a good deal deeper than the fact that the books (...)
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • On the induction schema for decidable predicates.Lev D. Beklemishev - 2003 - Journal of Symbolic Logic 68 (1):17-34.
    We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, $I\Delta_1$ . We show that $I\Delta_1$ is independent from the set of all true arithmetical $\Pi_2-sentences$ . Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of $\Delta_1-induction$ . An open problem formulated by J. (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • First-Order Proof Theory of Arithmetic.Samuel R. Buss - 2000 - Bulletin of Symbolic Logic 6 (4):465-466.
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • On the Interpretation of Non-Finitist Proofs.G. Kreisel - 1953 - Journal of Symbolic Logic 18 (1):78-80.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • (2 other versions)Grundlagen der Mathematik I.David Hilbert & Paul Bernays - 1968 - Springer.
    Die Leitgedanken meiner Untersuchungen über die Grundlagen der Mathematik, die ich - anknüpfend an frühere Ansätze - seit 1917 in Besprechungen mit P. BERNAYS wieder aufgenommen habe, sind von mir an verschiedenen Stellen eingehend dargelegt worden. Diesen Untersuchungen, an denen auch W. ACKERMANN beteiligt ist, haben sich seither noch verschiedene Mathematiker angeschlossen. Der hier in seinem ersten Teil vorliegende, von BERNAYS abgefaßte und noch fortzusetzende Lehrgang bezweckt eine Darstellung der Theorie nach ihren heutigen Ergebnissen. Dieser Ergebnisstand weist zugleich die Richtung (...)
    Download  
     
    Export citation  
     
    Bookmark   109 citations  
  • The growth of mathematical knowledge.Emily Grosholz & Herbert Breger (eds.) - 2000 - Boston: Kluwer Academic Publishers.
    This book draws its inspiration from Hilbert, Wittgenstein, Cavaillès and Lakatos and is designed to reconfigure contemporary philosophy of mathematics by making the growth of knowledge rather than its foundations central to the study of mathematical rationality, and by analyzing the notion of growth in historical as well as logical terms. Not a mere compendium of opinions, it is organised in dialogical forms, with each philosophical thesis answered by one or more historical case studies designed to support, complicate or question (...)
    Download  
     
    Export citation  
     
    Bookmark   16 citations  
  • Provability of the pigeonhole principle and the existence of infinitely many primes.J. B. Paris, A. J. Wilkie & A. R. Woods - 1988 - Journal of Symbolic Logic 53 (4):1235-1244.
    Download  
     
    Export citation  
     
    Bookmark   28 citations  
  • Existence and feasibility in arithmetic.Rohit Parikh - 1971 - Journal of Symbolic Logic 36 (3):494-508.
    Download  
     
    Export citation  
     
    Bookmark   90 citations  
  • “Clarifying the nature of the infinite”: The development of metamathematics and proof theory.Jeremy Avigad - manuscript
    We discuss the development of metamathematics in the Hilbert school, and Hilbert’s proof-theoretic program in particular. We place this program in a broader historical and philosophical context, especially with respect to nineteenth century developments in mathematics and logic. Finally, we show how these considerations help frame our understanding of metamathematics and proof theory today.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • (1 other version)Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic.Jeremy Avigad - 2001 - Bulletin of Symbolic Logic 7 (3):390-391.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (1 other version)Fragments of arithmetic.Wilfried Sieg - 1985 - Annals of Pure and Applied Logic 28 (1):33-71.
    We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...)
    Download  
     
    Export citation  
     
    Bookmark   53 citations  
  • (1 other version)Mathematically Strong Subsystems of Analysis with Low Rate of Growth of Provably Recursive Functionals.Ulrich Kohlenbach - 2001 - Bulletin of Symbolic Logic 7 (2):280-281.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Realizability.A. S. Troelstra - 2000 - Bulletin of Symbolic Logic 6 (4):470-471.
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • Die Widerspruchsfreiheit der Allgemeinen Mengenlehre.Wilhelm Ackerman - 1937 - Journal of Symbolic Logic 2 (4):167-167.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Reductions of Theories for Analysis.Wilfried Sieg, Georg Dorn & P. Weingartner - 1990 - Journal of Symbolic Logic 55 (1):354-354.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Mathematical explanation: Why it matters.Paolo Mancosu - 2008 - In The Philosophy of Mathematical Practice. Oxford, England: Oxford University Press. pp. 134--149.
    Download  
     
    Export citation  
     
    Bookmark   52 citations  
  • The partial unification of domains, hybrids, and the growth of mathematical knowledge.Emily R. Grosholz - 2000 - In Emily Grosholz & Herbert Breger (eds.), The growth of mathematical knowledge. Boston: Kluwer Academic Publishers. pp. 81--91.
    Download  
     
    Export citation  
     
    Bookmark   16 citations  
  • A proof-theoretic analysis of collection.Lev D. Beklemishev - 1998 - Archive for Mathematical Logic 37 (5-6):275-296.
    By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$ , is $\Pi_{n+2}$ conservative over $I\Sigma_n$ . We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left open by Sieg (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  • (1 other version)Gödel's Functional Interpretation.Jeremy Avigad & Solomon Feferman - 2000 - Bulletin of Symbolic Logic 6 (4):469-470.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • (1 other version)Godel's functional interpretation.Jeremy Avigad & Solomon Feferman - 1998 - In Samuel R. Buss (ed.), Handbook of proof theory. New York: Elsevier. pp. 337-405.
    Download  
     
    Export citation  
     
    Bookmark   31 citations  
  • Does mathematics need new axioms.Solomon Feferman, Harvey M. Friedman, Penelope Maddy & John R. Steel - 1999 - Bulletin of Symbolic Logic 6 (4):401-446.
    Part of the ambiguity lies in the various points of view from which this question might be considered. The crudest di erence lies between the point of view of the working mathematician and that of the logician concerned with the foundations of mathematics. Now some of my fellow mathematical logicians might protest this distinction, since they consider themselves to be just more of those \working mathematicians". Certainly, modern logic has established itself as a very respectable branch of mathematics, and there (...)
    Download  
     
    Export citation  
     
    Bookmark   79 citations  
  • (1 other version)Eliminating definitions and Skolem functions in first-order logic.Jeremy Avigad - manuscript
    From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
    A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • (2 other versions)Subrecursion. Functions and Hierarchies.H. Schwichtenberg - 1987 - Journal of Symbolic Logic 52 (2):563-565.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Reply to Charles Parsons.W. V. O. Quine - 1986 - In Lewis Edwin Hahn & Paul Arthur Schilpp (eds.), The Philosophy of W.V. Quine. Chicago: Open Court. pp. 396-404.
    Download  
     
    Export citation  
     
    Bookmark   60 citations