[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Mario,

On 16 Oct 2014, at 02:30, Mario Carneiro <di.gama at gmail.com> wrote:

>  Rob,
>> Well, there's no need to use the definition of ! : you could just write
>> 
>> (\a. (abs (rep a)) = a) = (\a. a = a)
>> (\r. (P r) = ((rep (abs r)) = r)) = (\r. r = r)
>> 
>> and since now the variables are bound, you are free to use whatever dummies you like.
> 
> But that’s just expanding the definition of the connectives and it’s not very pretty.
> (Strictly speaking, I don’t know whether it is expanding the definition of the
> connectives or not, since you haven’t told me what the type of the second
> variable called r is, and for technical reasons it is boolean in the definition
> of T.)
> 
> Actually, it's not just expanding the definition of the connectives, which would give
> 
> (\a:A. (abs (rep a)) = a) = (\a. \p:bool. p = \p. p )
> (\r:B. (P r) = ((rep (abs r)) = r)) = (\r. \p:bool. p = \p. p)
> 
> The variables a and r there have the same type in each abstraction, because the type of the abstraction in the first case is (A->bool) and carries the type over to the other abstraction. I realize that it's not that elegant, but if you want to eliminate free variables and still have the same result, that's the simplest way to do it.

Can you prove that?  E.g., if the measure of simplicity is the number of symbols?

Regards,

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/4540b866/attachment-0001.html>