Re: defn of impredicativity (was Re: goals and language?)

[Calvin Ostrum <***>]

On 8/10/05, glen e. p. ropella <***> wrote:

> The reason I sustained a conversation with Torkel even after he provided
> his personal definition of "impredicativity" was because he seems to
> think that type of circularity is completely different from the other
> types of circularity talked about in Kercel, Kline, B&M, etc.  And I
> don't understand that difference.

I don't think it is accurate to describe the definition
Torkel provided as "his personal definition".   I believe it
is simply the standard definition that is used in formal logic.

And the difference is quite clear.  They are not even applied to
the same thing (as explained before).  It is definitions that are
impredicative, but sets that are not well-founded, such as the
set a containing only a, for example.   Impredicative definitions
will never specify sets such as this as long as there is something
that entails the axiom of foundation among the axiom set.

> This is important to
> me because, as a modeler, models can be maps between things (as tight as
> real functions -- M:Input -> Output -- or as loose as simile) and things
> that can be mapped by other models.  In particular, when dealing with
> multi-level or multi-scale models.

I don't see what this means.  You would have to put it in more precise
terms.  But let us consider the following as an example.   You are 
familiar with the lambda calculus?   In its various forms, the lambda
calculus is a set of terms that denote either functions (\x.A) or applications
of functions (AB), where the general interpretation is that ((\x.A)B) is the
value of the expression A  evaluated with free variable x equal to the value 
of B.

The basic lambda calculus is untyped.  So we have the issue that in a 
model for the lambda calculus, functions can be applied to themselves.
In fact, the only thing you can apply a function to is a function of the
very same type.   This results in a "circular" sort of "domain equation"

    D == [D -> D]

A great deal of research has been done in solving such domain equations to
specify the set of objects D.   Non-well-founded set theories are not necessary,
although I think they can indeed be very helpful.   But there is nothing
"non-computable" or otherwise mysterious about these objects (in fact,
the lambda calculus was invented by Alonzo Church as one way of 
specifying the class of computable functions, and here they are, functions
that are intrinsically "circular" in some way or other.  Perhaps this could be
a suggestive metaphor, or even more)