Logic Day: Wednesday April 23rd in Cambridge 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.

April 23rd 2008, Meeeting Room 13, Centre for Mathematical Sciences, Wilberforce Road, CB3 0WB.

The speakers will be Richard Pettigrew, Basil Smith, Grant Passmore, Peter Lumsdaine, Chad Brown and Thierry Libert.

Talks will be at 0900 1030 1200 then 1400 1530 1700 (approximately! Cameleon is not a branch of the armed forces!) Crabbe, Duckerts, Libert, Brown, Pettigrew, Forster, Lumsdaine and Smith will all meet for dinner on april 22nd. Other interested parties are welcome to join.

15:30

Basil Smith:
Back to the roots

Richard Pettigrew, University of Bristol
"Number systems of different lengths, and a natural approach to infinitesimal analysis"
I present a theory of finite sets in which subset comprehension is restricted to bounded quantifier formulae. I define the notion of a natural number system in this theory, and show that Dedekind's Isomorphism Theorem for number systems fails. I give a brief glimpse into how badly it fails, the ways in which it fails, and the bizarre zoology of natural number systems differing in length and closure properties that results. Finally, I explain how one might found a natural version of infinitesimal analysis in this theory.

Thierry Libert, ULB, Brussels.
Positive Frege
We present a consistent fragment of Frege's "Grundgesetze der Arithmetic" as a system of illative lambda calculus. The set-theoretic part of that system is related to what is called Positive Set Theory and it is extensional, unlike most (all?) systems of illative lambda calculus that have been proposed so far. We show how much of arithmetic can be interpreted within the set-theoretic part of the system or in some of its extensions.

Chad E Brown, Saarland University
Nonstandard Models of Fragments of Church's Type Theory
We use logical relations to construct combinatory frames which model fragments of Church's type theory. The frames will not generally realize all the logical constants of Church's type theory and consequently will not satisfy the full set comprehension principles. In particular, we will define a combinatory frame in which a form of Cantor's theorem is false. This frame also has interesting properties with respect to the cardinality of domains at power types.

Grant Passmore. University of Edinburgh
A Family of Decidable Nonlinear Fragments of the True Existential Theory of the Rational Number Field

I am interested in isolating decidable nonlinear fragments of discrete number theories. Of particular interest to me is the isolation of decidable nonlinear fragments of the true existential theory of the rational number field, as the decidability of the full true existential theory of the rational number field (Hilbert's 10th Problem over Q) remains as a difficult and important problem in arithmetic algebraic geometry.
I've recently obtained the following result: Let L be the first-order language of fields restricted to only include WFFs formed with the existential quantifier, disjunction, and relation symbols for disequality and greater-than-or-equal-to in the natural way (note that term formation has not been restricted). Then, the true L-theory of the rational number field is decidable. Moreover, this decidability result holds even when the structure of the rational number field is extended by an arbitrary collection of F-definable `real-extended continuous rational endomaps,' where F is the full first-order language of fields and a `real-extended continuous rational endomap' is a continuous map from R^n -> R with the property that its image over a rational vector is always rational-valued. The proof is very simple, utilizing only rudimentary model-theoretic and topological properties of Euclidean space.
I will present some background on Hilbert's 10th Problem over Q, present this proof, and seek advice from attendees as to (a) whether this result was already known (perhaps it is folklore?), and (b) promising approaches and directions I might head into for hopefully isolating more interesting decidable nonlinear fragments.

Peter LeFanu Lumsdaine: Carnegie-Mellon and Cambridge
Sheaves for constructive set theories
We all know how to model classical first-order logic, by taking a model to be a set with appropriate functions and relations. If you replace "set" by "sheaf", it still works, except that the logic of the model may be not be classical. I will describe --- concretely, accessibly, and with pictures --- the resulting sheaf models of constructive logic, and present an application (due to Lubarsky): a sheaf model in which there exists a Cauchy sequence of rationals with no modulus of convergence.

Boffa and his students Boffa and his students
Cameleon in Leeds in November 2008

DPMMS front page.

Return to Thomas Forster's home page