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 TT_{3} (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 TT_{3}, 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
TT_{3}) 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 NF_{3}, 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.