×

On the form of witness terms. (English) Zbl 1205.03064

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.

MSC:

03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
03F30 First-order arithmetic and fragments

Software:

CERES
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Baaz, M., Stefan, H.: On the non-confluence of cut-elimination. to appear · Zbl 1220.03048
[2] Baaz, M., Stefan, H., Leitsch, A., Richter, C., Spohr, H.: Cut-elimination: experiments with CERES. In: Baader, F. Voronkov, A. (eds.) Logic for programming, artificial intelligence, and reasoning (LPAR) 2004. Lecture Notes in Computer Science, vol. 3452, pp. 481–495. Springer (2005) · Zbl 1108.03305
[3] Baaz M., Stefan H., Leitsch A., Richter C., Spohr H.: CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Theor. Comput. Sci. 403(2–3), 160–175 (2008) · Zbl 1181.68264 · doi:10.1016/j.tcs.2008.02.043
[4] Baaz M., Leitsch A.: On skolemization and proof Complexity. Fundamenta Informaticae 20(4), 353–379 (1994) · Zbl 0815.03003
[5] Baaz M., Leitsch A.: Cut-elimination and redundancy-elimination by resolution. J. Symb. Comput. 29(2), 149–176 (2000) · Zbl 0976.03059 · doi:10.1006/jsco.1999.0359
[6] Buss S: An introduction to proof theory. In: Buss, S (eds) Handbook of proof theory pages, pp. 2–78. Elsevier, Amsterdam (1998) · Zbl 0912.03024
[7] Carbone A: Turning cycles into spirals. Ann. Pure Appl. Log. 96, 57–73 (1999) · Zbl 0923.03066 · doi:10.1016/S0168-0072(98)00031-1
[8] Carbone A.: Cycling in proofs and feasibility. Trans. Am. Math. Soc. 352, 2049–2075 (2000) · Zbl 0941.03064 · doi:10.1090/S0002-9947-99-02300-4
[9] Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata: techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata2007 . release October 12th 2007
[10] Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), pp. 233–243. ACM (2000) · Zbl 1321.68146
[11] Danos V., Joinet J.-B., Schellinx H.: A new deconstructive logic: linear logic. J. Symb. Log. 62(3), 755–807 (1997) · Zbl 0895.03023 · doi:10.2307/2275572
[12] Edwards H.M.: Fermat’s Last Theorem: A Genetic Introduction to Algebraic Number Theory. Springer, Berlin (1977) · Zbl 0355.12001
[13] Gallier J.: Constructive logics. Part I: a tutorial on proof systems and typed {\(\lambda\)}-calculi. Theor. Comput. Sci. 110(2), 249–339 (1993) · Zbl 0772.03026 · doi:10.1016/0304-3975(93)90011-H
[14] Gécseg F., Steinby M.: Tree languages. In: Rozenberg, G., Salomaa, A. (eds) Handbook of Formal Languages, vol 3., pp. 1–68. Springer, Berlin (1997) · Zbl 0913.68115
[15] Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39:176–210, 405–431, (1934–1935) · JFM 60.0020.02
[16] Gentzen G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112, 493–565 (1936) · Zbl 0014.38801 · doi:10.1007/BF01565428
[17] Gerhardy, P.: Refined Complexity Analysis of Cut Elimination. In: Baaz, M., Makowsky, J. (eds), Computer Science Logic (CSL) 2003, vol. 2803 of Lecture Notes in Computer Science, pp. 212–225. Springer (2003) · Zbl 1116.03318
[18] Gerhardy, P.: The role of quantifier alternations in cut elimination. Notre Dame J. Formal Log. 46(2), 165–171 (2005) · Zbl 1078.03045
[19] Girard J.-Y.: Proof Theory and Logical Complexity. Elsevier, Amsterdam (1987) · Zbl 0635.03052
[20] Kurt G.: Über eine noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287 (1958) · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[21] Heijltjes, W.: Proof Forests with Cut-Elimination Based on Herbrand’s Theorem. In: Classical Logic and Computation (CL&C) 2008, participant’s proceedings. available at http://www.homes.doc.ic.ac.uk/svb/CLaC08/programme.html
[22] Hetzl S.: Describing proofs by short tautologies. Ann. Pure Appl. Log. 159(1–2), 129–145 (2009) · Zbl 1172.03027 · doi:10.1016/j.apal.2008.10.010
[23] Hilbert D., Bernays P.: Grundlagen der Mathematik II. Springer, Berlin (1939) · JFM 65.0021.02
[24] Kohlenbach U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, Berlin (2008) · Zbl 1158.03002
[25] Kreisel, G.: Finiteness theorems in arithmetic: An Application of Herbrand’s Theorem for {\(\Sigma\)}2-Formulas. In: Stern, J. (eds.), Logic Colloquium 1981, pp. 39–55. Elsevier, Amsterdam (1982)
[26] Luckhardt H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symb. Log. 54(1), 234–263 (1989) · Zbl 0669.03024 · doi:10.2307/2275028
[27] McKinley, R.: Herbrand expansion proofs and proof identity. In: Classical Logic and Computation (CL&C) 2008, participant’s proceedings. available at http://www.homes.doc.ic.ac.uk/svb/CLaC08/programme.html
[28] Miller D.: A compact representation of proofs. Studia Logica 46(4), 347–370 (1987) · Zbl 0644.03033 · doi:10.1007/BF00370646
[29] Orevkov V.P.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta 88, 137–161 (1979) · Zbl 0429.03033
[30] Prawitz D.: Natural Deduction: A Proof-Theoretical Study. Almqvist and Wicksell, Stockholm (1965) · Zbl 0173.00205
[31] Pudlák P. : The Lengths of Proofs. In: Buss, S. (eds) Handbook of Proof Theory, pp. 547–637. Elsevier, Amsterdam (1998) · Zbl 0920.03056
[32] Ratiu, D., Trifonov, T.: Exploring the computational content of the infinite pigeonhole principle. J. Log. Comput. (to appear) · Zbl 1259.03072
[33] Schwichtenberg H.: Proof Theory: Some Applications of Cut-Elimination. In: Barwise, J. (eds) Handbook of Mathematical Logic, pp. 867–895. Elsevier, Amsterdam (1977)
[34] Statman R.: Lower bounds on Herbrand’s theorem. Proc. Am. Math. Soc. 75, 104–107 (1979) · Zbl 0411.03048
[35] Tait, W.W.: Normal derivability in classical logic. In: Barwise, J. (ed.) The Syntax and Semantics of Infinitary Languages, vol. 72 of Lecture Notes in Mathematics, pp. 204–236. Springer (1968) · Zbl 0206.00502
[36] Takeuti, G.: Proof Theory, 2nd edn. Elsevier, Amsterdam, March 1987 · Zbl 0609.03019
[37] Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge, October 2000
[38] Urban C., Bierman G.: Strong Normalization of Cut-Elimination in Classical Logic. Fundamenta Informaticae 45, 123–155 (2000) · Zbl 0982.03032
[39] Zhang W.: Cut elimination and automatic proof procedures. Theor. Comput. Sci. 91, 265–284 (1991) · Zbl 0745.68098 · doi:10.1016/0304-3975(91)90086-H
[40] Zhang W.: Depth of proofs, depth of cut-formulas and complexity of cut formulas. Theor. Comput. Sci. 129, 193–206 (1994) · Zbl 0807.03038 · doi:10.1016/0304-3975(94)90087-6
[41] Zucker J.: The correspondence between cut-elimination and normalization. Ann. Math. Log. 7, 1–112 (1974) · Zbl 0298.02023 · doi:10.1016/0003-4843(74)90010-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.