[opentheory-users] Troubleshooting an article reader

[Ramana Kumar]

I think that is  weaker than the 2 original axioms. We need to know abs is
a left-inverse of rep regardless of P.

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

> ...which can also be written
>
> P = \r. (\a. ((rep a) = r) = (= (abs r)))
>
> (although using curried = that way is a bit strange)
>
> On Thu, Oct 16, 2014 at 4:04 AM, Mario Carneiro <di.gama at gmail.com> wrote:
>
>> 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.
>>>
>>
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/d74a7492/attachment.html>