Unless otherwise indicated, all meetings take place on Tuesdays at 4:30PM at 380-381T
The seminar is led by Professor Solomon Feferman
Autumn
This quarter we shall largely be making use of materials from the Exploring the Frontiers of Incompleteness (EFI) workshops held at Harvard in 2011-2012. The EFI site provides background materials, a series of eleven individual lectures and/or individual workshop materials. Some of the topics discussed are the incompleteness phenomena for set theory, the programs for new axioms--in particular large cardinal axioms--to overcome incompleteness, the axiom of determinacy, and the continuum problem. This material is of great active logical and philosophical interest. It will be assumed that participants have a background in first order logic through the completeness theorem as well as introductory set theory.
- Sept 22: Solomon Feferman (Stanford), Introduction to Axiomatic Set Theory, Part I
Materials: handout - Sept 29: Solomon Feferman (Stanford), Introduction to Axiomatic Set Theory, Part II
Materials: handout - Oct 6: Rick Sommer (Stanford), Introduction to Forcing and its Applications
Abstract (+/-):This talk will provide an introduction to Cohen's method of forcing and its application in proving the independence of the Continuum Hypothesis from ZFC. The basic definitions, framework, and ideas will be given without detailed proofs. We will also survey other important independence results that are obtained with the method of forcing.
- Oct 13: J.T. Chipman (Stanford), Introduction to Classical Descriptive Set Theory
Materials: handout
Abstract (+/-):Descriptive set theory is part of the mathematical basis for Godel's Program. That is, the program to "decide mathematically interesting questions independent of ZFC in well-justified extensions of ZFC" (Steel). Classical descriptive set theory, however, was developed over 30 years before independence phenomena were even discovered. In this presentation, we describe and motivate the major results of the classical theory, which concern properties of "well-behaved" subsets of the continuum. We then show how, if the classical results are to be developed further, philosophically controversial metamathematical barriers must addressed.
This presentation is the first of two. The second (Oct 20) concerns principles of definable determinacy. Projective Determinacy, in particular, is thought to solve all of the questions raised by the classical theorists by way of "a well-justified extension of ZFC."
- Oct 20: J.T. Chipman (Stanford), Principles of Definable Determinacy
Materials: handout
Abstract (+/-):Suppose that, for every instance of a given class of infinite games, there exists a winning strategy. The sets over which such games are "played" are then called determined. And, if these sets comprise an adequate pointclass, the regularity of this pointclass follows from its determinacy. Martin (1974) proves determinacy of the Borel sets. This result is of foundational significance---Friedman (1971), for instance, supplies a principled sense in which Martin's result is "best possible" in ZFC.
Last week (Oct 13), by contrast, we saw that the regularity of projective sets beyond those of very low rank is independent of ZFC. If we accept Martin and Steel's proof that the projective sets are determined (1985), however, it follows that the projective sets have the regularity properties after all. This proof is controversial insofar as it assumes the existence of certain large cardinals. This week (Oct 20), we therefore develop some elementary aspects of mathematical and philosophical analyses of that assumption.
- Oct 27: Larry Moss (Indiana), Thirty Years of Coalgebra: What Have We Learned?
Materials: handout
Abstract (+/-):Peter Aczel visited CSLI here at Stanford during the year 1984-85. During that time, he wrote the book Non-Well-Founded Sets. The most lasting contribution of that book was not to set theory itself but rather to other areas. These other areas include theoretical computer science, especially those parts of semantics where one needs circular processes and discrete dynamical systems of various sorts. The point is that Aczel phrased his results in the more general language of coalgebras and also worked with some associated concepts from category theory. When people saw that the more general concepts had applications to things in which they were interested, the subject took off. Coalgebra has been extensively developed and now offers a lot of ideas and connections that should be of interest to logicians. To name some examples: generalizations of modal logic in various ways, corecursion, algebraic characterizations of the real unit interval and of some fractal sets, and constructions of reflexive objects in domain theory and of types spaces in economics.
This talk will survey some of what has been done, centered on constructions of final coalgebras for various functors.
For background, I suggest the SEP site, especially Section 4.
- Nov 3: Chris Mierzewski (Stanford), Measurable Cardinals, Constructibility, and Scott’s Theorem
Materials: handout
Abstract (+/-):In his doctoral thesis, Lebesgue posed his well-known Measure Problem, which asks whether there exists a non-trivial, universal measure over the reals that is translation invariant. Vitali famously settled this question in the negative, relying on the Axiom of Choice.
A quarter of a century later, Banach formulated a more general question, in a slightly modified form: are there any (uncountable) sets admitting a non-trivial universal measure? This line of inquiry led Ulam to consider the existence of cardinals that admit a special kind of measure with strong additivity properties, which gave rise to the notion of 'measurable cardinal'. Tarski and Ulam then proved that measurable cardinals are inaccessible, which entails that the existence of measurable cardinals cannot be settled within ZFC. Thus emerged, from Lebesgue’s old problem, an interesting set-theoretic question touching upon the foundations of mathematics.
In 1961 Scott showed, via an elegant ultrapower construction, that the existence of measurable cardinals entails that V is not equal to L. In this sense, the question of whether measurable cardinals exist provides the first example of a large cardinal axiom that discriminates between Godel’s constructible universe and models of ZFC admitting non-constructible sets.
This talk will be devoted to presenting Scott’s proof. We will see how to generalise the ultrapower construction to proper classes (via "Scott’s trick") and clarify the relationship between measurable cardinals and non-trivial embeddings of the set-theoretic universe.
- Nov 10: Joseph Helfer (Stanford), The Interpretability Hierarchy
Abstract (+/-):Interpretability formalizes the notion of modelling one first-order theory in another. The relation "S is interpretable in T" forms a partial order on the class of all theories (up to a certain equivalence). This gives us a framework in which we can compare various extensions of ZFC, and in doing so, we discover a surprisingly well-behaved hierarchy of theories.
- Nov 17: Solomon Feferman (Stanford), The Continuum Hypothesis is Neither a Definite Mathematical Problem Nor a Definite Logical Problem
Materials: handout
Abstract (+/-):The title of the talk is the same as for the revised version of my contribution to the EFI project, and that is posted on my home page at http://math.stanford.edu/~feferman/papers/CH_is_Indefinite.pdf/. Participants are urged to read that before the seminar meeting. In my talk I will summarize the arguments and explain technical points. For a quick preview, see also the slides for an earlier version at http://math.stanford.edu/~feferman/papers/CH-Millennium.pdf/.
- Nov 24: Thanksgiving Break
- Dec 1: Thomas Icard (Stanford), A Survey on Topological Semantics for Provability Logics
Materials: handout
Abstract (+/-):This will be a survey of ideas and results on topological interpretations of provability logics, especially polymodal provability logics. Esakia first proved completeness for the basic Gödel-Löb logic of provability with respect to scattered spaces. Abashidze and Blass (independently) proved completeness w.r.t. a particular scattered space defined on the ordinal ωω. I will discuss older work of my own that extended the Abashidze-Blass result to a polymodal provability logic, which is complete with respect to a polytopological space on ε0. I will then discuss more recent developments, including work by Beklemishev, Fernandez-Duque, Joosten, Gabelaia, Aguilera, and others, generalizing and improving upon much of this.
Winter
After the first week, the material for the seminar will be drawn from the book, Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena by Jon Barwise and Larry Moss. It is available as a paperback at a reasonable price from online sellers, and also available online at the Stanford Libraries. I will reserve a copy for Tanner Library.
In the first part of the seminar we will cover the material from Part III, Chs. 6-9 on non-wellfounded set theory ZFA. Please read Ch. 2, a review of set theory in the form that will be needed for the construction of a model of ZFA. Participants are hereby encouraged to volunteer in advance for presentations of the chapters in Part III.
The material in the second half of the seminar will be decided later. One natural choice would be to cover Chs. 14-17 with applications to theoretical computer science: largest fixed points, co-induction, co-recursion and co-algebras. But there are several other options to consider.
The seminar will meet in Room 380D Tuesdays 4:30-5:50.
- Jan 12: Peter Koellner (Harvard), Feferman and the Case for New Axioms
Abstract (+/-):I will begin with a brief review of Feferman's work on predicative set theory, semi-constructive systems of set theory, and his philosophical critique of classical analysis and set theory. I will then critique this critique and, more positively, make a case for new axioms which, I will argue, is stronger than one might have ever hoped, given the phenomenon of incompleteness and independence. Whether this case is strong enough to warrant rational acceptance is something that we can debate during the discussion period.
- Jan 19: Solomon Feferman (Stanford), Introduction to Vicious Circles
Abstract (+/-):I will present the requisite background for the work for this quarter based on the book Vicious Circles by J. Barwise and L. Moss. (As previously announced, the book is available online from the Stanford libraries; there is also a copy on reserve in Tanner Library, Bldg.90.) My introduction will be drawn from Parts I and II of the book. In the seminar we will follow up with Part III which is devoted to the construction of a model of set theory with the Foundation Axiom replaced by the Anti Foundation Axiom (AFA). To be decided later is what further material to cover from the book.
- Jan 26: Shane Steinert-Threlkeld (Stanford), Two Formulations of the Anti-Foundation Axiom
Abstract (+/-):I will present material from chapter 7 and the beginning of chapter 10. We will see Barwise and Moss' formulation of AFA as well as Aczel's original formulation and show that the two are equivalent.
- Feb 2: Chris Mierzewski (Stanford), Bisimulations in ZFC
Abstract (+/-):We will cover material from chapters 7 and 10 of Barwise and Moss. We will define bisimulations and prove that flat systems of equations are bisimilar if and only if they have the same solution sets. We will then discuss the relation between bisimulations and the Axiom of Extensionality, and show how bisimulations provide an identity criterion for sets in ZFA. Lastly, we will briefly discuss bisimulations between labelled graphs, and show that each such graph admits a unique (canonical) representation.
- Feb 9: no seminar this week
- Feb 16: Francesca Zaffora Blando (Stanford), Substitution and the General Solution Lemma
Abstract (+/-):We will cover material from Chapter 8 of Barwise & Moss. We will discuss the notion of a general system of equations and the substitution operation needed to adapt the definition of a solution function to this generalised setting. We will prove that the substitution operation exists and is unique. Then, we will go through the proof of the General Solution Lemma, which has the advantage of being directly applicable to equations involving, for instance, natural numbers or ordered pairs. We will conclude by showing that, in ZFC¯, AFA is equivalent to the General Solution Lemma.
- Feb 23: Francesca Zaffora Blando & Chris Mierzewski (Stanford), A model of non-well-founded set theory: the relative consistency of ZFA
Abstract (+/-):In this talk, based on chapter 9 of Barwise and Moss, we construct a model of set theory satisfying the Anti-Foundation Axiom. The construction consists in extending a model of ZFC¯ to a larger universe in which all flat systems of equations admit (unique) solutions, by taking appropriate equivalence classes of pointed flat systems of equations. This shows that ZFA is consistent relative to ZFC¯: in this sense, one can safely enrich the set-theoretic universe with non-well founded sets.
- Mar 1: J.T. Chipman (Stanford), Games and Bisimulation for Non-wellfounded Sets
Abstract (+/-):Chapter 12 of Barwise and Moss. Two-player, non-wellfounded games of perfect information are defined and their novelty briefly illustrated in terms of classical determinacy properties. Then a game is defined for pairs of pointed systems of equations. Players take turns by legal selection of indeterminates from this pair, the result of which is a play. The players' winning conditions, which ensure no infinite play is winning for I, are used to define a relation on pointed systems of equations. Last, we show that these relations are exactly the bisimulations on such equations.
- Mar 8: Joseph Helfer (Stanford), Streams
Abstract (+/-):We will cover material from chapter 14 of Barwise & Moss. We will familiarize ourselves with our first example of a co-inductive structure, streams (which are actually just sequences, defined in a funny way), and see how the ideas of coinduction, corecursion, fixed points of operators, and universal coalgebras come into play in this example.
Spring
The seminar will meet in Room 380-381T Tuesdays 4:30-5:50.
- April 5: no seminar this week (Tarski Lectures at UC Berkeley)
- April 12: Ed Zalta (Stanford/CSLI), Infinity Without Mathematical Primitives or Axioms
Abstract (+/-):In this talk, I show how the existence of numbers, an infinite number, and an infinite set can be proved without any mathematical primitives or mathematical axioms. The derivation takes place in the extended theory of abstract objects. In contrast to ZF, we don’t assert an axiom of infinity, and in contrast to second-order logic extended by Hume's Principle (#F = #G iff there is a 1-1 correspondence between F and G), we don't take #F as a primitive notion or Hume’s Principle as a axiom. Nevertheless, some key parts of the strategy used in Frege's Theorem (http://plato.stanford.edu/entries/frege-theorem/) are preserved. The results are not intended as a replacement for any part of mathematics, but rather as a study into a body of logical concepts and principles from which something infinite emerges.
- April 19: Johan van Benthem (Stanford/UvA), Instantial Neighborhood Logic
Abstract (+/-):Neighborhood models generalize relational graph semantics for modal logic, offering more generality covering also old topological and new hyper-intensional semantics. Any generalized model class suggests richer logical languages. We introduce and explore a new 'instantial neighborhood logic' that can describe the full content of neighborhoods, and show where this style of thinking leads us.
- April 26: Rasmus Grønfeldt Winther (UC Santa Cruz), The "Mapping" Concept in Mathematics: Potential Cartographic Influences?
Abstract (+/-):Formally speaking, a mapping is "a correspondence by which each element of a given set has associated with it one element (occas., one or more elements) of a second set." (OED). What is the role of mapmaking and cartography in the history and philosophy of the "mapping" concept across mathematics and the exact sciences? How might the related formal concepts of "function" and "representation" also resonate cartographically? Is the polysemy of "map" in English an accident, or are there historical or conceptual reasons for it? A tentative archaeology of various sub-fields in 19th and early 20th century mathematics reveals possible influences and resonances of mapmaking, cartography, and the earth sciences on the concepts of "mapping" (English), and "Abbildung" and "Zuordnung" (German). The work of CF Gauss, Bernhard Riemann, Richard Dedekind, Ernst Mach, Henri Poincaré, Hermann Weyl, and Ludwig Wittgenstein, among others, is excavated for this conceptual genealogy. The exploration of surprising analogies and styles of reasoning may shed new light on the foundations of mathematics.
- May 3: no seminar this week
- May 10: Natarajan Shankar (SRI), PVS and the Pragmatics of Formal Proof
Abstract (+/-):A formal system establishes a trinity between language, meaning, and inference. Many domains of thought can be captured using formal systems in such a way that sound conclusions can be drawn through correct inferences. Philosophers have long speculated about machines that can distinguish sound arguments from flawed ones, and with modern computing, we can realize this dream to a significant extent. A research program to mechanize formal proof inevitably confronts a range of foundational and pragmatic choices. Should the foundations be classical or constructive, and should they be based on set theory, type theory, or category theory? What definitional principles should the language admit? How can formalizations be constructed from reusable modules? Should proofs be represented in a Hilbert calculus, natural deduction, or sequent calculus? Which inference steps in the proof calculus can and should be effectively mechanized in order to close the gap between informal arguments and their formal counterparts? The Prototype Verification System (PVS) developed at SRI over the past twenty five years is an interactive proof assistant aimed at capturing the pragmatic features of mathematical expression and argumentation. The PVS language augments a simply typed higher-order logic with subtypes, dependent types, and algebraic datatypes. The PVS interactive proof checker integrates a number of decision procedures into the sequent calculus proof system. We examine the implications of these choices for the original goal of constructing mathematically sound arguments.
- May 17: Christoph Benzmueller (FU Berlin), The Inconsistency in Gödel’s Ontological Argument: An Application of Mathematical Proof Assistants in Metaphysics
Abstract (+/-):I will report on the discovery and verification of the inconsistency in Gödel’s ontological argument with reasoning tools for higher-order logic. Despite the popularity of the argument since the appearance of Gödel’s manuscript in the early 70's, the inconsistency of the axioms used in the argument remained unnoticed until 2013, when it was detected automatically by the higher-order theorem prover LEO-II.
Understanding and verifying the refutation generated by LEO-II turned out to be a time-consuming task. Its completion required the reconstruction of the refutation in the Isabelle/HOL proof assistant. This effort also led to a more efficient way of automating higher-order modal logic S5 with a universal accessibility relation within the logic embedding technique we utilize in our work.
The development of an improved syntactical hiding for the logic embedding technique allows the refutation to be presented in a human-friendly way, suitable for non-experts in the technicalities of higher-order theorem proving. This should bring us a step closer to wider adoption of logic-based artificial intelligence tools by philosophers.
If time permits, I will also point to alternative, ongoing applications of the logic embeddings technique.
- May 24: Wesley Holliday (UC Berkeley), Complete Additivity and Modal Incompleteness
Abstract (+/-):This talk, based on joint work with Tadeusz Litak, will tell a story about incompleteness in modal logic. The story weaves together a paper of van Benthem (1979), "Syntactic aspects of modal incompleteness theorems," and a longstanding open question—whether every normal modal logic can be characterized by a class of completely additive modal algebras. Using a first-order reformulation of the property of complete additivity, we will prove that the modal logic that starred in van Benthem's paper resolves the open question in the negative. In addition, for the case of bimodal logic, we will show that there is a naturally occurring logic that is incomplete with respect to completely additive modal algebras, namely the provability logic GLB. After presenting these results, we will relate them to van Benthem's theme of syntactic aspects of modal incompleteness. Time permitting, we will also explain how the famed Blok Dichotomy can be generalized to degrees of incompleteness with respect to completely additive modal algebras.
- May 31: Valeria de Paiva (Nuance), Constructive Modal Logics: A Personal Overview
Abstract (+/-):This talk will review the program of intuitionistic modal logic considered from its two original sources: modal logicians interested in Intuitionism and functional programmers/type theorists interested in (computational) modalities. I will discuss some trends of this kind of work since the first Intuitionistic Modal Logic and Applications (IMLA) in Trento in 1999 and the tendencies that we can see in this line of work today.
Last modified