A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which represents (...) proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions. (shrink)

When working with a first-order theory, it is often convenient to use definitions. That is, if ϕ(x) is a first-order formula with the free variables shown, one can introduce a new relation symbol R to abbreviate ϕ, with defining axiom ∀x (R(x) ↔ ϕ(x)). Of course, this definition can later be eliminated from a proof, simply by replacing every instance of R by ϕ. But suppose the proof involves nested definitions, with a sequence of relation symbols R0, . . . (...) , Rk abbreviating formulae ϕ0, . . . , ϕk, where each ϕi may have multiple occurrences of R0, . . . , Ri−1. In that case, the naive elimination procedure described above can yield an exponential increase in the length of the proof. In Section 2, I show that if the underlying theory proves that there are at least two elements in the universe, a more careful translation allows one to eliminate the new definitions with at most a polynomial increase in length. In fact, I will describe an explicit algorithm that can be implemented in polynomial time. The proof is not difficult, but it relies on the assumption that equality is included in the logic. A similar trick has been used by Solovay in simulating iterated definitions efficiently, as discussed in Section 3.2 of [Pudl´ak 1998]. Consequently, the result proved here may be folklore, but to my knowledge it has not appeared in the literature, and it is needed in Section 3. It is also sometimes convenient, in a first-order setting, to introduce Skolem func-. (shrink)