[FOM] Predicativity

[Steve Newberry]

Dear Professor Tait,

I have a question about Predicativity [NOTHING to do w. L.W.]: Usually the 
predicative
criterion is linked to the Ramified Theory of Types, and in particular to a 
restriction
of the Comprehension Axiom something along the following lines:

C.A. is  (EP)(Ax/1, ... x/k)[ P(x/1, ... x/k) <=> R(x/1, ... x/k)] where P 
does not appear
in R and the type-order of R is


                  {  max(Ords of  unbound entities appearing in R)
Ord(R) is = max  {   (or)
{  1 + max(Ords of the bound variables appearing in  R )

and Ord(P) = Ord(R).

It has occurred to me that we might substantially *weaken* the restriction 
to the following:


                  {  max(Ords of  unbound entities appearing in R)
Ord(R) is = max  {   (or)
{  1 + max(Ords of the universally bound variables
{  appearing in  R  s.t. at least one  such variable
{  appears in a negated literal)

and Ord(P) = Ord(R).

without compromising the predicativity [at least in Poincare's sense.]

My reasoning is as follows:  No UNIVERSAL quantifier, no circularity; No 
NEGATED literal,
no viciousness. No vicious-circle, no need to increment the type-order. If 
my reasoning is sound, then the difficulty in obtaining GLB and LUB should 
go away, as there is NO *need*
for the vicious circle in these constructs.

Admittedly, this is a rather *terse* characterization.  I have no objection 
to expanding on
the idea, but for at least sixty years people have been telling me that I 
consistently
tend to over-explain, and so I'm *trying* to be brief.

Does any of this make sense to you?

Respectfully,

Steve Newberry