[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

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/a6ebf9c9/attachment.html>