From lusk Mon Jun 13 09:46:12 1994
Received: from cats.ucsc.edu (cats-po-1.UCSC.EDU [128.114.129.22]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA03083 for <qed@mcs.anl.gov>; Mon, 13 Jun 1994 09:44:52 -0500
From: beeson@cats.ucsc.edu
Received: from si.UCSC.EDU by cats.ucsc.edu with SMTP
	id HAA29496; Mon, 13 Jun 1994 07:44:48 -0700
Received: by si.UCSC.EDU (8.6.9/4.7) id HAA17556; Mon, 13 Jun 1994 07:44:34 -0700
Date: Mon, 13 Jun 1994 07:44:34 -0700
Message-Id: <199406131444.HAA17556@si.UCSC.EDU>
To: John.Harrison@cl.cam.ac.uk, qed@mcs.anl.gov
Subject: formalizing those examples

Those examples, involving direct limit constructions, are 
easy to formalize in Feferman's theories, which have primitive
function application AND nice set-theoretic apparatus.
The Join axiom, in particular, permits the formation of 
{ <n,a> :  a in X[n] } whenever you have a sequence of classes X[n]
as in those examples.