Abstract
Definitional Reflection is a principle for introducing atomic assumptions, given a set of definitional rules for atomic formulas. In this paper, proof-theoretic properties of first-order sequent systems with definitional reflection are proved. It is shown that the presence of contraction and the use of implication in the bodies of definitional clauses exclude each other, if cut-elimination is desired.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abrusci, V. M. Phase semantics and sequent calculus for pure noncommutative classical linear prepositional logic. Journal of Symbolic Logic, 56 (1991), 1403–1451.
Ackermann, W. Widerspruchsfreier Aufbau der Logik.I. Typenfreies System ohne tertium non datur. Journal of Symbolic Logic, 15 (1950), 33–57.
Aronsson, M., Eriksson, L.-H., Gäredal, A., Hallnäs, L. & Olin, P. The programming language GCLA: A definitional appraoch to logic programming. New Generation Computing, 4 (1990), 381–404.
Clark, K. L. Negation as failure. In: Gallaire, H. & Minker, J. (Eds.), Logic and Data Bases, New York 1978, 293–322.
Curry, H. B. The inconsistency of certain formal logics. Journal of Symbolic Logic, 7 (1942), 115–117.
Došen, K. A historical introduction to substructural logics. In: Došen, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in Tübingen, October 1990. Oxford University Press, 1992.
Dunn, M. Consecution formulation of positive R with co-tenability and t. In: Anderson, A.R. & Belnap, N.D., Entailment: The Logic of Relevance and Necessity, Vol. I, Princeton University Press, 1975, 381–391.
Eriksson, L.-H. A finitary version of the calculus of partial inductive definitions. In: Eriksson, L.-H., Hallnäs, L. & Schroeder-Heister, P. (Eds.), Extensions of Logic Programming. Second International Workshop, ELP-91, Stockholm, January 1991, Proceedings. Springer LNCS, Vol. 596, Berlin 1992, 89–134.
Fitch. F. B. A system of formal logic without an analogue to the Curry W operator. Journal of Symbolic Logic, 1 (1936), 92–100.
Gentzen, G. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39 (1935), 176–210, 405–431, English Translation in: M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, Amsterdam: North Holland 1969, 68–131.
Girard, J.-Y. Linear logic. Theoretical Computer Science, 50 (1987), 1–102.
Hallnäs, L. Partial inductive definitions. Theoretical Computer Science, 87 (1991), 115–142. Previous versions published as SICS Research Reports 86005 (1986) and 86005C (1988), and in: Avron, A. et al. (Eds.), Workshop on General Logic, Dept. of Computer Science, University of Edinburgh, Report ECS-LFCS-88-52 (1988).
Hallnäs, L. & Schroeder-Heister, P. A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation, 1 (1990), 261–283; II. Programs as definitions, ibid. 1 (1991), 635–660. Previous version published at SICS Research Report 88005, 1988.
Lambek, J. The mathematics of sentence structure. American Mathematical Monthly, 65 (1958), 154–170.
Lambek, J. On the calculus of syntactic types. In: R. Jacobson (Ed.), Proceedings of the 12th Symposium on Applied Mathematics, AMS, Providence 1961, 166–178, 264–265.
Lambek, J. Logic without structural rules (Another look at cut elimination). In: Došen, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in Tübingen, October 1990. Oxford University Press, 1992.
Lambek, J. From categorial grammar to bilinear logic. In: Došen, K. & Schroeder-Heister, P. (Eds.) Substructural Logics: Proceedings of the Conference held in Tübingen, October 1990. Oxford University Press, 1992.
Lorenzen, P. Einführung in die operative Logik und Mathematik. Springer: Berlin 1955, 2nd ed. Berlin 1969.
Martin-Löf, P. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J. E. (Ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland: Amsterdam 1971, 179–216.
Nadathur, G. & Miller, D. An overview of λ-Prolog. In: Kowalski, R. & Bowen, K. (Eds.), Fifth International Conference on Logic Programming, MIT Press 1988, 810–827.
Read, S. Relevant Logic: A Philosophical Examination of Inference. Oxford: Basil Blackwell, 1988.
Schroeder-Heister, P. Hypothetical reasoning and definitional reflection in logic programming. In: P. Schroeder-Heister (Ed.), Extensions of Logic Programming. International Workshop, Tübingen, FRG, December 1989, Proceedings. Springer LNCS, Vol. 475, Berlin 1991, 327–340.
Slaney, J. Solution to a problem of Ono and Komori. Journal of Philosophical Logic, 18 (1989), 103–111.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schroeder-Heister, P. (1992). Cut-elimination in logics with definitional reflection. In: Pearce, D., Wansing, H. (eds) Nonclassical Logics and Information Processing. All-Berlin 1990. Lecture Notes in Computer Science, vol 619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031929
Download citation
DOI: https://doi.org/10.1007/BFb0031929
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55745-6
Online ISBN: 978-3-540-47280-3
eBook Packages: Springer Book Archive