113 found
Order:
Disambiguations
Jeremy Avigad [111]Jeremy D. Avigad [2]
  1. A Formal System for Euclid's Elements.Jeremy Avigad, Edward Dean & John Mumma - 2009 - Review of Symbolic Logic 2 (4):700--768.
    We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  2. Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
    A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
    Direct download (12 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  3. Mathematical Method and Proof.Jeremy Avigad - 2006 - Synthese 153 (1):105-159.
    On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, and that (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  4. Forcing in Proof Theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
    Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...)
    Direct download (14 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  5.  68
    Number Theory and Elementary Arithmetic.Jeremy Avigad - 2003 - Philosophia Mathematica 11 (3):257-284.
    is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.
    Direct download (17 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  6.  29
    Local Stability of Ergodic Averages.Jeremy Avigad - unknown
    We consider the extent to which one can compute bounds on the rate of convergence of a sequence of ergodic averages. It is not difficult to construct an example of a computable Lebesgue measure preserving transformation of [0, 1] and a characteristic function f = χA such that the ergodic averages Anf do not converge to a computable element of L2([0, 1]). In particular, there is no computable bound on the rate of convergence for that sequence. On the other hand, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  7.  48
    The Epsilon Calculus.Jeremy Avigad & Richard Zach - 2008 - In Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University.
    The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes such terms (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  25
    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.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  9.  72
    Transfer Principles in Nonstandard Intuitionistic Arithmetic.Jeremy Avigad & Jeffrey Helzner - 2002 - Archive for Mathematical Logic 41 (6):581-602.
    Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  10. Understanding, Formal Verification, and the Philosophy of Mathematics.Jeremy Avigad - 2010 - Journal of the Indian Council of Philosophical Research 27:161-197.
    The philosophy of mathematics has long been concerned with deter- mining the means that are appropriate for justifying claims of mathemat- ical knowledge, and the metaphysical considerations that render them so. But, as of late, many philosophers have called attention to the fact that a much broader range of normative judgments arise in ordinary math- ematical practice; for example, questions can be interesting, theorems important, proofs explanatory, concepts powerful, and so on. The as- sociated values are often loosely classied as (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  33
    Fundamental Notions of Analysis in Subsystems of Second-Order Arithmetic.Jeremy Avigad - 2006 - Annals of Pure and Applied Logic 139 (1):138-184.
    We develop fundamental aspects of the theory of metric, Hilbert, and Banach spaces in the context of subsystems of second-order arithmetic. In particular, we explore issues having to do with distances, closed subsets and subspaces, closures, bases, norms, and projections. We pay close attention to variations that arise when formalizing definitions and theorems, and study the relationships between them.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  12.  7
    Character and Object.Rebecca Morris & Jeremy Avigad - 2016 - Review of Symbolic Logic 9 (3):480-510.
    In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. Modern presentations of the proof are explicitly higher-order, in that they involve quantifying over and summing over Dirichlet characters, which are certain types of functions. The notion of a character is only implicit in Dirichlet’s original proof, and the subsequent history shows a very gradual transition to the modern mode of presentation. In this essay, we (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  31
    Update Procedures and the 1-Consistency of Arithmetic.Jeremy Avigad - 2002 - Mathematical Logic Quarterly 48 (1):3-13.
    The 1-consistency of arithmetic is shown to be equivalent to the existence of fixed points of a certain type of update procedure, which is implicit in the epsilon-substitution method.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  14.  26
    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.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  15.  31
    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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  16.  2
    Transfer Principles in Nonstandard Intuitionistic Arithmetic.Jeremy Avigad & Jeremy Helzner - 2002 - Archive for Mathematical Logic 41 (6):581-602.
  17.  39
    On the Relationship Between ATR 0 And.Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (3):768-779.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  18.  40
    Methodology and Metaphysics in the Development of Dedekind's Theory of Ideals.Jeremy Avigad - 2006 - In Jose Ferreiros Jeremy Gray (ed.), The architecture of modern mathematics.
    Philosophical concerns rarely force their way into the average mathematician’s workday. But, in extreme circumstances, fundamental questions can arise as to the legitimacy of a certain manner of proceeding, say, as to whether a particular object should be granted ontological status, or whether a certain conclusion is epistemologically warranted. There are then two distinct views as to the role that philosophy should play in such a situation. On the first view, the mathematician is called upon to turn to the counsel (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  19.  14
    On the Relationships Between ATR0 and $\Widehat{ID}_{.Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (3):768 - 779.
    We show that the theory ATR 0 is equivalent to a second-order generalization of the theory $\widehat{ID}_{ . As a result, ATR 0 is conservative over $\widehat{ID}_{ for arithmetic sentences, though proofs in ATR 0 can be much shorter than their $\widehat{ID}_{ counterparts.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  20.  42
    The Metamathematics of Ergodic Theory.Jeremy Avigad - 2009 - Annals of Pure and Applied Logic 157 (2-3):64-76.
    The metamathematical tradition, tracing back to Hilbert, employs syntactic modeling to study the methods of contemporary mathematics. A central goal has been, in particular, to explore the extent to which infinitary methods can be understood in computational or otherwise explicit terms. Ergodic theory provides rich opportunities for such analysis. Although the field has its origins in seventeenth century dynamics and nineteenth century statistical mechanics, it employs infinitary, nonconstructive, and structural methods that are characteristically modern. At the same time, computational concerns (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  21.  13
    Modularity in Mathematics.Jeremy Avigad - 2017 - Review of Symbolic Logic:1-33.
    In a wide range of fields, the word "modular" is used to describe complex systems that can be decomposed into smaller systems with limited interactions between them. This essay argues that mathematical knowledge can fruitfully be understood as having a modular structure, and explores the ways in which modularity in mathematics is epistemically advantageous.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  22.  50
    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.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  23.  38
    Algebraic Proofs of Cut Elimination.Jeremy Avigad - manuscript
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24.  41
    A Formally Verified Proof of the Prime Number Theorem.Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff - unknown
    The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  25.  27
    An Effective Proof That Open Sets Are Ramsey.Jeremy Avigad - 1998 - Archive for Mathematical Logic 37 (4):235-240.
    Solovay has shown that if $\cal{O}$ is an open subset of $P(\omega)$ with code $S$ and no infinite set avoids $\cal{O}$ , then there is an infinite set hyperarithmetic in $S$ that lands in $\cal{O}$ . We provide a direct proof of this theorem that is easily formalizable in $ATR_0$.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  26.  25
    Predicative Functionals and an Interpretation of ⌢ID<Ω.Jeremy Avigad - 1998 - Annals of Pure and Applied Logic 92 (1):1-34.
    In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  27.  10
    Uniform Distribution and Algorithmic Randomness.Jeremy Avigad - 2013 - Journal of Symbolic Logic 78 (1):334-344.
    A seminal theorem due to Weyl [14] states that if $(a_n)$ is any sequence of distinct integers, then, for almost every $x \in \mathbb{R}$, the sequence $(a_n x)$ is uniformly distributed modulo one. In particular, for almost every $x$ in the unit interval, the sequence $(a_n x)$ is uniformly distributed modulo one for every computable sequence $(a_n)$ of distinct integers. Call such an $x$ UD random. Here it is shown that every Schnorr random real is UD random, but there are (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  28. A Language for Mathematical Knowledge Management.Jeremy Avigad, Steven Kieffer & Harvey Friedman - manuscript
    We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  29.  60
    The Lean Theorem Prover.Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn & Jakob von Raumer - unknown
    Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30.  32
    A Model-Theoretic Approach to Ordinal Analysis.Jeremy Avigad & Richard Sommer - 1997 - Bulletin of Symbolic Logic 3 (1):17-52.
    We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  31.  74
    Philosophy of Mathematics: 5 Questions.Jeremy Avigad - 2007 - In V. F. Hendricks & Hannes Leitgeb (eds.), Philosophy of Mathematics: Five Questions. Automatic Press/VIP.
    In 1977, when I was nine years old, Doubleday released Asimov on Numbers, a collection of essays that had first appeared in Isaac Asimov’s Science Fiction and Fantasy column. My mother, recognizing my penchant for science fiction and mathematics, bought me a copy as soon as it hit the bookstores. The essays covered topics such as number systems, combinatorial curiosities, imaginary numbers, and π. I was especially taken, however, by an essay titled “Varieties of the infinite,” which included a photograph (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  32.  54
    Marcus Giaquinto. Visual Thinking in Mathematics: An Epistemological Study. [REVIEW]Jeremy Avigad - 2009 - Philosophia Mathematica 17 (1):95-108.
    Published in 1891, Edmund Husserl's first book, Philosophie der Arithmetik, aimed to ‘prepare the scientific foundations for a future construction of that discipline’. His goals should seem reasonable to contemporary philosophers of mathematics: "…through patient investigation of details, to seek foundations, and to test noteworthy theories through painstaking criticism, separating the correct from the erroneous, in order, thus informed, to set in their place new ones which are, if possible, more adequately secured. 1"But the ensuing strategy for grounding mathematical knowledge (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  34
    The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength.Jeremy Avigad & Richard Sommer - 1999 - Journal of Symbolic Logic 64 (1):327-349.
    We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first- and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to Γ0.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  34.  25
    Functional Interpretation and Inductive Definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.
    Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35. Eliminating Definitions and Skolem Functions.Jeremy Avigad - unknown
    two elements, one can eliminate definitions with a polynomial bound on the increase in proof length. In any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions with a polynomial bound on the increase in proof length.
    Translate
     
     
    Export citation  
     
    Bookmark  
  36. Philosophy of Mathematics.Jeremy Avigad - manuscript
    The philosophy of mathematics plays an important role in analytic philosophy, both as a subject of inquiry in its own right, and as an important landmark in the broader philosophical landscape. Mathematical knowledge has long been regarded as a paradigm of human knowledge with truths that are both necessary and certain, so giving an account of mathematical knowledge is an important part of epistemology. Mathematical objects like numbers and sets are archetypical examples of abstracta, since we treat such objects in (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  37.  21
    Plausibly Hard Combinatorial Tautologies.Jeremy Avigad - manuscript
    We present a simple propositional proof system which consists of a single axiom schema and a single rule, and use this system to construct a sequence of combinatorial tautologies that, when added to any Frege system, p-simulates extended-Frege systems.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  38. Philosophical Relevance of Computers in Mathematics.Jeremy Avigad - 2008 - In Paolo Mancosu (ed.), The Philosophy of Mathematical Practice. Oxford University Press.
  39.  75
    Computers in Mathematical Inquiry.Jeremy Avigad - manuscript
    In Section 2, I survey some of the ways that computers are used in mathematics. These raise questions that seem to have a generally epistemological character, although they do not fall squarely under a traditional philosophical purview. The goal of this article is to try to articulate some of these questions more clearly, and assess the philosophical methods that may be brought to bear. In Section 3, I note that most of the issues can be classified under two headings: some (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  40.  71
    “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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  41.  55
    Formalizing O Notation in Isabelle/Hol.Jeremy Avigad - manuscript
    We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  42.  17
    Smullyan Raymond M.. First-Order Logic. Corrected Republication of XL 237. Dover Publications, New York 1995, Xii + 158 Pp. [REVIEW]Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (1):351.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  43.  20
    Computability and Analysis: The Legacy of Alan Turing.Jeremy Avigad & Vasco Brattka - unknown
    We discuss the legacy of Alan Turing and his impact on computability and analysis.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44.  52
    Proof Theory.Jeremy Avigad - unknown
    At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45.  57
    Understanding Proofs.Jeremy Avigad - manuscript
    “Now, in calm weather, to swim in the open ocean is as easy to the practised swimmer as to ride in a spring-carriage ashore. But the awful lonesomeness is intolerable. The intense concentration of self in the middle of such a heartless immensity, my God! who can tell it? Mark, how when sailors in a dead calm bathe in the open sea—mark how closely they hug their ship and only coast along her sides.” (Herman Melville, Moby Dick, Chapter 94).
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  46.  38
    Computability and Convergence.Jeremy Avigad - unknown
    For most of its history, mathematics was fairly constructive: • Euclidean geometry was based on geometric construction. • Algebra sought explicit solutions to equations. Analysis, probability, etc. were focused on calculations. Nineteenth century developments in analysis challenged this view. A sequence (an) in a metric space is said Cauchy if for every ε > 0, there is an m such that for every n, n ≥ m, d (a n , a n ) < ε.
    Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  47.  42
    By Marcus Giaquinto.Marcus Giaquinto & Jeremy Avigad - unknown
    Published in 1891, Edmund Husserl’s first book, Philosophie der Arithmetik, aimed to “prepare the scientific foundations for a future construction of that discipline.” His goals should seem reasonable to contemporary philosophers of mathematics: . . . through patient investigation of details, to seek foundations, and to test noteworthy theories through painstaking criticism, separating the correct from the erroneous, in order, thus informed, to set in their place new ones which are, if possible, more adequately secured. [7, p. 5]2 But the (...)
    Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  48.  50
    Notes on a Formalization of the Prime Number Theorem.Jeremy Avigad - unknown
    On September 6, 2004, using the Isabelle proof assistant, I verified the following statement: (%x. pi x * ln (real x) / (real x)) ----> 1 The system thereby confirmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an infinite set. All told, our number theory session, including the proof of the prime number theorem and supporting libraries, constitutes 673 pages of proof scripts, or roughly 30,000 (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  49.  32
    By Dennis E. Hesseling.Jeremy Avigad - unknown
    The early twentieth century was a lively time for the foundations of mathematics. This ensuing debates were, in large part, a reaction to the settheoretic and nonconstructive methods that had begun making their way into mathematical practice around the turn of the twentieth century. The controversy was exacerbated by the discovery that overly na¨ıve formulations of the fundamental principles governing the use of sets could result in contradictions. Many of the leading mathematicians of the day, including Hilbert, Henri Poincar´e, ´.
    Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  50.  20
    Proof Mining.Jeremy Avigad - unknown
    Hilbert’s program: • Formalize abstract, infinitary, nonconstructive mathematics. • Prove consistency using only finitary methods.
    Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
1 — 50 / 113