Set Theory Day: 24th November. CAMELEON

CAMELEON (CAMbridgE LEeds Or Norwich) exists to further links between logicians at the three universities its name alludes to. It has funding from The London Mathematical Society and The St Luke's Institute.

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.

Provisional timetable

1300: Greg Restall

1420: Allen Mann

1540: Michael Rathjen

1700: Randall Holmes

1815: Drinks, nibbles, etc..

Greg Restall: Proof Nets for the Modal Logic S5

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.)

Allen Mann Algebraic IFG-Logic

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.

Michael Rathjen

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.

M. Randall Holmes
Cardinality and (sometimes) Functions in Three Types

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.

If you want to come to the meeting tell tf@dpmms.cam.ac.uk so we can get a good fix on numbers. There will be a supper after the meeting. Definitely tell tf if you wish to stay for this!

Cameleon: November 2005 in Cambridge

DPMMS front page.