Cut-Elimination: Syntax and Semantics
Tóm tắt
In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES (cut-elimination by resolution) which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD (this part contains new previously unpublished results). In the generalized version CERESD we admit general elimination rules which are based on the mere semantical truth of sentences. We construct complete cut-free LK-derivations originating from derivations potentially containing unproven lemmas. Finally we give a comparison of reductive methods and CERESD by presenting a general simulation result.
Tài liệu tham khảo
Baaz M., Hetzl S., Weller D.: On the complexity of proof deskolemization. Journal of Symbolic Logic 77(2), 669–686 (2012)
Baaz M., Leitsch A.: Cut-Elimination and Redundancy-Elimination by Resolution. Journal of Symbolic Computation 29, 149–176 (2000)
Baaz M., Leitsch A.: Towards a Clausal Analysis of Cut-Elimination. Journal of Symbolic Computation 41, 381–410 (2006)
Baaz, M, and A. Leitsch, Methods of Cut-Elimination, Springer-Verlag, 2011.
Baaz, M., and P. Pudlak, Kreisels Conjecture for LE1, in P. Clote, J. Krajicek (eds.), Arithmetic Proof Theory and Computational Complexity, Oxford University Press, 1993, pp. 30–49.
Gentzen, G., Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39:405–431, 1934–1935.
Girard, J.Y., Proof Theory and Logical Complexity, Bibliopolis, 1987.
Krajicek, J., and P. Pudlak, The Number of Proof Lines and the Size of Proofs in First Order Logic, Archive of Mathematical Logic 27:69–84, 1988.
Leitsch, A., The Resolution Calculus, Springer-Verlag, 1997.
Robinson, J.A., A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM 12(1):23–41, 1965.
Schütte, K., Beweistheorie, Springer-Verlag 1960.
Tait, W.W., Normal derivability in classical logic, in The Syntax and Semantics of Infinitary Languages, Springer Verlag, 1968, pp. 204–236.
Takeuti, G., Proof Theory, North-Holland, 2nd edition, 1983.