On the form of witness terms

We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions. Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only elementary cut-elimination. Keywords Cut-elimination

• Type: Journal
• Year: 2010
• Where: AML
• Authors: Stefan Hetzl
• Keywords: AML 2010, Cut-free Proofs, Peano Arithmetic, Witness Terms