From cat-dist Thu Apr 1 10:24:48 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id IAA04316
for categories-list; Thu, 1 Apr 1999 08:17:14 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Date: Thu, 1 Apr 1999 13:10:47 +0100 (BST)
From: Paul Taylor
Message-Id: <199904011210.NAA21705@wax.dcs.qmw.ac.uk>
To: categories@mta.ca
Subject: categories: Is Zermelo-Fraenkel set theory inconsistent?
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
IS ZERMELO-FRAENKEL SET THEORY INCONSISTENT?
At the end of this message is a sketch of an argument that leads to
the conclusion that Zermelo-Fraenkel set theory is inconsistent.
The impact on mathematics is not as devastating as the incautious
observer might suppose. Recall that ZERMELO set theory (1908), which
is essentially equivalent to the categorists' notion of ELEMENTARY TOPOS
with natural numbers and the axiom of choice, is adequate for
most of the purposes of mathematics, though not, as I shall try to
explain, logic (and theoretical computer science).
ZERMELO-FRAENKEL set theory is the extension of this system by the
axiom-scheme of REPLACEMENT, which was first formulated by Adolf
(later Abraham) Fraenkel, Nels Lennes and Thoralf Skolem in 1922,
although Dimitry Mirimanoff already had something of the idea in 1917.
Notice that this is some two decades after the appearance of the famous
"antinomies" of set theory, so presumably the set theorists' guard had
dropped by that time, and they had begun again to assert megalomaniac
axioms. On the other hand, it is a decade before the second generation
of paradoxical results, Godel's incompleteness theorem and Turing's
unsolvability of the Halting Problem.
Whenever I see set theory books in a library or bookshop, I turn to
the index to find out what they have to say about Replacement. Usually
there is some trivial result, such as the existence of what categorists
call image factorisation, that could have been proved from Zermelo's
axioms with a little more facility in set-theoretic constructions.
The basic use of Replacement, that you will find in the better set theory
books, is the recursive construction of sets (in substance -- types or
objects to type-theorists and categorists -- rather than their names).
For example, Mostowski's theorem states that every well founded extensional
binary relation < is isomorphic to the membership relation for a unique
transitive set. This is found, recursively, by means of the formula
f(x) = { f(y) | y < x },
which also provides the extensional reflection (quotient) of any well
founded relation. In fact the latter result (where the quotient relation
is merely another relation, rather than a membership relation) can be
proved using the topos or Zermelo axioms alone, and not Replacement [1],
although there are categorical generalisations of this that certainly do
need Replacement.
Richard Montague [2] proved a result that should have been taken as a
warning of the perilous nature of Replacement, though I suspect that
Montague's personal eccentricities may have been the reason why he was
ignored. ZF can prove the consistency, not only of Zermelo set theory (Z)
itself, but also of Z extended by any single theorem of ZF.
Adrian Mathias has claimed [3] that Bourbaki was "ignorant" of Replacement,
ie that it did not occur in "Theorie des Ensembles" [4]. Although
Bourbaki is hardly very clear on this matter, it does include a
version of Replacement in its axioms, indeed one that is in widespread
use in category theory and other parts of mathematics, namely that one
can form the UNION of any SET-INDEXED FAMILY of SETS.
One application of N-indexed unions in theoretical computer science is
Scott's "D-infinity" construction of models of the untyped lambda calculus.
Starting from any domain D0=D, one may form its function-space D1=(D0->D0),
and similarly D2=(D1->D1), etc., linking these together with embedding-
projection pairs. If D was one of the examples of L-domains, having a
pair of elements with infinitely many minimal upper bounds, then one can
show (classically) that D-infinity has the cardinality of a model of
Zermelo set theory, so need not exist within such a model unless it also
satisfies Replacement.
These two ways of seeing Replacement have a common theme: we use N-indexed
or transfinite unions to unfold a free(ish) model of one logic within
a model of another.
Having seen this in the context of a messy domain-theoretic construction,
we may think in a more disciplined way about free models of the lambda
calculus, the topos axioms, etc. In fact, there is no difficulty in
constructing these models, as they are merely TERM ALGEBRAS. The problem
lies in proving that the term algebra has the universal (initiality)
property that qualifies it as "free":
Let S be the universe (the category of ZF-sets, for example)
and F the term algebra (internal to S) for the logic L.
Suppose that S itself is a model of L.
Then there is a unique interpretation functor []:F->S
that takes each syntactic operation of F (eg prod(a,b))
to the semantics ([a] x [b]) in S.
It is merely unique up to unique isomorphism if the L-structure in S is
defined by universal properties rather than being chosen.
This initiality property may also be expressed type-theoretically.
Per Martin-Lof [5] introduced objects with such a property, called UNIVERSES,
observing the analogy with Replacement. This point of view stresses that
the above property is a RECURSION SCHEME.
Let me explain how I came to realise that the existence of []:F->S depends,
in general, on Replacement.
There is an amazingly simple but incredibly powerful argument, due to
Peter Freyd and known variously as (Artin-Wraith) glu(e)ing, sconing,
the Freyd cover, logical relations and other names. It is based on some
very elementary categorical investigations of a certain comma category
involving F and S. This argument has been developed rather a long way
(the most recent paper that I know of is [6]), and we are pretty close
to having a purely categorical proof of the strong normalisation theorem
for lambda calculi that, unlike the syntactic proofs, is completely
generic with regard to the calculus in question.
Freyd originally showed that the terminal object (1) of the free topos (F)
is projective, and more generally the "global sections functor"
F(1,-) : F -> S preserves colimits. In particular, it preserves the
initial object (0), which is categorical jargon for saying that S proves
the consistency of F, because the S-set of F-morphisms 1->0 is the
initial (empty) S-set.
I found this suspicious, because the punch-line of Andre Joyal's 1973
(but as yet unpublished and unavailable) categorical proof of Godel's
incompleteness theorem is that such a functor F(1,-) : F -> S does *not*
preserve the initial object.
The more careful amongst categorists ought also to be suspicious when
I speak of "a functor F(1,-) or [] : F -> S" where F is an INTERNAL
category in S. The meaning that we must give to this phrase is that
it is "syntactic sugar" for a certain FIBRATION p: V -> F, where V is
also an internal category and p and internal functor in S.
This brings us back to the relationship between Replacement as a recursive
construction of objects and Replacement as infinitary colimits:
"p: V -> F" is the colimit (in a 2-category whose objects are fibrations)
of a recursively defined diagram vaguely similar to that which gives Scott's
D-infinity.
I have come to the conclusion that attempts to define "colimits" such as
this are inherently circular: what, after all, does it mean to have a
"cocone" to test such an alleged colimit?
My categorical formulation of Replacement speaks about fibrations
and smaller colimits defined internally in the style of Benabou.
This is to be found in the final section (9.5) of my book [7],
Section 7.7 of which also gives an account of Freyd's gluing construction.
This book is officially due to be published in mid-May, but it is
already in stock (and I have my own copy in front of me), and is
available direct from the publishers at 50 pounds (inclusive of overland
postage and packing). Please contact
Richard Knott,
email: rknott@cup.cam.ac.uk
fax: +44 1223 315 052
tel: +44 1223 325 916 (but other methods are preferable)
snail: Cambridge University Press, The Edinburgh Building,
Shaftesbury Road, Cambridge, CB2 2RU, UK
with your address and credit card number. (2.50 pounds extra for airmail.)
Having seen that Replacement provides a UNIFORM way of proving
consistency of any fragment of logic, we come at last to the
inconsistency argument:
Let L(0) be Zermelo set theory
(or the axioms for an elementary topos).
For each n, let L(n+1) be L(n) plus
as much of the axiom-scheme of replacement as is needed
to justify the gluing construction that shows that
L(n+1) |- ``L(n) is consistent.''
Now let L(infinity) be the union of L(n) over n:N.
If L(infinity) |- false then L(n) |- false for some n.
But L(infinity) |- ``L(n) is consistent,''
so L(infinity) proves its OWN consistency,
contradicting Godel's theorem.
However, L(infinity) has a standard non-trivial interpretation
in Zermelo--Fraenkel set theory, which is therefore inconsistent.
[1] Paul Taylor, Intuitionistic Sets and Ordinals, JSL 61 (1996) 705-44
[2] Richard Montague, Fraenkel's Addition to the Axioms of Zermelo,
pp 91--114 of Bar-Hillel, et al., eds., Essays on the Foundations of
Mathematics, Magnes Press, Hebrew University, 1966 (distributed
by Oxford University Press).
[3] Adrian Mathias, The Ignorance of Bourbaki, Mathematical Intelligencer,
14 (1992) 4-13.
[4] Nicolas Bourbaki, Elements de Mathematique XXII: Theories des Ensembles,
Livre I, Structures, Hermann, 1957 (English translation 1968).
[5] Per Martin-Lof, An Intuitionistic Theory of Types: Predicative part,
pp 73--118 in Rose and Sheperdson, eds., Logic Colloquium '73,
North-Holland, Studies in Logic and the Foundations of Mathematics #80,
1975
[6] Djordje Cubric, Peter Dybjer and Philip Scott, Normalisation and the
Yoneda Embedding, MSCS 8 (1998) 153--192.
[7] Paul Taylor, Practical Foundations of Mathematics, Cambridge University
Press, Cambridge Studies in Advanced Mathematics #59, xii+572pp, 1999.
http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/
Paul Taylor 19990401
This message may be copied elsewhere,
ON CONDITION that it is quoted in its ENTIRETY.
From cat-dist Fri Apr 2 06:24:24 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id FAA23825
for categories-list; Fri, 2 Apr 1999 05:37:38 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Message-ID: <3703D5AD.CEE89138@kestrel.edu>
Date: Thu, 01 Apr 1999 12:23:09 -0800
From: Dusko Pavlovic
X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u)
X-Accept-Language: en
MIME-Version: 1.0
To: CATEGORIES@mta.ca
Subject: categories: Re: Is Zermelo-Fraenkel set theory inconsistent?
References: <199904011210.NAA21705@wax.dcs.qmw.ac.uk>
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
> Let L(0) be Zermelo set theory (or the axioms for an elementary topos).
>
> For each n, let L(n+1) be L(n) plus
> as much of the axiom-scheme of replacement as is needed
> to justify the gluing construction that shows that
>
> L(n+1) |- ``L(n) is consistent.''
>
> Now let L(infinity) be the union of L(n) over n:N.
>
> If L(infinity) |- false then L(n) |- false for some n.
>
> But L(infinity) |- ``L(n) is consistent,''
>
> so L(infinity) proves its OWN consistency,
> contradicting Godel's theorem.
>
> However, L(infinity) has a standard non-trivial interpretation
> in Zermelo--Fraenkel set theory, which is therefore inconsistent.
i think there is a gap is in the step
L(infinity) |- "L(n) is consistent"
so L(infinity) proves its OWN consistency
formalized in a suitable category of theories and interpretations, paul's
construction, if i understand it correctly, refers to the colimit of the tower
L(0) --> FL(0) --> FFL(0) -->...
where FX = X + replacement_X, so that FX |- "X is consistent".
IF the colimit of this tower, paul's L(infinity), were a fixpoint of F, THEN it
would indeed prove its own consistency. but it doesn't seem to be a fixpoint:
the restrictions of the replacement to L(0), FL(0) etc. do not imply the
replacement for L(infinity).
btw, i bought paul's book and warmly recommend it.
-- dusko
From cat-dist Fri Apr 2 06:29:44 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id FAA28262
for categories-list; Fri, 2 Apr 1999 05:36:24 -0400 (AST)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Message-ID: <37039621.7387D2A7@math.ucla.edu>
Date: Thu, 01 Apr 1999 07:52:01 -0800
From: Mike Oliver
Reply-To: oliver@math.ucla.edu
Organization: UCLA
X-Mailer: Mozilla 4.5 [en] (Win95; U)
X-Accept-Language: it
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Re: Is Zermelo-Fraenkel set theory inconsistent?
References: <199904011210.NAA21705@wax.dcs.qmw.ac.uk>
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
Paul Taylor wrote:
> Now let L(infinity) be the union of L(n) over n:N.
>
> If L(infinity) |- false then L(n) |- false for some n.
>
> But L(infinity) |- ``L(n) is consistent,''
>
> so L(infinity) proves its OWN consistency,
> contradicting Godel's theorem.
How do you conclude, from the fact that L(infinity) |- "L(n) is consistent", that
L(n) is in fact consistent?
Generally, if T1 |- "T2 is consistent", then to conclude "T2 is consistent",
we use the following argument: Suppose T2 is inconsistent. Then
there is some proof by which T2 |- false. Assuming T1 is strong enough
to formalize the deductive system being used, then it follows
that T1 |- "T2 is inconsistent". But by hypothesis, T1 |- "T2 is consistent",
therefore T1 is inconsistent.
But this is not a contradiction unless we were already *assuming* the
consistency of T1 ! I.e. it follows from T1+Con(T1) that
if T1 |- Con(T2), then Con(T2), but it does *not* in general
follow from T1 alone.
So the step from
L(infinity) |- "L(n) is consistent"
to
L(n) is consistent
cannot be formalized in any obvious way in L(infinity), and therefore
you cannot (again in any obvious way) conclude
L(infinity) |- "L(infinity) is consistent."
--
Disclaimer: I could be wrong -- but I'm not. (Eagles, "Victim of Love")
Finger for PGP public key, or visit http://www.math.ucla.edu/~oliver.
1500 bits, fingerprint AE AE 4F F8 EA EA A6 FB E9 36 5F 9E EA D0 F8 B9
From cat-dist Tue Apr 6 06:03:11 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id EAA28995
for categories-list; Tue, 6 Apr 1999 04:36:25 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
From: Thomas Streicher
Message-Id: <199904031512.AA079642350@fb0448.mathematik.tu-darmstadt.de>
Subject: categories: Re: incompleteness of ZF
To: CATEGORIES@mta.ca
Date: Sat, 3 Apr 1999 17:12:29 +0200 (MESZ)
X-Mailer: ELM [version 2.4ME+ PL47 (25)]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
Dear Paul,
a short reply to your mail about inconsistency of replacement.
As Paul has already remarked in his mail the type-theoretic counterpart of
replacement is that of universe `a la Martin-Loef. As in case of replacement
the use of universes is that they allow for construction of families of types
(as e.g. needed for inverse limit constructions in Domain Theory which cannot
be performed in pure topos logic precisely for this reason).
But as already observed in a survey article by Thierry Coquand
(ftp://ftp.cs.chalmers.se/users/cs/coquand/meta.ps.Z) and, surely,
known to Martin-Loef himself it holds that in type theory with n+1 universes
one may prove the consistency of type theory with n universes simply by
constructing a model using the n+1st universe. But, of course, this extra
universe is needed for the consistency proof. Accordingly, one cannot prove
the consistency of type theory with $\omega$ universes without postulating an
$\omega$th universe.
Quite the same phenomenon is going on in set theory as already pointed out by
some previous replies. However, in set theory due to the presence of
``impredicative'' axioms the proof theoretic strength is incredibly stronger
than set of Martin-Laoef type theory with $\omega4 universes.
Best, Thomas
From cat-dist Tue Apr 6 06:13:13 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id EAA28154
for categories-list; Tue, 6 Apr 1999 04:51:01 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Date: Mon, 5 Apr 1999 13:25:26 -0400 (EDT)
From: Phil Scott
Message-Id: <199904051725.NAA01504@dinats.mathstat.uottawa.ca>
To: categories@mta.ca
Subject: categories: Position at Ottawa U.
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
The Department of Mathematics and Statistics of the
University of Ottawa is expecting one, if not several,
temporary positions for the upcoming year. The most
significant is the Canadian Mathematical Society
Fellowship. This is a 3 year position (1 + renewable
for 2 years), at the level of Assistant Professor,
with a reduced teaching load of 1 course per semester
available July 1. This position recently became
available when the current holder moved elsewhere. There
may also be one or more temporary positions pending
budgetary approval.
We are hopeful to attract candidates interested in
one or more of the following fields:
1. Categorical and Linear Logic
2. Theoretical Computer Science
3. Tensored Categories
We are also members of the Category Theory Centre in
Montreal (Team members and colleagues include: M. Barr,
M. Bunge, T. Fox, J. Lambek, M. Makkai, P. Panangaden, G.
Reyes, R. Seely). The category team has weekly seminars
(Ottawa is 2 hours from Montreal). We shall also be having
frequent seminars of our team here at U. Ottawa.
If you are interested, please contact one of us by
email right away:
Prof. R. Blute Prof. P. Scott
rblute@mathstat.uottawa.ca phil@mathstat.uottawa.ca
Thanks. We hope to hear from you soon.
Rick Blute and Phil Scott
From cat-dist Wed Apr 7 21:04:31 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id TAA32348
for categories-list; Wed, 7 Apr 1999 19:53:28 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Date: Tue, 6 Apr 1999 17:41:04 -0400 (EDT)
From: F W Lawvere
Reply-To: wlawvere@ACSU.Buffalo.EDU
To: CATEGORIES@mta.ca
Subject: categories: Re: incompleteness of ZF
In-Reply-To: <199904031512.AA079642350@fb0448.mathematik.tu-darmstadt.de>
Message-ID:
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
Using an old logician's trick (see eg Feferman on paths thru O, or even
Goedel's original papers) as an
April Fool joke
may be amusing to some within the closed gates of a British University,
but is irresponsible on the world network. Think of the hundreds of
lurkers (who hesitate to speak up so that misconceptions can
be discussed and clarified openly, but) who are now furthering the rumor
that mathematics has somehow been proved inconsistent.The waves of such
disinformation can last for years or even decades.
*******************************************************************************
F. William Lawvere Mathematics Dept. SUNY
wlawvere@acsu.buffalo.edu 106 Diefendorf Hall
716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA
*******************************************************************************
From cat-dist Thu Apr 8 12:11:40 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id KAA15575
for categories-list; Thu, 8 Apr 1999 10:44:27 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Message-ID: <217F6DFA440ED111ACDA00A0C906B006109ABC@arsenic.rcp.co.uk>
From: Michael Abbott
To: "'wlawvere@ACSU.Buffalo.EDU'" ,
"'CATEGORIES@mta.ca'"
Subject: categories: RE: incompleteness of ZF
Date: Thu, 8 Apr 1999 08:49:35 +0100
MIME-Version: 1.0
X-Mailer: Internet Mail Service (5.5.1960.3)
Content-Type: text/plain
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
As a lurker who failed to either notice the date or understand any
detail of Paul's demonstration, I appreciate Lawvere's comments.
I do feel, though, that he is overstating the impact of Paul's little
jest. There were several immediate replies (to the effect, I think,
that F(lim X) is not lim F X), and no riposte from Paul. My own
reaction was: hmm, it'll be interesting if anything else comes out of
this.
I sympathise very much with Paul's "anti-ZF" stance; after all, hasn't
Lawvere set the basis for a non-set foundation of practical mathematics?
-----Original Message-----
From: cat-dist@mta.ca [mailto:cat-dist@mta.ca]On Behalf Of F W Lawvere
Sent: 06 April 1999 22:41
To: CATEGORIES@mta.ca
Subject: categories: Re: incompleteness of ZF
Using an old logician's trick (see eg Feferman on paths thru O, or even
Goedel's original papers) as an
April Fool joke
may be amusing to some within the closed gates of a British University,
but is irresponsible on the world network. Think of the hundreds of
lurkers (who hesitate to speak up so that misconceptions can
be discussed and clarified openly, but) who are now furthering the rumor
that mathematics has somehow been proved inconsistent.The waves of such
disinformation can last for years or even decades.
************************************************************************
*******
F. William Lawvere Mathematics Dept. SUNY
wlawvere@acsu.buffalo.edu 106 Diefendorf Hall
716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA
************************************************************************
*******
From cat-dist Thu Apr 8 12:20:29 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id KAA00730
for categories-list; Thu, 8 Apr 1999 10:50:53 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Date: Thu, 08 Apr 1999 10:08:52 -0300
From: Robert Dawson
Subject: categories: April 1st & related matters
To: CATEGORIES@mta.ca
Message-id: <019601be81c0$f31e3660$1c8eb88c@stmarys.ca>
Organization:
MIME-version: 1.0
X-Mailer: Microsoft Outlook Express 5.00.2314.1300
Content-type: text/plain; charset="iso-8859-1"
Content-transfer-encoding: 7bit
X-Priority: 3
X-MSMail-Priority: Normal
X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300
References:
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
[Note from Moderator: With the posts just sent, this discussion should
come to a close. Readers of the list, and those posting to it, should be
aware that it contains about 500 addresses.]
*Had* Paul posted his clever hoax on, say, sci.math (which, AFAIK, he
did not) where it would be widely available to J. Random Lurker, I would
share Bill Lawvere's concerns. Had he placed it permanently on his web
server, with a big flashing link from his home page, advertised it by
spamming 100,000 random netizens, and issued a trilingual press release, I
would share those concerns to a much greater extent. However, CATEGORIES is
a mailing list; probably everybody who received Paul's posting also received
the two debunkings, Bill's comment, and is reading this even as, er, they
read this. I don't imagine that we *have* hundreds of lurkers. (Lurkers!
Please identify yourselves... I'm curious.)
While Bill is undoubtedly correct that not all readers of CATEGORIES
share his ability to look at Paul's joke and instantly recognize not only
the fallacy but its antecedents [I offer myself as a proof of the
nonemptiness of the complement], surely we all have been around the block
enough times to distinguish between a full formal proof and what Paul
presented? Even had it been in earnest, such an announcement would justify
only the reaction "Somebody thinks he's shown ... but I don't think he has
circulated a complete proof yet."
I suppose that it is possible that somebody, browsing at random, *might*
find it in the CATEGORIES archives, in years to come, and not read ahead to
find out what the world had had to say about this discovery back in the mad,
exciting days of the late C20. But anybody who could do this and not
realize that there was something odd going on would probably either (a) not
understand why anybody should care if ZF is consistent or not, or (b) have a
vague feeling that Goedel, or Escher, or somebody, already proved that, or
something, didn't he?
-Robert Dawson
From cat-dist Thu Apr 8 12:26:00 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id KAA25533
for categories-list; Thu, 8 Apr 1999 10:43:27 -0300 (ADT)
X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs
Date: Wed, 7 Apr 1999 19:45:26 -0400 (EDT)
From: "R.A.G. Seely"
To: Categories List
Subject: categories: Re: incompleteness of ZF
In-Reply-To:
Message-ID:
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
On Tue, 6 Apr 1999, F W Lawvere wrote:
> Using an old logician's trick (see eg Feferman on paths thru O, or even
> Goedel's original papers) as an
> April Fool joke
> may be amusing to some within the closed gates of a British University,
> but is irresponsible on the world network. Think of the hundreds of
> lurkers (who hesitate to speak up so that misconceptions can
> be discussed and clarified openly, but) who are now furthering the rumor
> that mathematics has somehow been proved inconsistent.The waves of such
> disinformation can last for years or even decades.
Curiously, my reaction to this has been rather different. We were
discussing Paul's note after the seminar here the other day, and apart
from one reply, I rather had the idea that most replies were aware
that this was a joke, but that it was a subtle one (not all that
subtle, perhaps, but a lot more subtle that what often passes as
humour on the net, for sure). And that finding the error was a
respectable response.
As for spreading disinformation, there has been no shortage of people
who look serious, (I avoid the harder question as to whether they are,
and what exactly that ought to mean) and who have been spreading tales
of the inconsistency of maths for decades. As a graduate student, I
often attended logic meetings where Edward Wette proved ever more
basic fragments of our subject inconsistent (I recall he got as far as
propositional logic, Peano arithmetic, and several branches of
physics. I am not sure he made any serious distinction between the
last case and the others.) Perhaps one point here is that anyone who
believes all he reads is a fool, and anyone who believes all he reads
on the net is a fool who cannot even learn from experience. (It takes
about 5 minutes to uncover patently silly things on the net! - not
even counting this one...)
So - I agree Bill raises a serious matter, but I think in this case it
may be an overreaction. Paul's note was certainly "fishy" (French
reference for those not in a French environment), but it was
essentially harmless. This group is comparitively closed (even your
average academic journal is probably more open). And if anyone missed
the joke up to now, surely that has been remedied. (If only in that
refutations appeared quickly.)
However, if I see a report on this on "60 minutes" I will eat my
hat...
- all the best, Robert
= rags =
=================================
From cat-dist Sun Apr 11 17:49:58 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id QAA22515
for categories-list; Sun, 11 Apr 1999 16:45:08 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
X-Received: from callisto.acsu.buffalo.edu (qmailr@callisto.acsu.buffalo.edu [128.205.7.122])
by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id OAA11719
for ; Sun, 11 Apr 1999 14:51:47 -0300 (ADT)
X-Received: (qmail 4406 invoked by uid 39883); 11 Apr 1999 17:51:46 -0000
Date: Sun, 11 Apr 1999 13:51:46 -0400 (EDT)
From: F W Lawvere
Reply-To: wlawvere@ACSU.Buffalo.EDU
To: categories
Subject: categories: AMS Buffalo April 24/25, 1999
Message-ID:
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
LAST ANNOUNCEMENT
SMOOTH CATEGORIES IN GEOMETRY AND MECHANICS
Special session of AMS Meeting No. 943 in Buffalo, N.Y.
Diefendorf Hall, SUNY, Main Street Campus
April 24/25, 1999
note: changes in Sunday schedule
SCHEDULE:
Saturday, April 24, 1999
9:00 - 9:20 James FARAN:
A Synthetic Approach to Characteristic Cohomology
(Abstract # 943-18-72)
9:30 - 9:50 Hirokazu NISHIMURA:
Infinitesimal Calculus of Variations
(Abstract # 943-18-71)
10:00 - 10:20 Jonathon FUNK:
Lebesgue Toposes
(Abstract # 943-18-65)
10:30 - 10:50 George JANELIDZE: (joint work with Walter Tholen)
Strongly Separable Morphisms
(Abstract # 943-18-73)
***
2:30 - 2:50 Gonzalo REYES: (joint work with Anders Kock)
Atoms and Categories of Differential Equations in SDG
(Abstract # 943-18-109)
3:00 - 3:20 Felipe GAGO:
Transversal Stability
for Infinitesimally Represented Germs
(Abstract # 943-18-66)
3:30 - 3:50 Anders KOCK:
Infinitesimal Geometric Aspects of Riemannian
Metrics
(Abstract # 943-18-68)
***
4:30 - 4:50 Rene LAVENDHOMME:
Infinitesimal Deformations in SDG
(Abstract # 943-18-70)
5:00 - 5:20 Marta BUNGE:
Single Universe for Intensive and Extensive
Quantities in a Topos
(Abstract # 943-18-76)
Sunday, April 25, 1999
9:00 - 9:20 Peter FREYD:
Arithmetic Categories
(Abstract # 943-18-69)
9:30 - 9:50 Craig SNYDAL:
Vertex Algebras, an Example of a
Relaxed Multilinear Category
(Abstract # 943-18-67)
10:00 - 10:20 Walter NOLL:
Conceptual Mathematics, Categories,
Functors, and Tensors
(Abstract # 943-18-176)
10:30 - 10:50 Bill LAWVERE
Smoothness of Cubical Splines
(Abstract # 943-18-145)
*****
2:30 - 4:00 Round Table Discussion on the Theme
of the Special Session
ARRIVAL DATE: Friday, April 23, 1999
BUFFET DINNER: Saturday, April 24, 6:30 p.m. - 11 p.m. at the Center
for Tomorrow on UBs North Campus. Cost $ 10.--; cash bar. Transportation
available from Diefendorf Hall.
LUNCHES: available for both days at Diefendorf Hall.
ACCOMODATIONS:
For the participants of the meeting the downtown HYATT REGENCY BUFFALO
has special rates. For more information about hotels, etc. see
Http://www.acsu.buffalo.edu/~jjfaran/AMS_MEETING_home.html
A block of rooms under the name AMS SMOOTH CATEGORIES
has been reserved at the UNIVERSITY MANOR, 3612 Main Street,
(intersection Main/Bailey, at walking distance from Main Street Campus).
Prices are: Queen US$ 50.--/ King or 2 beds US$ 54.--, minus 10%
for participants, plus 13% tax. Tel. (716) 837-3344; Fax (716 )834-6246.
REGISTRATION:
Room 114, Diefendorf Hall, Saturday starting at 7:30 am. Fees are $
30.--/AMS or CMS members, $ 45.-- /nonmembers, $ 10.-- emeritus members,
students, unemployed mathematicians, (payable on-site only)
*******************************************************************************
F. William Lawvere Mathematics Dept. SUNY
wlawvere@acsu.buffalo.edu 106 Diefendorf Hall
716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA
*******************************************************************************
From cat-dist Mon Apr 12 07:51:07 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id GAA06994
for categories-list; Mon, 12 Apr 1999 06:30:47 -0300 (ADT)
X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs
Date: Thu, 8 Apr 1999 11:19:53 -0400 (EDT)
From: Michael Barr
X-Sender: barr@triples.math.mcgill.ca
To: Categories list
Subject: categories: email
Message-ID:
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
I have a new email address, as above. This new address will be given ONLY
to genuine correspondents. Although the addresses at math and triples
will remain valid, I will eventually route all mail that does not go to
the barrs address to my spam file to be looked at once or twice a week and
all spam deleted. This is because I have begun to receive a half dozen
spams a day.
-------------------------------------------------------------------
History shows that the human mind, fed by constant accessions of
knowledge, periodically grows too large for its theoretical coverings, and
bursts them asunder to appear in new habiliments, as the feeding and
growing grub, at intervals, casts its too narrow skin and assumes
another... Truly the imago state of Man seems to be terribly distant, but
every moult is a step gained.
- Charles Darwin, from "The Origin of Species"
From cat-dist Mon Apr 12 12:54:30 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id KAA30607
for categories-list; Mon, 12 Apr 1999 10:25:16 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Message-Id: <199904121311.JAA27400@christopher.INS.CWRU.Edu>
Date: Mon, 12 Apr 1999 09:11:10 -0400 (EDT)
From: cxm7@po.cwru.edu (Colin Mclarty)
To: categories@mta.ca
Subject: categories: small universes
Reply-To: cxm7@po.cwru.edu (Colin Mclarty)
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
Has anyone considered this idea for smaller Universes?
Maybe it is well known but I had not seen it.
We can drop the "replacement" condition on a
Grothendieck universe U: for every x in U and every onto
function h:x-->y with y a subset of U, y is also a member of
U. It is enough if a universe naturally models Zermelo set
theory. (Or even a bit less, as in the elementary theory of
the cagtegory of sets.)
So we could define a "universe" to be any set of the
form V(i) for i a limit ordinal (greater than omega). Here
V(i) is the set of all sets with rank less than i.
Then the claim "each set is member of some universe"
is simply a theorem of ZF. This is a great deal weaker than
Grothendieck's axiom as stated in SGA. Grothendieck's is
equivalent to extending ZF by a proper class of inaccessible
cardinals.
Each of these "universes" models Zermelo set theory
(i.e. ZF without the replacement axiom but with separation)
and a bit more. Insofar as general category theory is
provable in Zermelo set theory, it applies to the U-small
categories for each universe U in this sense.
I believe all the apparatus of Grothendieck's
TOHOKU paper, and the topos theory and cohomology of the
SGAs, is provable in Zermelo set theory with axiom of choice.
So this definition of universes formalizes current
cohomological number theory just as Grothendieck suggested,
within the axioms ZFC.
The only thing I want to check (as soon as I get
to my office) is Grothendieck's proof that every AB5 category
has enough injectives--it is an induction with a proper
class of steps but you prove it is fixed after some set of
steps. Possibly you need the axiom of replacement to show
it is indeed a set of steps. I cannot think of any other
result in this part of category theory that could require
replacement.
So, is this all old news? Or does anyone see a
problem here that I am missing?
From cat-dist Tue Apr 13 08:35:49 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id GAA04895
for categories-list; Tue, 13 Apr 1999 06:34:34 -0300 (ADT)
X-Authentication-Warning: mordred.eng.buffalo.edu: ji2 owned process doing -bs
Date: Mon, 12 Apr 1999 12:56:06 -0400 (EDT)
From: John R Isbell
To: categories@mta.ca
Subject: categories: Re: small universes
In-Reply-To: <199904121311.JAA27400@christopher.INS.CWRU.Edu>
Message-ID:
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
I certainly saw this in something more official than
handwriting -- print or preprint -- before I went to Italy
in 1973. For a guess, Sol Feferman proposed it.
John R. Isbell ji2@eng.buffalo.edu or just ji2@buffalo.edu
_____________________________
Home: http://www.unipissing.ca/topology/z/a/a/a/05.htm
__________________________________________________
| |
| Der Mensch ist nur da ganz Mensch, wo er spielt. |
| |
| -- Friedrich Schiller |
|__________________________________________________|
From cat-dist Mon Apr 19 14:12:24 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id LAA18230
for categories-list; Mon, 19 Apr 1999 11:30:38 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Message-Id: <2.2.32.19990419133109.007242d4@163.10.5.24>
X-Sender: gbaum@163.10.5.24
X-Mailer: Windows Eudora Pro Version 2.2 (32)
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Date: Mon, 19 Apr 1999 10:31:09 -0300
To: categories@mta.ca
From: Gabriel Baum
Subject: categories: WAIT99 - Call for Papers
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id KAA05260
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
Please find below the WAIT'99 Call for Papers. We apologize if you receive
this message more than once.
Call for Papers
28 JAIIO - WAIT'99
Argentinian Workshop on Theoretical Computer Science
Buenos Aires - Argentina
September 6-7, 1999
----------------------------------------------------------------------------
---------
The 3rd Argentinian Workshop on Theoretical Computer Science (WAIT'99)
will be part on the 28th Argentinean Conference on Informatics and
Operations Research (28 JAIIO), to be held in Buenos Aires from September
6th to September 10th, 1999.
The goal of the workshop is bringing together researchers from academy
(from Argentinean and other universities) and industry professionals in
order to discuss theoretical, empirical and experimental results on the
field of theoretical computer science.
This workshop will consist of invited talks and technical presentations.
Contributions are expected in all the areas of theoretical computer
science, including the following:
* Logical and algebraic foundations for computer science (logics for
computer science, category theory, relation algebras, type theory, etc.),
* Formal program construction (formal specification of sequential and
concurrent programs; analysis, verification and transformation of
programs, etc.),
* Algorithms and data structures (sequential, parallel, distributed,
on-line, probabilistic, etc.),
* Computational complexity,
* Automata theory,
* Graph theory,
* Symbolic and algebraic computation.
The expected contributions will describe original results as well as
undergoing research and development projects on theoretical computer
science coming from academy and industry.
Papers will be refereed by the International Program Committee, based
on the following:
* Papers reporting research / experimental results: these papers must
present previously unpublished results and will be judged based on their
originality, significance, relevance and clarity of presentation.
Authors must submit an extended abstract of up to 4 pages containing
enough information to allow the referees to determine the merits of their
work. It is also allowed to submit the full paper of up to 12 pages
including figures and references.
* Research projects: aiming to fostering the cooperation among national
and foreign researchers, short papers describing ongoing research will
be considered. Papers in this category may report already published
results. In that case, the authors must include the corresponding references.
* Industrial / Commercial applications: also relevant are papers describing
applications of theoretical results to real-life situations. Short papers
describing results that are both of significance for industry and that make
novel or defying applications of theoretical results are sought.
INVITED SPEAKERS
Thomas S. E. Maibaum (Imperial College, London, UK)
Bernhard Moeller (Universitaet Augsburg, Germany)
INSTRUCTIONS FOR AUTHORS:
In order to facilitate the widest dissemination of the papers, authors are
recommended the use of the English language. Nevertheless, papers in Spanish
or Portuguese are also welcome.
The deadline for submission of papers is May 3rd, 1999. Papers must be
submitted electronically in PostScript format (ghostview-readable) to the
e-mail address:
wait99@sol.info.unlp.edu.ar
Authors must send in a separate message in ASCII format the following: title
of the paper, name and affiliation of all the authors, their e-mail addresses,
phone and FAX numbers, an abstract of their contribution of at most ten lines,
a list of keywords that best describe the paper, and also the category within
which the paper is to be evaluated.
Alternative ways for paper submission are possible and must be discussed with
the workshop co-chairs.
The format for camera-ready papers will be announced with the letter of
acceptance.
IMPORTANT DATES:
Deadline for reception of papers....................May 3rd, 1999
Notification of acceptance..........................June 15th, 1999
Deadline for reception of camera-ready versions.....July 16th, 1999
WORKSHOP CO-CHAIRS:
Prof. Gabriel Baum
LIFIA Dto. de Informatica
Universidad Nacional de La Plata
Calle 50 y 115 1er piso.
(1900) La Plata - Argentina
Tel/Fax : +54-21-22-8252
e-mail: gbaum@sol.info.unlp.edu.ar
Prof. Marcelo Frias
Dpto. De Computacion -FCEyN-
Universidad de Buenos Aires
Pabellon I - Ciudad Universitaria
1428- Buenos Aires - ARGENTINA
Tel/Fax : +54-1-783-0729
e-mail: mfrias@sol.info.unlp.edu.ar
PROGRAM COMMITTEE:
Gabriel Baum (Universidad Nacional de La Plata, Argentina)
Javier Blanco (Universidad Nacional de Cordoba, Argentina)
Luis Fariņas del Cerro (Universite Paul Sabatier, France)
Esteban Feuerstein (Universidad Nacional de Buenos Aires and Universidad
Nacional de General Sarmiento, Argentina)
Marcelo Frias (Universidad Nacional de Buenos Aires, Argentina)
Armando Haeberer (Pontificia Universidade Catolica de Rio de Janeiro, Brazil)
Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro,
Brazil)
Joos Heintz (Universidad Nacional de Buenos Aires, Argentina)
Roger Maddux (Iowa State University, USA)
Tom Maibaum (Imperial College, UK)
Bernhard Moeller (Universitaet Augsburg, Germany)
Gonzalo Navarro (Universidad de Chile, Chile)
Alfredo Olivero (Universidad Nacional de Buenos Aires and Universidad
Nacional de General Sarmiento, Argentina)
Ruy de Queiroz (Universidade Federal de Pernambuco, Brazil)
Alvaro Tasistro (Universidad de la Republica, Uruguay)
Sergio Yovine (CNRS-VERIMAG, France)
For more information send e-mail to: jaiio@sadio.edu.ar, write to:
SADIO / WAIT'99
Uruguay 252 2D
1015 - Buenos Aires
ARGENTINA
TEL: +54-1-3715755/4763950
FAX: +54-1-3723950
or see http://www.uba.ar/wwws/sadio
___________________________________________
Gabriel Baum
LIFIA
Facultad de Ciencias Exactas
Universidad Nacional de La Plata
Calle 50 y 115 - 1er piso
(1900) La Plata
e-mail: gbaum@sol.info.unlp.edu.ar
Tel/Fax: +54 21 228252
___________________________________________
From cat-dist Thu Apr 22 12:49:58 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id KAA13507
for categories-list; Thu, 22 Apr 1999 10:34:00 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
X-Received: from bommel.math.uu.nl (bommel.math.uu.nl [131.211.22.23])
by mailserv.mta.ca (8.9.3/8.9.3) with ESMTP id KAA00265
for ; Wed, 21 Apr 1999 10:27:20 -0300 (ADT)
X-Received: from verkwil.math.uu.nl (verkwil [131.211.23.35])
by bommel.math.uu.nl (VMailer) with ESMTP
id CF6CC144CB; Wed, 21 Apr 1999 15:28:08 +0200 (MET DST)
X-Received: (from moerdijk@localhost) by verkwil.math.uu.nl id PAA06991
(8.8.8/IDA-1.6 for RROSEBRUGH@mta.ca); Wed, 21 Apr 1999 15:28:08 +0200 (MET DST)
Date: Wed, 21 Apr 1999 15:28:08 +0200 (MET DST)
From: "I. Moerdijk"
Message-ID: <199904211328.PAA06991@verkwil.math.uu.nl>
To: categories@mta.ca
Subject: categories: Workshop: "OPERADS AND APPLICATIONS",
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
ANNOUNCEMENT:
On June 10-12 (Thurday-Saturday), 1999, an informal workshop will take
place at University of Utrecht, The Netherlands, under the title
"OPERADS AND APPLICATIONS",
organized by F. Clauwens (Nijmegen), E. Looijenga and I. Moerdijk
(Utrecht).
Invited lectures will be given by:
A. Joyal
M. Kapranov
I. Kriz
J.-L.Loday
M. Markl
J. Morava
T.Pirashvili
S. Shnider
J. Stasheff
A.Voronov
Further information is available via the home page of our institute (http//www.math.uu.nl/operads/).
There is no registration fee. Unfortunately, we will not be able to
provide funding for participants other than the speakers listed above.
If you wish to attend, please register with Corrie van Os
(os@math.uu.nl). If you do so before April 26, she will be able to book
a hotel room for you.
Ieke Moerdijk.
From cat-dist Thu May 6 23:23:23 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id WAA07146
for categories-list; Thu, 6 May 1999 22:32:26 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
Date: Fri, 23 Apr 1999 16:44:13 +0100 (BST)
Message-Id: <24946.199904231544@craro.dcs.ed.ac.uk>
To: categories@mta.ca
Subject: categories: CTCS '99: Extension of deadline till 7 May 1999.
From: "Martin Hofmann"
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
[ apologies from the moderator for the posting delay which makes this
almost moot... ]
CATEGORY THEORY IN COMPUTER SCIENCE 1999 10-12 September 1999
EDINBURGH, SCOTLAND
**********************************************************
**** Submission deadline extended till 7 May 1999 ********
**********************************************************
Dear colleague,
Following a number of requests we have decided to postpone the
submission deadline for CTCS '99 by two weeks until 7th May
1999. Notification of authors of accepted papers will take place on
18th June 1999.
The proceedings will appear at the conference as Electronic Note in
Theoretical Computer Science ENTCS (http://www.elsevier.com/locate/entcs).
ENTCS have encouraged us to guest-edit a special issue of Theoretical
Computer Science (TCS) consisting of journal versions of selected
papers after the conference.
The full call for papers can be found under
http://www.dcs.ed.ac.uk/home/ctcs99
Martin Hofmann
Laboratory for Foundations of Computer Science
JCM, Rm 1606
The King's Buildings
Mayfield Rd
Edinburgh EH9 3JZ
UK
Phone: +44 131 650 5187
Fax: +44 131 667 7209
E-mail: mxh@dcs.ed.ac.uk
WWW: www.dcs.ed.ac.uk/home/mxh
From cat-dist Thu May 6 23:23:49 1999
Received: (from Majordom@localhost)
by mailserv.mta.ca (8.9.3/8.9.3) id WAA02465
for categories-list; Thu, 6 May 1999 22:28:59 -0300 (ADT)
X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Message-ID: <14112.24346.837327.881377@rsund.crn.cogs.susx.ac.uk>
Date: Fri, 23 Apr 1999 12:52:58 +0100 (BST)
From: Matthew Hennessy
To: categories@mta.ca
Subject: categories: Research Positions
X-Mailer: VM 6.68 under 20.4 "Emerald" XEmacs Lucid
Sender: cat-dist@mta.ca
Precedence: bulk
Status: O
X-Status:
____________________________________________________
My apologies if you receive this more than once!
____________________________________________________
UNIVERSITY OF SUSSEX
RESEARCH FELLOWS IN THE FOUNDATIONS OF COMPUTING
Two Research Fellows are required for a 2-year project entitled ``The
Semantic Foundations of Mobile Computation'', under the direction of
Prof. M. Hennessy and funded by the EPSRC.
The project objectives include
- the development of abstract foundational calculi for mobile
systems in which the concepts of location, mobility, failure
and security play an central role
- the elaboration of behavioural equivalences for these calculi,
and their associated algebraic theories
- the construction of proof systems and methodologies for
establishing properties of mobile systems.
The project will start on 1/10/99 and salary will be related to the
academic 1A scale. A Ph.D. in Computer Science or Mathematics or
equivalent experience is required. In addition to normal research
duties the successful candidate will be expected to provide some
assistance to undergraduate teaching.
To apply please submit applications to
Matthew Hennessy
School of COGS
University of Sussex
Falmer
Brighton BN1 9QH
UK
Tel: +44 01273 678101
email: matthewh@cogs.sussex.ac.uk
from whom more details of the project and the conditions of service
are available.
Applications should include
- a detailed curriculum vitae,
- names of three referees with their email addresses,
- a statement outlining the candidates proposed contribution
to the goals of the project,
- copies (or URL references) of any relevant publications.