patternMinor
Lower bound on size of proof that a list of integers is sorted
Viewed 0 times
boundlowersizethatsortedlistintegersproof
Problem
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.)
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.)
Solution
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.
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.
Context
StackExchange Computer Science Q#7396, answer score: 4
Revisions (0)
No revisions yet.