The next meeting is on Thursday 24 November. Venue: Meeting Room 11, Centre for Mathematical Sciences, Wilberforce Road, Cambridge.
Speakers: Greg Restall, Allen Mann, Michael Rathjen, Randall Holmes.
1300: Greg Restall
1420: Allen Mann
1540: Michael Rathjen
1700: Randall Holmes
1815: Drinks, nibbles, etc..
It turns out to be surprisingly straightforward to extend proof nets for classical logic to treat the operators of the simple modal logic S5. In this talk I explain just how you can do that, and -- furthermore -- how you can use the resulting proof nets to define a new, simple, cut-free sequent calculus for S5. Along the way I hope to explain why proof-nets are not merely technical devices but have philosophical application. (This talk motivates the results from the point of view of the philosopher interested in inference, but the connections to category theory and computation are not too far from the surface.)
In The Principles of Mathematics Revisited (1996), Hintikka introduces independence-friendly logic (IF-logic), a conservative extension of first-order logic that allows a quantifier that falls within the syntactic scope of another quantifier to be independent of it. IFG-logic is a generalization of IF-logic introduced by Caicedo, Krynicki, and Dechesne. We present an algebraization of IFG-logic along the lines of cylindric algebra.
The Disjunction and Related Properties for Intuitionistic Set Theories
The talk will be concerned with the disjunction property, the numerical existence property, Church's rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.
As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth. The technique applies to full intuitionistic Zermelo-Fraenkel set theory, IZF, as well.
In TT3 (type theory with just three types) it is impossible to define the usual (Wiener-Kuratowski) ordered pair so it appears difficult to define functions, and defining functions seems to be a conceptual prerequisite for defining cardinality of sets. However, Henrard showed (in unpublished work) that cardinality can nonetheless be defined in three types. We show how it is possible to define almost all functions in TT3, and always to define equinumerosity of sets. In the presence of a linear order on the universe (a condition which can be expressed in the language of TT3) it becomes possible to define an ordered pair and so easily define functions and cardinals. The details of the problem with defining functions make it clear that what is needed to get a full definition of functions is any principle that will allow choice from an arbitrarily large collection of finite sets.
This sheds light on how much mathematics can be done in NF3, the fragment of Quine's New Foundations with full extensionality and all comprehension axioms that can be expressed in three types; we will allude to this but the talk does not depend in any way on knowledge of New Foundations.
Cameleon: November 2005 in Cambridge