Complete linear proofs of systems of linear inequalities

摘要

Rabin has investigated the difficulty of proving that a set of linear forms is simultaneously positive by the evaluation of analytic functions. In this paper we study this same question under the restriction that each analytic function itself be linear. A complete result is given in the case that the original set of linear forms are simultaneously positive on a subspace having at least one extreme point. Applications are then given. In particular, it is shown that the proof that a real number x1 is maximal out on the set {x1,…,xm} requires evaluation of m−1 linear forms even if x1 is known in advance to be exceeded by at most one xi for 2≤i≤m.