Abstract
A new cut elimination method is obtained here by “proof mining” (unwinding) from the following non-effective proof that begins with extracting an infinite branch \(\mathcal{B}\) when the canonical search tree \(\mathcal{T}\) for a given formula E of first order logic is not finite. The branch \(\mathcal{B}\) determines a semivaluation so that \(\mathcal{B}\models \bar{E}\) and (*) every semivaluation can be extended to a total valuation. Since for every derivation d of E and every model \(\mathcal{M}\), \({\mathcal M}\models E\), this provides a contradiction showing that \(\mathcal{T}\) is finite, \(\exists l(\mathcal{T}<l)\). A primitive recursive function L(d) such that \(\mathcal{T}< L(d)\) is obtained using instead of (*) the statement: For every r, if the canonical search tree \(\mathcal{T}^{r+1}\) with cuts of complexity r + 1 is finite, then \(\mathcal{T}^r\) is finite.
In our proof the reduction of (r + 1)-cuts does not introduce new r-cuts but preserves only one of the branches.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Kreisel, G., Mints, G., Simpson, S.: The Use of Abstract Language in Elementary Metamathematics. Lecture Notes in Mathematics 253, 38–131 (1975)
Mints, G.: The Universality of the Canonical Tree. Soviet Math. Dokl. 14, 527–532 (1976)
Mints, G.: E-theorems. J. Soviet Math. 8, 323–329 (1977)
Mints, G.: Unwinding a Non-effective Cut Elimination Proof. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 259–269. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Mints, G. (2008). Proof Search Tree and Cut Elimination. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-78127-1_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78126-4
Online ISBN: 978-3-540-78127-1
eBook Packages: Computer ScienceComputer Science (R0)