Steve Awodey (CMU) explains the relevance of the foundational program of homotopy type theory and the univalence axiom to the philosophy of mathematics in a new preprint, “Structuralism, Invariance, and Univalence.”
Recent advances in foundations of mathematics have led to some developments that are signicant for the philosophy of mathematics, particularly structuralism. Specically, the discovery of an interpretation of Martin-Löf’s constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics, with both intrinsic geometric content and a computational implementation. Leading homotopy theorist Vladimir Voevodsky has proposed an ambitious new program of foundations on this basis, including a new axiom with both geometric and logical signicance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to the framework of homotopical type theory.
Going through old emails, I found the following announcement by Larry Paulson, posted to the FOM list by Jeremy Avigad. Good stuff, including the link to Stanis?aw ?wierczkowski’s monograph in Dissertationes Mathematicae where he carries out the proof of the incompleteness theorems in HF, the theory of hereditarily finite sets. This should be of independent interest even if you don’t care about proof formalization — I hear of it, I think, but haven’t read it. You can buy it here.
I’ve completed a formalisation of Gödel’s two incompleteness theorems, including what may be the first-ever formalisation of the second incompleteness theorem. The proof was done in Isabelle/HOL and uses Christian Urban’s Nominal2 package for dealing with bound variables. The formalisation follows an unpublished paper by S. ?wierczkowski, who presents proofs of both incompleteness theorems using the hereditarily finite sets rather than Peano Arithmetic:
Proving the second incompleteness theorem requires some quite intricate operations on alphabets, as well as lengthy derivations in an internal calculus. Apart from those derivations, the proof script is structured and quite legible. The full development is concise, at under 17,000 lines, plus a further 3000 lines to develop HF set theory. (A recent Coq proof of the first incompleteness theorem alone is over 52,000 lines.)
The development is instructive. While first-order logic is formalised here using “nominal” binding primitives, the coding uses de Bruijn indexes. A precise correspondence is proved between the two representations of formulas. A series of correspondence proofs provides confidence in the correctness of the complicated syntactic definitions. The second incompleteness theorem follows from the Hilbert-Bernays derivability conditions. Proving the crucial theorem |- A => Prov[“A“] requires transforming a coded formula. During this process, the coded variables (which are constant terms) need to be replaced by terms consisting of a special function applied to the same variable (not coded). But this calculus has no functions, and this step needs to be expressed by introducing new variables that satisfy a certain relation with the original variables. The proof is by induction on the formula A, but relies on properties proved by a mutual induction within the encoded first-order calculus itself.
Ergo is a general, open access philosophy journal accepting submissions on all philosophical topics and from all philosophical traditions. This includes, among other things: history of philosophy, work in both the analytic and continental traditions, as well as formal and empirically informed philosophy.
Ergo uses a triple-anonymous peer review process and aims to return decisions within two months on average.
Ergo is published by MPublishing at the University of Michigan and sponsord by the Department of Philosophy at the University of Toronto. Papers are published as they are accepted; there is no regular publication schedule.
To submit a paper, please register and login to Ergo’s editorial management system at:
Submitted manuscripts should be prepared for anonymous review, containing no identifying information. Submissions need not conform to the journal style unless and until accepted for publication.
Submission and publication is free, but the journal essentially depends on the support of reliable reviewers returning informative reports in a timely manner. We hope that you will consider acting as referee for Ergo if asked by one of its editors. We also hope that you will consider submitting your work to Ergo.
Please share this call for papers with your colleagues!
Franz Huber (University of Toronto)
Jonathan Weisberg (University of Toronto)
Rachael Briggs (Australian National University & Griffith University)
Eleonora Cresto (University of Buenos Aires)
Vincenzo Crupi (University of Turin)
Imogen Dickie (University of Toronto)
Catarina Dutilh-Novaes (University of Groningen)
Kenny Easwaran (University of Southern California)
Matt Evans (University of Michigan)
Laura Franklin-Hall (New York University)
Ole Hjortland (LMU Munich)
Michelle Kosch (Cornell University)
Antonia LoLordo (University of Virginia)
Christy Mag Uidhir (University of Houston)
Julia Markovits (Massachusetts Institute of Technology)
Lionel McPherson (Tufts University)
Jennifer Nagel (University of Toronto)
Jill North (Cornell University)
Brian O’Connor (University College Dublin)
Laurie A. Paul (University of North Carolina at Chapel Hill)
Richard Pettigrew (Bristol University)
Martin Pickavé (University of Toronto)
Adam Sennet (University of California at Davis)
Nishi Shah (Amherst College)
Quayshawn Spencer (University of San Francisco)
Ásta Sveinsdóttir (San Francisco State University)
Robbie Williams (University of Leeds)
Wayne Wu (Carnegie Mellon University)
Jiji Zhang (Lingnan University)