Groupe de contact Décembre 2005

Groupe de contact à l'ULB : "Set Theory in the third Millenium "

JEUDI 1 décembre 2005 : LOCAL 2-NO-906

* 14.00 : P.Aczel (Manchester) : An Introduction to Constructive Set Theory
* 15.15 : M.Forti (Pise) : A tradition-preserving way of counting infinite sets
* 16.30 : pause café
* 17.00 : T.Forster (Cambridge) : Stratified formulae in ZF

Repas du soir : probablement au restaurant « Le Campus » ; à charge des participants ( non-conférenciers du 1&2 décembre, bien sûr), vers 19.00; les personnes désireuses de se joindre à ce repas sont priée d'envoyer un e-mail à : rhinnion@ulb.ac.be, pour le 25 novembre au plus tard.

VENDREDI 2 décembre 2005 : LOCAL 2-NO-906

*14.00 : S.Tupailo (Tallin) : Monotone Inductive Definitions and consistency of New Foundations
* 15.15 : M.Forti (Pise) : Leibniz Principles and Topological Nonstandard Extensions
* 16.30 : pause café

Conférences de la Société Belge de Logique & Philosophie: Local probable : Salle Solvay, niveau 5, bâtiment NO, local 2-NO-507

* 17.00 : T.Forster (Cambridge) : The Iterative Conception of Set
* 18.15 : P.Aczel (Manchester) : The Constructive Notion of Set

Repas du soir : restaurant à fixer ; vers 20h00 ; à charge des participants (non-conférenciers, bien entendu) ; les personnes désireuses de se joindre à ce repas sont priées d'envoyer un e-mail à : tlibert@ulb.ac.be , pour le 25 novembre au plus.

Résumés:

Peter Aczel (Manchester) : An Introduction to Constructive Set Theory
The topic of Constructive Set Theory (CST) was initiated by John Myhill in his 1975 JSL paper. In the late 1970s and early 1980s I published a sequence of three papers in which I formulated a variant formal system, CZF, of the system introduced by Myhill, and gave a type theoretic interpretation of CZF and various extensions of it. CST provides a natural extensional setting in which to develop constructive mathematics in a similar style to the standard set theoretical approach used in presenting classical mathematics. My talk will introduce CZF and its use as a formal system for the development of elementary constructive mathematics.

Marco Forti (Pise) : A tradition-preserving way of counting infinite sets
The naive idea of ``size'' for collections seems to obey both to Aristotle's Principle: ``the whole is greater than its parts'' and to Cantor's Principle: ``1-to-1 correspondences preserve size''. Notoriously, Aristotle's and Cantor's principles are incompatible for infinite collections. Cantor's theory of cardinalities weakens the former principle to ``the part is not greater than the whole'', but the outcoming cardinal arithmetic is very unusual. In particular it does not allow for inverse operations, and so there is no natural way of introducing infinitesimal numbers. We aim to maintain Aristotle's principle, and we half instead Cantor's principle to ``equinumerous collections are in 1-1 correspondence''. (But large classes of ``natural'' correspondences preserve size). In this way we obtain a very nice arithmetic: in fact, our ``numerosities'' may be taken to be nonstandard integers, and so the five "common notions" of Euclid's Elements are all preserved.

Thomas Forster (Cambridge) : The stratified formulae in ZF
The theory axiomatised by all the stratified axioms of ZF is a subsystem of NF and it is not obviously impossible that a consistency proof for NF might emerge from the study of it. It is even know that this theory has nontrivial models (= not satisfying ZF) in which AC fails. I shall present a summary of what is know, and develop some hopes for the future

Sergei Tupailo (Tallin) : Monotone Inductive Definitions and consistency of New Foundations
We present -- yet another one -- reduction of NF to an extension of NFU. We apply the so called bisimulation method in order to model NF in an appropriate NFU's extension. This method has been used in many different situations, when there was a need to satisfy Extensionality in a non-extensional, non-wellfounded, framework. It is a standard tool for modelling Set Theory in Analysis. Working in NFU+Pairing, NFUP (consistent by [Jensen 1969]), we define a certain monotone operation pw acting on sets of trees and conclude the following :

Lemma 3.4 : Any set models all Equality axioms of NF,

Lemma 3.19 : Any fixpoint of the pw operation models Stratified Comprehension,
and
Lemma 3.18 : Any least fixpoint, in addition, models Extensionality.

Thus, existence of a pw- least fixpoint is sufficient to model NF. This connects us with the well-known MID principle, which asserts existence of least fixpoints of monotone operations and has been studied extensively in different areas of Mathematical Logic. For example, in Set Theory, many ZF- large cardinal axioms can be seen as the MID principle for particular monotone operations; in Proof Theory, much research has been done about the MID principle over Peano Arithmetic and subsystems of Analysis; in Computer Science, one manifestation of MID is various mu-calculi.
Related to all of the above, including New Foundations, is the study of MID in Feferman's Explicit Mathematics, EM. Explicit Mathematics can be seen as an extension of NFUP containing only two types; for this reason the only set operations $f$ one can talk about in EM are type-preserving (or type level), i.e. such that $x$ and $f(x)$ must have the same type. However, since EM postulates many more set existence principles than just those provided for by Stratified Comprehension, the very question of consistency and strength of MID becomes very non-trivial; this question has been answered, positively. In NFUP in general, as well, MID for type level operations easily follows from Stratified Comprehension, but the consistency question seems to be much more difficult if the operation is not so. Anyway, for our operation pw, a positive answer would imply Consis(NF).
In our talk, we want to discuss possible ways to tackle this problem. The paper, containing the current result, can be downloaded from http://www.cs.ioc.ee/~sergei/binf-lc05.pdf , and, pending refereeing, will appear in the Proceedings of Logic Colloquium 2005.

Marco Forti (Pise) : Leibniz Principles and Topological Nonstandard Extensions
Three different philosophical principles are often quoted in connection with Leibniz, namely
- Identity of Indiscernibles Principle (IIP) : "objects sharing the same properties are the same object."
- Possible Worlds Principle (PWP) : "everything can possibly exist, unless it yields contradiction."
- Transfer Principle (TP) : "the ideal elements we conceive are useful to correctly determine the real things".
We give a precise interpretation of these principles in the context of Topological Extensions, recently introduced structures which generalize at once compactifications, completions, and nonstandard extensions. We obtain the surprising result that these three principles cannot be simultaneously satisfied, whereas any pair of them can.

Thomas Forster (Cambridge) : The Iterative Conception of Set
"The cumulative hierarchy" and "The iterative conception of sets" are usually taken to be synonymous expressions. However the second is more general than the first, in that there are recursive procedures that generate some illfounded sets as well as wellfounded sets. The interesting question is whether or not the arguments in favour of the more restrictive version - the cumulative hierarchy - were all along arguments for the more general version.

Peter Aczel (Manchester) : The Constructive Notion of Set
I claim that there is a natural constructive notion of set that can be used to interpret formal systems for constructive set theory such as the formal system CZF and various extensions of it. This notion of set has been formulated in Martin-Lof's Intuitionistic Type Theory. In my talk I will try to explain this notion of set informally without presupposing previous familiarity with Martin-Lof's type theory. I will contrast my explanation with the explanations often given for the classical notion of set used to interpret ZFC.

Retour à la page de garde / Back to the homepage Page maintenue par Cédric Rivière