formalizing those examples
beeson@cats.ucsc.edu
Mon, 13 Jun 1994 07:44:34 -0700
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.