[FOM] Predicativity

[William Tait]

On Wednesday, April 23, 2003, at 04:24  AM, Steve Newberry wrote:

> 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.]

I don't understand the grammar of your proposed weakening of the 
ramification condition for predicativity---in particular

> 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)

I don't understand the grammar of your proposed weakening of the 
ramification condition for predicativity---in particular

> 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)

But in any case,  this

> 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.

I doubt. On Poincare's conception---on Kreisel's and Feferman's 
reading, at least---the definition of a  set should be absolute (i.e. 
independent of the precise extension of the universe of sets beyond a 
certain minimum which has already been constructed), not just downward 
absolute---i.e. its complement should also be downward absolute.  Eg. a 
  Pi^1_1 set of numbers is downward absolute, but not in general its 
complement (which contains existential quantifiers).

In terms of the vicious circle principle, if there are vicious circles 
in connection with  statements of the form  forall X phi(n, X), then 
there are vicious circles in connection with statements of the form not 
exists X phi(n, X).

Feferman discusses Poincare's conception of predicativity in a paper in 
JSL from the early 1960's.


Best,  Bill Tait

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/enriched
Size: 3015 bytes
Desc: not available
Url : /pipermail/fom/attachments/20030423/6bda9abc/attachment.bin