## Existence assumptions in Agda

After discussing the proof that “among all positive integers, the integer 1 is the largest” at length with some colleagues, I decided to formalize the proof in Agda. Well, of course the theorem is false, so I formalized the result actually concluded by the given proof—if there is some largest positive integer, then it is \(1\). (This is the hidden “existence assumption” the quote alludes to.)

If you’d like to follow along, here’s my expanded explanation of the original proof:

Any positive integer \(n\) can be squared, and squaring has the property that \(n^2 \geq n\). In fact, it is easy to see that \(1\) is the

unique\(n\) for which \(n^2 = n\); in all other cases, \(n^2 > n\). Let us assume for a moment that thereisa largest positive integer \(N\). Well, it certainly cannot be a number besides \(1\), because if so, \(N^2\) is larger than \(N\), a contradiction. Therefore, the only possibility is that \(N=1\).However, there is another possibility—that there simply is no largest positive integer. The fact that squaring can embiggen all numbers besides \(1\) is irrelevant, because there is in fact also a way to obtain a number larger than \(1\). (If there were some largest positive integer, then the previous facts about squaring would imply that no other technique could obtain a number larger than \(1\).)

And here’s my standalone Agda formalization. (It checks for me in Agda 2.3.2, without the standard library.) The interesting definitions are the last four, in particular, the key lemma that squaring embiggens numbers besides \(1\), and the theorem statement itself (`one-is-maximal`

).

Thanks for posting this code, good sir.

May 21st, 2013 at 9:28 am