# Lower bound on size of proof that a list of integers is sorted

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.)

-
What is your proof language? If it admits proofs such as forall i, i + 1 < length(array) -> nth i array < nth (i+1) array, then the length of the proof might be $O(1)$. –  Gilles Dec 14 '12 at 21:40
@Gilles, that's a good point. For the sake of the question, instead of fixing a particular proof language, may I stipulate that the proof be checkable in time polynomial in the size of the proof? That would exclude the forall approach. –  Chris Pressey Dec 14 '12 at 22:39
This answer on cstheory.SE looks closely related; it looks like it requires the use of the comparison model in the proof in essentially the same way as the $\Omega(n \log n)$ bound on sorting requires the comparison model in the algorithm. –  Chris Pressey Dec 16 '12 at 15:54

When talking about proofs, you need to explain three things: (1) formal proof system, (2) what you want to prove, (3) what you want to prove it from.

You seem to imply that item 3 should be $n$ different axioms, listing the contents of the array. In that case, you're right that you will need to invoke all axioms to prove that the list is sorted, in any consistent formal system.

Another reason why the proof will need to be of linear length is that item 2, what you want to prove, might be stated as $A[1] \leq A[2] \land A[2] \leq A[3] \land \cdots \land A[n-1] \leq A[n]$.

However, perhaps it is the case that item 3 is a description of the algorithm, and item 2 is something similar to Gilles's formulation, $\forall i \in [n-1], A[i] \leq A[i+1]$. In that case, if the proof system is strong enough (say ZFC), then you should be able to prove item 2 in $O(\log n)$ by starting with a general correctness proof for your algorithm, and then invoking it for your particular $n$. If your proof system is too weak to prove something like that, you might still be able to prove that the array is sorted in $O(\log^{O(1)})$; the relevant subject is known as bounded arithmetic.

-
This answer is helpful (I'll upvote it as soon as I get enough reputation to allow me to do that.) Clearly I am going to have to think about the larger context and possibly ask a better question, since I don't presently have a fixed proof language in mind. –  Chris Pressey Dec 14 '12 at 22:56
I'm still fairly confused on (at least) one point: When you say "the algorithm" in the last paragraph, what algorithm are you referring to? –  Chris Pressey Dec 15 '12 at 23:43
Perhaps you want to prove a statement like "A is a list that has undergone Quicksort, and A is now sorted". In this case, you don't have to exhibit the elements of A, you only have to prove the correctness of Quicksort. –  Yuval Filmus Dec 17 '12 at 8:23

An alternative way to look at the problem is to ask what is the complexity of checking if a given list of numbers is sorted. Then by an adversary argument it can be shown that you have to access all of the numbers and therefore the time complexity (also query complexity) of the algorithm needs to be $\Omega(n)$.

This is related to Yuval's answer. You can consider an algorithm as a proof system for the problem: a proof will be an execution of the algorithm on the input resulting in the desired output.

-