<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 16, 2014 at 3:18 AM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word">Mario,<div><div><div class="h5"><br><div><div>On 16 Oct 2014, at 02:30, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> wrote:</div><br><blockquote type="cite"><div dir="ltr"> Rob,<div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><span></span></div><div style="word-wrap:break-word"><span><blockquote type="cite"><div dir="ltr">Well, there's no need to use the definition of ! : you could just write<br><div><div class="gmail_extra"><div class="gmail_quote"><div><br></div><div>(\a. (abs (rep a)) = a) = (\a. a = a)<br>(\r. (P r) = ((rep (abs r)) = r)) = (\r. r = r)<br></div><div><br></div><div>and since now the variables are bound, you are free to use whatever dummies you like.<br></div></div></div></div></div></blockquote><div><br></div></span>But that’s just expanding the definition of the connectives and it’s not very pretty.<div><div>(Strictly speaking, I don’t know whether it is expanding the definition of the</div><div>connectives or not, since you haven’t told me what the type of the second</div><div>variable called r is, and for technical reasons it is boolean in the definition</div><div>of T.)</div></div></div></blockquote><div><br></div><div>Actually, it's not just expanding the definition of the connectives, which would give<br><span><br>(\a:A. (abs (rep a)) = a) = (\a. \p:bool. p = \p. p )</span><br><span>(\r:B. (P r) = ((rep (abs r)) = r)) = (\r.</span><span><span> \p:bool. p = \p. p</span>)<br><br></span></div><div>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.<br></div></div></div></div></blockquote></div><br></div></div><div>Can you prove that?  E.g., if the measure of simplicity is the number of symbols?</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.<br></div></div></div></blockquote><div><br></div><div>Actually, that was a lie, because I just thought of an even simpler way to quantify the statement "<span>(abs (rep a)) = a", and that's<br><br></span><span>\a. (abs (rep a)) = \a. a</span><br><br></div><div>and similarly for the other:<br><br><span>P = \r. ((rep (abs r)) = r</span><br><br></div><div>Assuming that <span> (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.<br></span></div><div><br></div><div>Mario<br></div><div><span></span></div></div></div></div>