[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

On Thu, Oct 16, 2014 at 3:18 AM, Rob Arthan <rda at lemma-one.com> wrote:

> 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.
>

Actually, that was a lie, because I just thought of an even simpler way to
quantify the statement "(abs (rep a)) = a", and that's

\a. (abs (rep a)) = \a. a

and similarly for the other:

P = \r. ((rep (abs r)) = r

Assuming that (abs (rep a)) = a is the shortest way to express the original
claim, I am confident that this is the symbol-minimal quantified version of
the same formula.

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