[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

If you allow combining the two equations into one, there is also the option

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

On Thu, Oct 16, 2014 at 3:57 AM, Mario Carneiro <di.gama at gmail.com> wrote:

>
>
> On Thu, Oct 16, 2014 at 3:43 AM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
>
>> On Thu, Oct 16, 2014 at 8:36 AM, Mario Carneiro <di.gama at gmail.com>
>> wrote:
>>
>>> 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.
>>>
>>
>> What if we relax that assumption?
>>
>
> A really clever way of writing it would be (abs o. rep) = id , where o. is
> composition, but I don't think there is a way to write that using
> primitives any simpler than \a. (abs (rep a)) = \a. a. You already know
> that it needs a dummy variable (because things like (abs rep) are not
> well-typed, and you have no other objects using type A), needs to have abs
> and rep, and needs to be quantified over the dummy variable (once on each
> side of the equality so the types match), which gives \a. (abs (rep a)) =
> \a. ? where the a on the left may possibly be somewhere else. There really
> aren't too many options that are even shorter than \a. (abs (rep a)) =
> \a. a, so I would say that it's probably as good as it gets. For the other
> one, there are no spare symbols in P = \r. ((rep (abs r)) = r, so again I
> think that's minimal. A rigorous proof would need an enumeration of all
> smaller formulas, but it's hard to see anything well-typed that is any
> smaller than this and still uses all the essential elements.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/ad029e5d/attachment-0001.html>