Suppose we have a list of unbounded integers, written in binary, and we want to write a (formal) proof that the list is sorted in ascending order.
Such a proof might look (informally) like: "2 < 3, and 3 < 5, and ... and 71 < 79, so the list is sorted."
It would seem such a proof must have length $\Omega(n)$ where $n$ is the length of the list of integers, as you could use the same kind of argument that is used to show that comparison sorting is $\Omega(n \log n)$; roughly, if the proof was any shorter than $n$, it would have missed one of the integers on the list.
Is this the case, or have I missed something? Is there a clever way to construct an asymptotically shorter proof?
Edit: As Gilles and Yuval Filmas point out below, a specific answer can only be given if we have some constraints on the language in which the formal proof is written. For the purposes of this question, suppose that no matter what particular proof language is used, the proof must be written such that it can be verified in time at most polynomial in the length of the proof. This excludes proofs of the form "for all elements of the list, ..." (I realize this constraint may make the question more difficult than if a particular proof language was chosen, but it really is closest to what I was thinking when I asked the question.)
forall i, i + 1 < length(array) -> nth i array < nth (i+1) array
, then the length of the proof might be $O(1)$. $\endgroup$forall
approach. $\endgroup$