[Prev][Next][Index][Thread]
Re: chains, etc & announcement on intuitionistic Tarski theorem
Date: Sun, 1 Dec 91 15:20:06 EST
To: pt@doc.imperial.ac.uk
On the question of "what notion of ordinal is suitable for a fully
intuitionistic transfinite induction"
I think it should be pointed out that the weakest known definition that
works (and permits the proof of tarski's theorem)
is the so-called "Powell Ordinal"
Def: An Ordinal is a transitive set of transitive sets.
This, and the corresponding transfinite induction theorem, as well as
other useful lemmas about constructive sets is covered succinctly
and clearly in Grayson's
"Heyting Valued Models for Intuitionistic Set Theory"
in the Durham Sheaf-Theory Symposium proceedings
Lecture Notes in Mathematics 753 (Springer)
as well as in C.D. McCarty's thesis (under D. Scott at Oxford) on
Constructive Set theory which is available as a CMU tech report (ca.
1985).
This is a strong enough notion to formalize the model theory for
IZF (Intuitionistic Zermelo Fraenkel Set Theory) with the axiom of
collection (instead of replacement). One can construct a ranked
universe
V = union {Va: a an ORD}
such that every set lies in V, like the Von Neumann ranked hierarchy.
The induction scheme that replaces the traditional axiom of foundation
is:
(x)[(y)(y in x & p(y) --> p(x))] --> (x)(p(x))
--J. Lipton