Message-Id: <9106270844.AA02964@erbert.win.icl.co.uk>
From: Rob Arthan <rda@uk.co.icl.win>
Date: Thu, 27 Jun 91 08:44:55 GMT
To: info-hol@edu.uidaho.cs.ted
Subject: select

Concerning Sandy Murphy's meta-theoretical conjecture:

>       So presumably, if one had a proof of a
>       term involving (@x.Px), the same proof should work for a term which
>       substituted (f P) for (@x.Px).  But this is a meta-theorem, something
>       like
>       (|- t[...,(@x.Px),...])  ==> (|-(!f (!Q.Q (f Q)) ==> t[...,(f P),...]))
>       I don't think the un-meta version of this (take out the turnstiles) can
>       be proven in HOL.  (From what I understand about Isabelle, the meta
>       version could be proven there.)

This meta-result is not valid. E.g. consider P (x:*) = T \/ F. Then we can prove
in HOL that (@x.P x)  = (@x.T) (since (@x.P x) = (@x. T \/ F) = (@x.T)).
So

        |- (@x.P x) = (@x.T)

I.e. I am taking t[f] = (f = @x.T). But we cannot have:

        |- (!f.!Q.Q(f Q)) ==> |- f P = (@x.T)

since that says that there is only one choice function for the identically true
predicate (\x:*.T), whereas clearly there are as many such choice functions as
there are elements of *.

Semantically, the fact that you can't prove such a meta-result indicates
that @ must be interpreted by a predetermined fixed choice of representative
for every non-empty subset of every type in the universe. Thus the comment:

>       On the other hand, the only property of x that one knows and can use in
>       a proof is that x satisfies P.

(where x = @x.P) is not really true. One `knows' much more about x, namely that
it is the predetermined representative for P.

Rob Arthan.