[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

 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.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141015/0aa4dd27/attachment.html>