How Exhaustive Does an Extension-Based Proof Need to Be?

The class of extension-based proofs encompasses traditional valency arguments. It has been shown that they are insufficient to establish the impossibility of (n-1)-set agreement among n ≥ 3 processes in an asynchronous system with crash failures. We generalize this definition to k-exhaustive extension-based proofs, in which a prover can learn the maximum length of all executions involving a set of at most k processes from a specified configuration (which may be infinite). An upper bound on the length of these executions enables the prover to determine the outputs of all these executions. When k = n, this enables the prover to perform an exhaustive search of all reachable configurations, so it knows everything about the protocol. On the other hand, extension based proofs are as powerful as 1-exhaustive extension-based proofs. For any task with no deterministic, wait-free solution among n ≥ 2 processes, we show that there is an (n-1)-exhaustive extension-based proof of its impossibility. This is done using a new characterization of such tasks. In contrast, we prove that for 1 ≤ k ≤ n-2, there is no k-exhaustive extension-based proof of the impossibility of (n-1)-set agreement.