Negotiation is a key technique for dynamically organizing activity in multi-agent systems, yet the negotiation process itself can often be difficult to reason about. In this paper, we introduce a framework in which negotiation can be characterized as a form of distributed, multi-agent theorem proving. Thus, in this preliminary analysis, we show that certain simple forms of negotiation will be successful if, and only if, a corresponding theorem can be proved by agents acting as theorem-proving components. We extend this approach further to represent situations where the agent has a choice of possible responses, given a proposal received. In such cases, an ordering strategy is used to select the order in which replies are provided; this corresponds to a common use of ordering within classical theorem proving.