Jan Brosius wrote:
> look at this example:
>
> alpha(x) == x is_an Integer => x^2 > -1
>
> this is an example of a formula that is true
>
> *If you want to come up with your own logic, where alpha(x)
> is equivalent to
> *forall x. alpha(x), then that's fine.
>
> No, if alpha(x) is a true formula then forall x. alpha(x) is
> again a true assertion
I think part of the confusion here has to do with the notation alpha(x).
The traditional mathematical notation f(x) is ambiguous. It may either
refer to an abstraction or an application. In this regard, lambda notation
is much superior. What does the alpha(x) here mean?
If we assume it is a function like:
alpha = \ x . (x is_an Integer => x^2 > -1 )
then it is meaningful to debate whether or not the inner 'x's refer to the
same x as the lambda bound x or whether "x is_an integer" creates a new
binding.
On the other hand, if we assume that alpha(x) is an application of alpha
to x then the debate seems to be whether x refers to some value, or whether
it is simply a place-holder.
Perhaps Jan can clarify what is meant here.
--Peter Douglass
