<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Mario,<div><br><div><div>On 16 Oct 2014, at 02:30, Mario Carneiro <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><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 class=""></span></div><div style="word-wrap:break-word"><span class=""><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 class=""><br>(\a:A. (abs (rep a)) = a) = (\a. \p:bool. p = \p. p )</span><br><span class="">(\r:B. (P r) = ((rep (abs r)) = r)) = (\r.</span><span class=""><span class=""> \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>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.</div><div><br></div></div></body></html>