Why Extension-Based Proofs Fail

We prove that a class of fundamental shared memory tasks are not amenable to certain standard proof techniques in the field. We formally define a class of extension-based proofs, which contains impossibility arguments like the valency proof by Fisher, Lynch and Paterson of the impossibility of wait-free consensus in an asynchronous system. We introduce a framework which models such proofs as an interaction between a prover and an adversarial protocol. Our main contribution is showing that extension-based proofs are inherently limited in power: for instance, they cannot establish the impossibility of solving (n-1)-set agreement among n > 2 processes in a wait-free manner. This impossibility result does have proofs based on combinatorial topology. However, it was unknown whether proofs based on simpler techniques were possible.