On the form of witness terms (Q982183): Difference between revisions

The paper tries to characterize the set of cut-free proofs obtainable from proofs (possibly with cuts) through various methods of cut-elimination. The author restricts the attention to the term level of first-order proofs. For a valid existential formula \(F=\exists x_1\dots\exists x_n A(x_1,\dots,x_n)\), and an enumeration \(\overline{t_1},\overline{t_2},\dots\) of all \(n\)-tuples of variable-free terms, the set \({\mathcal H}(F)=\big\{\{ A(\overline{t_i})\mid i\in I\}\mid I\subseteq{\mathbb N}, \;\bigvee_{i\in I}A(\overline{t_i}) \text{\;is \;a \;tautology}\big\}\) is an upper semi-lattice. For each proof (possibly with cuts) \(\pi\) of \(F\) one can associate a set of points in \({\mathcal H}(F)\): the cut-free proofs reachable by cut-elimination from \(\pi\). The characterization problem that the author is interested in is finding the least upper bound of the reachable proofs, as it represents, as the author claims, the content of \(\pi\) on an elementary level (in the sense of the sub-formula property) but at the same time it considers \(\pi\) in its full generality (as no particular proof has been pre-determined by the choice of a cut-elimination procedure). Another aspect to take into consideration is finding a characterization based on a pure term formalism not referring to proofs. In the paper, the author gives a characterization for a non-trivial (but not necessarily the least) upper bound in terms of a regular tree grammar. Then, as an application, a certain class of proofs having only elementary cut-elimination is obtained. The results are also extended to Peano Arithmetic, and are demonstrated on the formalization of a short proof in number theory (of the theorem stating that for any \(m\geq 2\) and \(n\geq 1\) there exists a number between \(n\) and \(m^2\cdot n\) which can be written as a sum of two squares). The author notes that this method provides a new way of computing witness terms that circumvents cut-elimination.