On the non-confluence of cut-elimination. (English) Zbl 1220.03048

Working in a language of first-order arithmetic, the authors construct a family of proofs of a simple \(\Sigma_1\) sentence with the property that different cut-elimination procedures produce cut-free proofs in which the existential quantifier has different witnesses. In fact, the example constructed guarantees that, for every term \(t\) of appropriate complexity, there is a cut-elimination procedure giving a cut-free proof in which \(t\) is the only possible witness to the existential quantifier. (Furthermore, these proofs have size polynomial in a parameter \(n\) while the number of choices of term \(t\) is super-exponential in \(n\).) These examples demonstrate that under the right circumstances, different methods for extracting witnesses from proofs could extract very different witnesses from the same proof.


03F05 Cut-elimination and normal-form theorems
Full Text: DOI


[1] Mathematische Zeitschrift 39 pp 405– (1934)
[2] DOI: 10.1007/BF01565428 · Zbl 0014.38801 · doi:10.1007/BF01565428
[3] DOI: 10.1145/322248.322249 · Zbl 0456.68119 · doi:10.1145/322248.322249
[4] Fundamenta Informaticae 45 pp 123– (2000)
[5] Proceedings of the American Mathematical Society 75 pp 104– (1979)
[6] Handbook of proof theory pp 547– (1998)
[7] Doklady Akademii Nauk 293 pp 313– (1987)
[8] 8th Soviet Conference on Mathematical Logic (1984)
[9] Zapiski Nauchnykh Seminarov Leningradskogo Otdelemya Matematicheskogo Instituta 88 pp 137– (1979)
[10] DOI: 10.1007/BF01625836 · Zbl 0644.03032 · doi:10.1007/BF01625836
[11] Grundlagen der Mathematik II (1939)
[12] Applied proof theory: Proof interpretations and their use in mathematics (2008) · Zbl 1158.03002
[13] DOI: 10.1111/j.1746-8361.1958.tb01464.x · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[14] Proofs and types (1989) · Zbl 0671.68002
[15] Proof theory and logical complexity (1987) · Zbl 0635.03052
[16] DOI: 10.1007/s00153-005-0275-1 · Zbl 1081.03056 · doi:10.1007/s00153-005-0275-1
[17] DOI: 10.1016/B978-044450813-3/50010-2 · doi:10.1016/B978-044450813-3/50010-2
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.