Abstracts
Benedikt Ahrens (INRIA Nantes, France)
Univalent Foundations and the Equivalence Principle
The "equivalence principle" (EP) says that meaningful statements in mathematics should be invariant under the appropriate notion of equivalence - "sameness" - of the objects under consideration. In set theoretic foundations, the EP is not enforced; e.g., the statement "1 ϵ Nat" is not invariant under isomorphism of sets. In univalent foundations, on the other hand, the equivalence principle has been proved for many mathematical structures. In this introductory talk, I first give an overview of earlier attempts at designing foundations that satisfy some invariance property. Afterwards I present results, both by other and myself, on the validity of EP in univalent foundations.
fomus_slides_ahrens.pdf |
Thorsten Altenkirch (University of Nottingham, UK)
Naïve Type Theory
In this course we introduce Type Theory (sometimes called "dependent type theory") as an informal language for mathematical constructions in Computer Science and other disciplines. By Type Theory we mean the constructive foundation of Mathematics whose development was started by Per Martin-Loef in the 1970ies based on the Curry-Howard equivalence of propositions and types. Because of this proximity to Computer Science, Type Theory has been the foundation of interactive theorem provers and programming languages such as NuPRL, Coq, Agda and Idris. While the calculi on which these systems are based are an important research topic, in this course we want to emphasise the "naive" use of Type Theory using just pen and paper. Indeed this is similar to the naive use of set theory which is usually applied informally without explicitly relating each constructions to the axioms of set theory (as in Halmos' book on "Naive Set Theory").
In this course we focus on the intuitive foundations of Type Theory and on basic constructions such as: universes, (dependent) function types, (dependent) products, inductive types and equality and their use in informal reasoning. If time permits we will also cover basic constructions from Homotopy Type Theory, such as the univalence axiom (isomorphism is equality), and some Higher Inductive Types (a generalisation of quotient types). A good reference for our course is chapter 1 of the book on Homotopy Type Theory (available here).
In this course we focus on the intuitive foundations of Type Theory and on basic constructions such as: universes, (dependent) function types, (dependent) products, inductive types and equality and their use in informal reasoning. If time permits we will also cover basic constructions from Homotopy Type Theory, such as the univalence axiom (isomorphism is equality), and some Higher Inductive Types (a generalisation of quotient types). A good reference for our course is chapter 1 of the book on Homotopy Type Theory (available here).
Clemens Ballarin (aicas GmbH Karlsruhe, Germany)
Structuring Mathematics in Higher-Order Logic
The logical foundation is an important aspect of the design of a proof assistant. So is its support for structuring formal developments. The Isabelle proof assistant is based on an intuitionist fragment of higer-order logic, in which logical systems of discourse such as classical higher-order logic and set theory are represented. The former is known as meta logic, the latter are called object logics. Locales, the module system of Isabelle, are based on Isabelle's meta logic and are therefore capable of supporting all of Isabelle's object logics. The talk will cover both foundational aspects of Isabelle and its module system.
Clemens Ballarin (aicas GmbH Karlsruhe, Germany)
Proof Assistants (Isabelle) (Workshop)
This tutorial is a short introduction to the proof assistant Isabelle and its use. Part I covers interacting with Isabelle, step-by-step natural deduction proofs and some automation. Part II introduces Isar, Isabelle’s declarative proof language, support for inductive definitions and induction.
Each part comprises a lecture followed by a session where participants can use Isabelle themselves. Please bring a laptop with Isabelle installed. For instructions, see http://isabelle.in.tum.de/installation.html. (The tutorial will not cover document preparation, so installing TeX is not required.)
Each part comprises a lecture followed by a session where participants can use Isabelle themselves. Please bring a laptop with Isabelle installed. For instructions, see http://isabelle.in.tum.de/installation.html. (The tutorial will not cover document preparation, so installing TeX is not required.)
Marc Bezem (Universitetet i Bergen, Norway)
"Elements of Mathematics" in the Digital Age
"Elements of Mathematics" is the title of some grand endeavours in the foundations of mathematics. Euclid's "Elements" have undoubtedly be the most influential, followed at a certain distance by Bourbaki. Less well known, but also potentially influential, is the "Elements"-like project Automath by N.G. de Bruijn.
The essence of the latter (and more recent) projects is the ultimate formalization of mathematics, to the extent that mathematical prose (definitions, theorems, proofs) becomes machine-processable. Independent verification of proofs by a computer constitutes a transition from mathematical-proofs-as-social-constructs to full accountability. We discuss how this development can lead to a cultural change in research and education in mathematics.
The essence of the latter (and more recent) projects is the ultimate formalization of mathematics, to the extent that mathematical prose (definitions, theorems, proofs) becomes machine-processable. Independent verification of proofs by a computer constitutes a transition from mathematical-proofs-as-social-constructs to full accountability. We discuss how this development can lead to a cultural change in research and education in mathematics.
Alexander Carstensen Block (Universität Hamburg, Germany)
Modal Logic of Forcing (Workshop)
In set theory we have a rich assortment of methods to prove independence results. Many of these can be naturally seen as construction methods which construct from a given set theoretic model other set theoretic models in a way that we can control whether certain set theoretic statements are satisfied in the constructed models. Probably the most important such construction method is the method of Forcing, which was introduced by Paul Cohen in 1963. Given a (countable) model M of say ZFC we can consider the relational structure generated by closing off the singleton {M} under the construction method of forcing together with a
binary relation R relating a model N to N' iff N'can be obtained via forcing from N. We call this the generic multiverse generated by M and it is now natural to wonder what we can say about the general pattern of truth values of set theoretic sentences inside the models of a generic multiverse with respect to the relation R. A useful tool for this is modal logic, whose language an extension of propositional language by a unary operator which we here interpret as "In every model generated by forcing: ...".
Generic multiverses were introduced (in a slightly different form) by Hugh Woodin in 2009 and embedded into the set-theoretic multiverse program (cf. the talk "Multiverse Truth Behaviour Patterns" by Benedikt Löwe below), which serves as the main motivation for studying the former, by Joel D. Hamkins in 2012.
In this workshop I will give an introduction to modal logic and show how it can be used to describe behaviour patterns of truth values in generic multiverses. I will illustrate this application of modal logic by giving a characterisation of the modal logic of forcing, which is the modal logic expressing exactly those behaviour patterns of truth values which are common to all generic multiverses. The method to prove this result was introduced by Joel D. Hamkins and Benedikt Löwe in 2008 and is applicable to the investigation of modal logics related to other set theoretic model constructions. Finally I will point to a few open questions.
binary relation R relating a model N to N' iff N'can be obtained via forcing from N. We call this the generic multiverse generated by M and it is now natural to wonder what we can say about the general pattern of truth values of set theoretic sentences inside the models of a generic multiverse with respect to the relation R. A useful tool for this is modal logic, whose language an extension of propositional language by a unary operator which we here interpret as "In every model generated by forcing: ...".
Generic multiverses were introduced (in a slightly different form) by Hugh Woodin in 2009 and embedded into the set-theoretic multiverse program (cf. the talk "Multiverse Truth Behaviour Patterns" by Benedikt Löwe below), which serves as the main motivation for studying the former, by Joel D. Hamkins in 2012.
In this workshop I will give an introduction to modal logic and show how it can be used to describe behaviour patterns of truth values in generic multiverses. I will illustrate this application of modal logic by giving a characterisation of the modal logic of forcing, which is the modal logic expressing exactly those behaviour patterns of truth values which are common to all generic multiverses. The method to prove this result was introduced by Joel D. Hamkins and Benedikt Löwe in 2008 and is applicable to the investigation of modal logics related to other set theoretic model constructions. Finally I will point to a few open questions.
Nathan Bowler (Universität Hamburg, Germany)
Borel Determinacy and Infinite Graphs
Borel Determinacy is a deep result within ZF set theory which relies heavily on transfinitely iterated use of the replacement axiom. It does not appear to fit well with other foundational approaches. This wouldn't matter if it were only of set-theoretic interest; however, as I shall explain, it has concrete implications in the field of topological infinite graph theory.
Ulrik Buchholtz (Carnegie Mellon University, USA)
Proof Theory of Homotopy Type Theories
It is my opinion that a proposed class of formal systems for the foundations of mathematics needs to be thoroughly understood in terms of interpretations to and from other such systems, with an eye towards answering questions such as 1) what rests on what?, 2) what is needed for what?, 3) how do things fit together?, and 4) how much strength do various principles buy us? In this talk, I shall give an overview about what is known about these questions for systems for homotopy type theory. I shall recall earlier work on the proof theory on type theory and explain how recent work on cubical type theories furthers our understanding.
fomus_buchholtz_proof-theory.pdf |
Ulrik Buchholtz (Carnegie Mellon University, USA)
Higher Inductive Types and Synthetic Homotopy Theory (Workshop)
Synthetic homotopy theory is a way of doing abstract homotopy theory in such a way that everything we do is invariant under homotopy equivalence. This approach is enabled by homotopy type theory and gives very direct ways of reasoning about homotopy types (analogously to how euclidean geometry provides direct reasoning about points, lines and circles), but otherwise follows the tradition of other approaches to abstract homotopy theory. In the workshop, we shall introduce the basic ideas through many examples, and we shall in particular focus on the use of higher inductive types to furnish us with many constructions on homotopy types. Higher inductive types also figure prominently in other uses of homotopy type theory, and we shall briefly touch on those as well.
fomus_buchholtz_hits.pdf |
Ioanna Dimitriou (University of Bonn, Germany)
Formalising a FOL Set Theory in Isabelle/HOL, in a Textbook Fashion
Isabelle/HOL is classical Higher Order Logic (HOL) with rank-1 polymorphism, with the axioms of infinity and Hilbert choice, and with a mechanism for overloading constant and type definitions. It includes a set theory, which is comparable to ZFC plus an inaccessible cardinal. In this setting, classes are typically formalised as all metafunctions from the type of sets to the type bool (True/False). In the first order logic (FOL) NBG set theory, we have to restrict the accepted metafunction-classes to the ones definable from FOL formulas with class parameters. Moreover, NBG set theory does not automatically include the axiom of choice, yet Isabelle/HOL does.
I will talk about the obstacles we encountered, and the solutions we found, in the process of formalising NBG set theory in Isabelle/HOL, and about how our theory is related to other approaches to set theory in Isabelle. I will present a project of the mathematical logic group in Bonn, namely formalising set theoretic techniques in Isabelle/HOL, in a textbook style that we hope will make formal mathematics and formal set theory, more approachable to the working mathematician and set theorist.
The theory files I will be talking about will be the ones used during my workshop on Monday (17:30-19:00) and Tuesday (14:00-15:30).
I will talk about the obstacles we encountered, and the solutions we found, in the process of formalising NBG set theory in Isabelle/HOL, and about how our theory is related to other approaches to set theory in Isabelle. I will present a project of the mathematical logic group in Bonn, namely formalising set theoretic techniques in Isabelle/HOL, in a textbook style that we hope will make formal mathematics and formal set theory, more approachable to the working mathematician and set theorist.
The theory files I will be talking about will be the ones used during my workshop on Monday (17:30-19:00) and Tuesday (14:00-15:30).
Ioanna Dimitriou (University of Bonn, Germany)
Formalising Set Theoretic Proofs with Isabelle/HOL in Isar (Workshop)
We shall work with a "natural" formalisation of NBG set theory in Isabelle/HOL, "natural" here meaning following a textbook, namely
Mendelson's classic textbook "Introduction to mathematical logic", Chapter 4: "An axiom system" (Chapman & Hall, 4th edition, 1997). This formalisation is based on this textbook, mainly because it presents the finite axiomatisation of NBG set theory, which simplifies setting up the basics of our theory.
I will only shortly talk about other set theories in Isabelle, the reasons for choosing our theory, and the obstacles we encountered during this formalisation. More details will be given during my talk on Saturday. In this workshop, we shall concentrate on formalising set theoretic proofs in this system, in Isabelle's human readable proving language Isar (Intelligible semi-automatic reasoning).
The workshop participants are required to bring laptops with Isabelle2016 installed, which can be found in https://isabelle.in.tum.de/ for all operating systems, and to download relevant files from the workshop website, starting from June 30: http://www.math.uni-bonn.de/people/dimitri/FOMUS2016-workshop.shtml
This website contains an example proof in our theory, written with Isar in Isabelle/HOL.
Mendelson's classic textbook "Introduction to mathematical logic", Chapter 4: "An axiom system" (Chapman & Hall, 4th edition, 1997). This formalisation is based on this textbook, mainly because it presents the finite axiomatisation of NBG set theory, which simplifies setting up the basics of our theory.
I will only shortly talk about other set theories in Isabelle, the reasons for choosing our theory, and the obstacles we encountered during this formalisation. More details will be given during my talk on Saturday. In this workshop, we shall concentrate on formalising set theoretic proofs in this system, in Isabelle's human readable proving language Isar (Intelligible semi-automatic reasoning).
The workshop participants are required to bring laptops with Isabelle2016 installed, which can be found in https://isabelle.in.tum.de/ for all operating systems, and to download relevant files from the workshop website, starting from June 30: http://www.math.uni-bonn.de/people/dimitri/FOMUS2016-workshop.shtml
This website contains an example proof in our theory, written with Isar in Isabelle/HOL.
Mirna Džamonja (University of East Anglia, UK)
A New Look at an Old Lady: Modern Set Theory and its Place in the Foundations of Mathematics
Gödel taught us that our dreams about perfect foundations of mathematics will not be fulfilled by writing a reasonable list of axioms in the first order logic. Hence, set theory ZFC cannot give us the promised paradise. Almost a century later, after some mini-wars between various approaches, what is the place of set theory in the foundations of mathematics today? We give a pluralistic vision, accepting that different parts of mathematics need different approaches.
Regula Krapf (University of Bonn, Germany)
Introduction to Forcing (Workshop)
The method of forcing was first used in 1963 by Paul Cohen in order to show that the Continuum Hypothesis is independent of the axioms of Zermelo-Fraenkel set theory (ZFC). Since then, forcing has turned out to be a powerful tool for obtaining independence results in set theory. In this workshop I will give a short introduction to forcing and its applications.
James Ladyman (University of Bristol, UK)
Does HoTT Provide a Foundation for Mathematics?
Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory, that offers an alternative to the foundations provided by ZFC set theory and category theory. This paper explains and motivates an account of how to define, justify and think about HoTT in a way that is self-contained, and argues that so construed it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be expected to answer, and find that the standard formulation of HoTT as presented in the `HoTT Book' does not answer many of them. More importantly, the presentation of HoTT given in the HoTT Book is not 'autonomous' since it explicitly depends upon other fields of mathematics. In particular, an important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory’s types, tokens, and identities as (respectively) spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. We offer a derivation of path induction, motivated from pre-mathematical considerations, without recourse to homotopy theory. We use this as part of an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on an interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory.
Benedikt Löwe (Universität Hamburg, Germany & Universiteit van Amsterdam, Netherlands)
Multiverse Truth Behaviour Patterns
In his "The set-theoretic multiverse" (2012), Hamkins argues that the multiverse view of set theory "explains our experience with the
enormous diversity of set-theoretic possibilities, a phenomenon that challenges the universe view". Hamkins's multiverse view gives rise to a foundational setting in which the role of (absolute) truth values is replaced by the behaviour patterns of truth values throughout the multiverse. We compare this setting with the theory of truth, where self-referential sentences can be classified according to their revision-theoretic truth value behaviour. Finally, we give an overview of known truth behaviour patterns in the multiverse and list interesting questions.
enormous diversity of set-theoretic possibilities, a phenomenon that challenges the universe view". Hamkins's multiverse view gives rise to a foundational setting in which the role of (absolute) truth values is replaced by the behaviour patterns of truth values throughout the multiverse. We compare this setting with the theory of truth, where self-referential sentences can be classified according to their revision-theoretic truth value behaviour. Finally, we give an overview of known truth behaviour patterns in the multiverse and list interesting questions.
Paige North (University of Cambridge, UK)
Models of Type Theory (Workshop)
I will give an introduction to models of type theory from a categorical perspective. I will discuss problems of strictness that arise and some solutions. I will also discuss the relationship between models of type theory and weak factorization systems. In conclusion, I will give some examples of models in various categories of spaces.
Andrew Pitts (University of Cambridge, UK)
On Proofs of Equality as Paths
In the Type Theoretic approach to mathematical foundations, proofs about properties of mathematical objects can have the same status as the objects themselves. In particular, proofs about equality of objects themselves become mathematical objects that can be studied. The homotopical approach to Type Theory views such proofs of equality as paths, possibly in an abstract sense. Taking this view literally, what is required of an interval-like object I in order to give a model of Type Theory in which elements of identity types really are just functions on I? I will discuss this question and introduce a surprisingly simple coherent theory of the interval that suffices to model Coquand's recent axiomatization of propositional identity types.
Michael Rathjen (University of Leeds, UK)
Relating Type and Set Theories
There exists a fairly tight fit between type theories à la Martin-Löf and constructive set theories (based on intuitionistic logic) such as Constructive Zermelo-Fraenkel Set Theory, CZF and its extensions. Moreover, consistency strength-wise, they can be related to extensions of classical Kripke-Platek set theory.
The technology for determining the (exact) proof-theoretic strength of such theories was developed in the late 20th century. The situation is rather different, though, when it comes to type theories (with universes) having the impredicative type of propositions Prop from the Calculus of Constructions that features in some powerful proof assistants. The aim of the talk is to present some of the current knowledge.
The technology for determining the (exact) proof-theoretic strength of such theories was developed in the late 20th century. The situation is rather different, though, when it comes to type theories (with universes) having the impredicative type of propositions Prop from the Calculus of Constructions that features in some powerful proof assistants. The aim of the talk is to present some of the current knowledge.
Andrei Rodin (Saint Petersburg State University, Russia)
Proofs and Objects in HoTT
HoTT supports and exemplifies a concept of theory, which differs from the standard notion used in the mainstream logical discussion in the 20th century. While the standard notion construes a theory as a set of propositions, HoTT supports a notion of theoretical object that serves as a vehicle of both propositional and non-propositional contents. This non-standard view on theories and their models appears unusual in the context of mathematical logic of the 20th century but it has strong historical roots in some earlier logical traditions and in the current mathematical practice.
The talk is based on my paper “On Constructive Axiomatic Method” (arXiv:1408.3591).
The talk is based on my paper “On Constructive Axiomatic Method” (arXiv:1408.3591).
Urs Schreiber (Czech Academy of Sciences, Czechia)
Modern Physics Formalized in Modal Homotopy Type Theory
Homotopy type theory is argued to have semantics in infinity-toposes. Under this translation, modal operators are interpreted as idempotent infinity-(co-)monads. Remarkably, a simple progression of adjoint idempotent infinity-(co-)monads on an infinity-topos ("differential cohesion") provides enough structure to elegantly axiomatize large fragments of modern physics: pre-quantum local variational field theory, Noether's theorem, BPS charges, etc. Hence all of this lends itself to synthetic formalization in HoTT. The talk gives a survey of the relevant cohesive infinity-topos theory and of the first steps of formalizing it in HoTT, due to Shulman and Wellen.
Bas Spitters (Aarhus University, Denmark)
Sets in Homotopy Type Theory
We consider 0-types, so-called hsets, in the univalent foundation. We show that they satisfy the categorical axioms of a structural set theory with natural numbers, dependent (co)products, image factorizations, quotients, the axiom of description and (large) power sets. Technically 0-types form a (predicative) topos. Using classical logic, we even have a model of Lawvere set theory. In conclusion, we retrieve the set theoretic foundations with the univalent foundations. This may be viewed in the light of Voevodsky's simplicial set model which shows that conversely the univalent foundations may be modeled in ZFC (or Lawvere) set theory.
This is based on the article:
Egbert Rijke and Bas Spitters. "Sets in homotopy type theory."
Mathematical Structures in Computer Science 25.05 (2015): 1172-1202.
http://journals.cambridge.org/abstract_S0960129514000553
This is based on the article:
Egbert Rijke and Bas Spitters. "Sets in homotopy type theory."
Mathematical Structures in Computer Science 25.05 (2015): 1172-1202.
http://journals.cambridge.org/abstract_S0960129514000553
fomus_slides_spitters.pdf |
Thomas Streicher (Technische Universität Darmstadt, Germany)
Isomorphic Types are Equal!?
We describe the route how Martin Hofmann and myself arrived at the Groupoidmodel and describe how from that one can arrive at the simplicial model of Voevodsky. We also describe a construction of a univalent universe alternative to the one by Voevodsky.
Claudio Ternullo (University of Vienna, Austria)
Multiversism and Naturalism
In a recent paper, [3], Maddy has argued that there is presently no conclusive reason to construe set theory as being concerned with a multiverse rather than with the universe V. The overall goal of my talk is to provide a careful response to Maddy, which should, ideally, help make a full case for the multiverse view.
First, I will briefly review alternative accounts of the set-theoretic multiverse as can be found in the literature (e.g., [2], [4], [5], [6] and, specially, my [1]) and I will then argue that a multiverse theory may be epistemically more attractive than a universe theory, in particular with reference to foundational requirements that a maddian naturalist or arealist is likely to feel as most prioritary, such as, for instance:
[1] C. Antos, S.-D. Friedman, R. Honzik, and C. Ternullo. Multiverse Conceptions in Set Theory. Synthese, 192(8):2463–2488, 2015.
[2] J. D. Hamkins. The Set-Theoretic Multiverse. Review of Symbolic Logic, 5(3):416–449, 2012.
[3] P. Maddy. Set-Theoretic Foundations. September 2015.
[4] J.R. Steel. Gödel’s Program. In J. Kennedy, editor, Interpreting Gödel. Critical Essays, pages 153–179. Cambridge University Press, Cambridge, 2014.
[5] J. Väänänen. Multiverse set theory and absolutely undecidable propositions. In J. Kennedy, editor, Interpreting Gödel. Critical Essays, pages 180-205. Cambridge University Press, Cambridge, 2014.
[6] W. H. Woodin. The Realm of the Infinite. In W. H. Woodin and M. Heller, editors, Infinity. New Research Frontiers, pages 89–118. Cambridge University Press, Cambridge, 2011.
First, I will briefly review alternative accounts of the set-theoretic multiverse as can be found in the literature (e.g., [2], [4], [5], [6] and, specially, my [1]) and I will then argue that a multiverse theory may be epistemically more attractive than a universe theory, in particular with reference to foundational requirements that a maddian naturalist or arealist is likely to feel as most prioritary, such as, for instance:
- Unification. Set theory is meant to be a conceptually unified arena where the whole of maths can be carried out and its results adequately interpreted. However, a universe theory fails to provide, at least prima facie, an adequate interpretation of the independence phenomenon. On the contrary, a multiverse theory, by suggesting the existence of alternative concepts of set, seems more apt to represent current set-theoretic practice.
- Elucidation. A multiverse theory has better prospects to elucidate the conceptual nature of tools, such as forcing, inner models, ultrafilter constructions, etc. needed to produce set-theoretic models (along the lines, for instance, of Hamkins’ use of a naturalist account of forcing in [2]). While there certainly are ways to construe the existence of different models also within a universe theory, I will argue that it is epistemically more advantageous to resort to a multiverse framework.
- Demise of robust realism. A (mathematical) naturalist/arealist is interested in existence and truth claims, insofar as they serve the purpose of developing mathematics. In particular, the choice of alternative set-theoretic axioms only conforms to internal epistemic criteria, such as success, expedience, omprehensiveness. A multiverse theory seems to be more adequate to reflect the wealth of available choices, as well as connect them to internal criteria of evidence. In particular, a multiverse framework makes the issue of whether a set-theoretic axiom should be adopted on the grounds of its being ‘true’ in V irrelevant.
[1] C. Antos, S.-D. Friedman, R. Honzik, and C. Ternullo. Multiverse Conceptions in Set Theory. Synthese, 192(8):2463–2488, 2015.
[2] J. D. Hamkins. The Set-Theoretic Multiverse. Review of Symbolic Logic, 5(3):416–449, 2012.
[3] P. Maddy. Set-Theoretic Foundations. September 2015.
[4] J.R. Steel. Gödel’s Program. In J. Kennedy, editor, Interpreting Gödel. Critical Essays, pages 153–179. Cambridge University Press, Cambridge, 2014.
[5] J. Väänänen. Multiverse set theory and absolutely undecidable propositions. In J. Kennedy, editor, Interpreting Gödel. Critical Essays, pages 180-205. Cambridge University Press, Cambridge, 2014.
[6] W. H. Woodin. The Realm of the Infinite. In W. H. Woodin and M. Heller, editors, Infinity. New Research Frontiers, pages 89–118. Cambridge University Press, Cambridge, 2011.
Vladimir Voevodsky (Institute for Advanced Study, Princeton, USA)
Multiple Concepts of Equality in the New Foundations of Mathematics
One of the most confusing aspects of the Univalence Axiom (UF) is that it seems to assert that, which mathematical students learn early in their education to be a mistake - that isomorphic objects are equal. The source of the confusion is in the failure of the earlier attempts to explain UF to emphasize the existence of two classes of equalities in the theories used to formalize it - substitutional equalities and transportational equalities. The concept of transportational equality is the adaptation to the precise requirements of a formal theory of the philosophical equality principle going back to Leibniz. The concept of the substitutional equality is the one that we all learn at school. In the original formal system used for the Univalent Foundations there was one transportational and one substitutional equality. In the more complex formal systems that are being studied now there can be several equalities of each class.
voevodsky_slides_fomus.pdf |
Philip Welch (University of Bristol, UK)
Proving Theorems from Reflection
In the recent decades set theorists have provided answers to thorny questions in analysis from strong axioms of infinity. These questions fall short of the Continuum Problem, but nevertheless would otherwise have been considered independent of the ZFC axioms. The ostensible paradox of the last statement is resolved by strengthening the ZFC axiom base with so-called 'strong axioms of infinity'. However the justification of these axioms as postulates is considered by some as problematic. We argue that 'Global Reflection Principles' which bite the Cantorian bullet of considering both sets and proper classes, can be deployed to pass over the usual threshold of reflection principles limiting them to the Goedelian universe of constructible sets. Questions concerning the Luzin projective sets in analysis (which naturally extend the Borel) then drop out by earlier work of Martin-Steel, Woodin et al. as these principles readily deliver the assumptions needed for their theorems.
fomus_slides_welch.pdf |