This note is concerned with an aspect of the length of proof of formulas in recursively enumerable theories T adequate for recursive arithmetic. In particular, we consider the relative length of proof of formulas in the theories T and T(S), where F represents an r.e. set A in T and T(S) is the theory obtained from T by adjunction, as a new axiom, of a sentence S undecidable in T.Throughout the sequel T is a consistent, r.e. theory with standard formalization [7] in which all recursive functions of one variable are definable, and in which there is a binary formula x ≤ satisfying the well-known conditions [7]:Here is the constant term corresponding to the natural number n. Wn is the nth r.e. set in a standard enumeration of the r.e. sets. Also, we assume an a priori Gödel numbering of our formalism satisfying the usual conditions, so that all formulas are numbers ab initio.In the more common applications of the theorem below, if F is a k-ary formula of T, is a natural number that measures in some way the length of the shortest proof of in T.
Harpoon: Mechanizing Metatheory Interactively