Placeholder Calculus for First-Order Logic

Abstract. In this paper we present an extension of first-order predi-cate logic with placeholders. These placeholders allow the construction of proofs for incomplete theorems. These theorems can be completed during the proof construction process. By using special definitions of substitutions and replacements, we obtain an unexpectedly simple cal-culus. Furthermore, we avoid the need of additional rules for explicit substitutions to deal with postponed substitutions in placeholders, since the definitions of substitution and replacement deal with them directly.