86 found
Sort by:
Disambiguations:
Jeremy Avigad [85]Jeremy D. Avigad [1]
  1. Jeremy Avigad, A Decision Procedure for Linear “Big o” Equations.
    Let F be the set of functions from an infinite set, S, to an ordered ring, R.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Jeremy Avigad & Harvey Friedman, Combining Decision Procedures for the Reals.
    We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which “local'’ decision or heuristic procedures for fragments of the theory of the reals can be amalgamated into global ones. Let $Tadd[QQ]$ be the first-order theory of the real numbers in the language with symbols $0, 1, +, -.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Jeremy Avigad, Steven Kieffer & Harvey Friedman, A Language for Mathematical Knowledge Management.
    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 (...)
    No categories
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  4. Jeremy Avigad, By Calixto Badesa.
    From ancient times to the beginning of the nineteenth century, mathematics was commonly viewed as the general science of quantity, with two main branches: geometry, which deals with continuous quantities, and arithmetic, which deals with quantities that are discrete. Mathematical logic does not fit neatly into this taxonomy. In 1847, George Boole [1] offered an alternative characterization of the subject in order to make room for this new discipline: mathematics should be understood to include the use of any symbolic calculus (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  5. Jeremy Avigad, By Dennis E. Hesseling.
    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, ´.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  6. Jeremy Avigad, Computability and Convergence.
    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 ) < ε.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  7. Jeremy Avigad, Eliminating Definitions and Skolem Functions in First-Order Logic.
    When working with a first-order theory, it is often convenient to use definitions. That is, if ϕ(x) is a first-order formula with the free variables shown, one can introduce a new relation symbol R to abbreviate ϕ, with defining axiom ∀x (R(x) ↔ ϕ(x)). Of course, this definition can later be eliminated from a proof, simply by replacing every instance of R by ϕ. But suppose the proof involves nested definitions, with a sequence of relation symbols R0, . . . (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  8. Jeremy Avigad, Eliminating Definitions and Skolem Functions.
    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.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  9. Jeremy Avigad, Proof Mining.
    Hilbert’s program: • Formalize abstract, infinitary, nonconstructive mathematics. • Prove consistency using only finitary methods.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  10. Jeremy Avigad, Kevin Donnelly, David Gray & Adam Kramer, Number Theory.
    1.1 Some examples of rule induction on permutations . . . . . . . 6 1.2 Ways of making new permutations . . . . . . . . . . . . . . . 7 1.3 Further results . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Removing elements . . . . . . . . . . (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  11. Marcus Giaquinto & Jeremy Avigad, By Marcus Giaquinto.
    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 (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  12. Andrea Asperti & Jeremy Avigad, Zen and the Art of Formalization.
    N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970’s, his work on the Automath system introduced the architecture that is common to most of today’s proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  13. Jeremy Avigad, Algebraic Proofs of Cut Elimination.
    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)  
     
    My bibliography  
     
    Export citation  
  14. Jeremy Avigad, A Realizability Interpretation for Classical Arithmetic.
    Summary. A constructive realizablity interpretation for classical arithmetic is presented, enabling one to extract witnessing terms from proofs of 1 sentences. The interpretation is shown to coincide with modified realizability, under a novel translation of classical logic to intuitionistic logic, followed by the Friedman-Dragalin translation. On the other hand, a natural set of reductions for classical arithmetic is shown to be compatible with the normalization of the realizing term, implying that certain strategies for eliminating cuts and extracting a witness from (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Jeremy Avigad, A Variant of the Double-Negation Translation.
    An efficient variant of the double-negation translation explains the relationship between Shoenfield’s and G¨odel’s versions of the Dialectica interpretation.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  16. Jeremy Avigad, Computers in Mathematical Inquiry.
    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)  
     
    My bibliography  
     
    Export citation  
  17. Jeremy Avigad, “Clarifying the Nature of the Infinite”: The Development of Metamathematics and Proof Theory.
    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)  
     
    My bibliography  
     
    Export citation  
  18. Jeremy Avigad, Dedekind's 1871 Version of the Theory of Ideals.
    By the middle of the nineteenth century, it had become clear to mathematicians that the study of finite field extensions of the rational numbers is indispensable to number theory, even if one’s ultimate goal is to understand properties of diophantine expressions and equations in the ordinary integers. It can happen, however, that the “integers” in such extensions fail to satisfy unique factorization, a property that is central to reasoning about the ordinary integers. In 1844, Ernst Kummer observed that unique factorization (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  19. Jeremy Avigad, Eliminating Definitions and Skolem Functions in First-Order Logic.
    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 (4 more)  
     
    My bibliography  
     
    Export citation  
  20. Jeremy Avigad, Formalizing O Notation in Isabelle/Hol.
    We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. Jeremy Avigad, Odel and the Metamathematical Tradition.
    The metamathematical tradition that developed from Hilbert’s program is based on syntactic characterizations of mathematics and the use of explicit, finitary methods in the metatheory. Although G¨.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  22. Jeremy Avigad, Local Stability of Ergodic Averages.
    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, (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  23. Jeremy Avigad, Methodology and Metaphysics in the Development of Dedekind's Theory of Ideals.
    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.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  24. Jeremy Avigad, Notes on a Formalization of the Prime Number Theorem.
    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)  
     
    My bibliography  
     
    Export citation  
  25. Jeremy Avigad, Ordinal Analysis Without Proofs.
    An approach to ordinal analysis is presented which is finitary, but highlights the semantic content of the theories under consideration, rather than the syntactic structure of their proofs. In this paper the methods are applied to the analysis of theories extending Peano arithmetic with transfinite induction and transfinite arithmetic hierarchies.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Jeremy Avigad, Plausibly Hard Combinatorial Tautologies.
    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.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  27. Jeremy Avigad, Philosophy of Mathematics.
    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)  
     
    My bibliography  
     
    Export citation  
  28. Jeremy Avigad, Proof Theory.
    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 (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  29. Jeremy Avigad, Philosophy of Mathematics: 5 Questions.
    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)  
     
    My bibliography  
     
    Export citation  
  30. Jeremy Avigad, Understanding Proofs.
    “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).
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  31. Jeremy Avigad, Weak Theories of Nonstandard Arithmetic and Analysis.
    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.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  32. Jesse Hughes, Steve Awodey, Dana Scott, Jeremy Avigad & Lawrence Moss, A Study of Categorres of Algebras and Coalgebras.
    This thesis is intended t0 help develop the theory 0f coalgebras by, Hrst, taking classic theorems in the theory 0f universal algebras amd dualizing them and, second, developing an interna] 10gic for categories 0f coalgebras. We begin with an introduction t0 the categorical approach t0 algebras and the dual 110tion 0f coalgebras. Following this, we discuss (c0)a,lg€bra.s for 2. (c0)monad and develop 2. theory 0f regular subcoalgebras which will be used in the interna] logic. We also prove that categories 0f (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  33. Jeremy Avigad (forthcoming). On the Relationships Between ATR 0 And ID_<Ω. Journal of Symbolic Logic.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  34. Jeremy Avigad (2013). Uniform Distribution and Algorithmic Randomness. 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 (4 more)  
     
    My bibliography  
     
    Export citation  
  35. Jeremy Avigad (2012). Uncomputably Noisy Ergodic Limits. Notre Dame Journal of Formal Logic 53 (3):347-350.
    V’yugin has shown that there are a computable shift-invariant measure on $2^{\mathbb{N}}$ and a simple function $f$ such that there is no computable bound on the rate of convergence of the ergodic averages $A_{n}f$ . Here it is shown that in fact one can construct an example with the property that there is no computable bound on the complexity of the limit; that is, there is no computable bound on how complex a simple function needs to be to approximate the (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  36. Jeremy Avigad, Edward T. Dean & Jason Rute (2012). Algorithmic Randomness, Reverse Mathematics, and the Dominated Convergence Theorem. Annals of Pure and Applied Logic 163 (12):1854-1864.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  37. Jeremy Avigad, Ulrich W. Kohlenbach, Henry Towsner, Samson Abramsky, Andreas Blass, Larry Moss, Alf Onshuus Nino, Patrick Speissegger, Juris Steprans & Monica VanDieren (2012). New Orleans Marriott and Sheraton New Orleans Hotels New Orleans, LA January 8–9, 2011. Bulletin of Symbolic Logic 18 (1).
    Direct download  
     
    My bibliography  
     
    Export citation  
  38. Jeremy Avigad (2010). Proof Theory. Gödel and the Metamathematical Tradition. In Kurt Gödel, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Kurt Gödel: Essays for His Centennial. Association for Symbolic Logic.
  39. Jeremy Avigad (2010). Understanding, Formal Verification, and the Philosophy of Mathematics. Journal of the Indian Council of Philosophical Research 27:161-197.
  40. Jeremy Avigad (2009). Marcus Giaquinto. Visual Thinking in Mathematics: An Epistemological Study. Philosophia Mathematica 17 (1):95-108.
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  41. Jeremy Avigad, The Computational Content of Classical Arithmetic to Appear in a Festschrift for Grigori Mints.
    Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of the Godel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  42. Jeremy Avigad (2009). The Metamathematics of Ergodic Theory. Annals of Pure and Applied Logic 157 (2):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 (...)
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  43. Jeremy Avigad, Edward Dean & John Mumma (2009). A Formal System for Euclid's Elements. 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)  
     
    My bibliography  
     
    Export citation  
  44. Jeremy Avigad & Henry Towsner, Metastability in the Furstenberg-Zimmer Tower.
    According to the Furstenberg-Zimmer structure theorem, every measure-preserving system has a maximal distal factor, and is weak mixing relative to that factor. Furstenberg and Katznelson used this structural analysis of measure-preserving systems to provide a perspicuous proof of Szemer\'edi's theorem. Beleznay and Foreman showed that, in general, the transfinite construction of the maximal distal factor of a separable measure-preserving system can extend arbitrarily far into the countable ordinals. Here we show that the Furstenberg-Katznelson proof does not require the full strength (...)
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  45. Jeremy Avigad (2008). Philosophical Relevance of Computers in Mathematics. In Paolo Mancosu (ed.), The Philosophy of Mathematical Practice. Oup Oxford.
    No categories
     
    My bibliography  
     
    Export citation  
  46. Jeremy Avigad & Henry Towsner, Functional Interpretation and Inductive Definitions.
    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 (7 more)  
     
    My bibliography  
     
    Export citation  
  47. Jeremy Avigad & Richard Zach, The Epsilon Calculus. Stanford Encyclopedia of Philosophy.
    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..
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  48. Steven Kieffer, Jeremy Avigad & Harvey Friedman, A Language for Mathematical Knowledge Management.
    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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  49. Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff, A Formally Verified Proof of the Prime Number Theorem.
    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.
    No categories
    Translate to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  50. Jeremy Avigad, Sy Friedman, Akihiro Kanamori, Elisabeth Bouscaren, Philip Kremer, Claude Laflamme, Antonio Montalbán, Justin Moore & Helmut Schwichtenberg (2007). Montréal, Québec, Canada May 17–21, 2006. Bulletin of Symbolic Logic 13 (1).
    Translate to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 86