Despite the absence from Gentzen’s conception of logic of the customary distinction between syntax and semantics, we show how reasoning about cut-free proofs leads naturally to ordinary completeness theorems. In reviewing this well-documented strategy we emphasize an overlooked detail: The “semantics” with respect to which a logical calculus is shown to be “complete” need not be specified in advance of the coordination procedure. Beginning with Ketonen’s inversion theorem (and appropriate modifications of it in the case of LI and other nonclassical systems), one can specify a procedure for proof search from which the type of refutation structure for unprovable sentences can be reverse-engineered. The same approach applies in the case of quantification theories by considering the features of infinite constructions. As different as truth-functions, Kripke frames, and the set-theoretic semantics for classical quantification theory are, the route to proof search via invertibility reveals similarities in the concept of logical completeness associated with each. Details of Gentzen’s, Ketonen’s, and Maehara’s formulations of sequent calculi that appear first like nothing more than design preferences are shown to have deep consequences for the procedures described.