Hostname: page-component-cd9895bd7-gxg78 Total loading time: 0 Render date: 2024-12-26T07:35:26.220Z Has data issue: false hasContentIssue false
  • English
  • Français

Admissibility of structural rules for contraction-free systems of intuitionistic logic

Published online by Cambridge University Press:  12 March 2014

Roy Dyckhoff  and
Sara Negri
Roy Dyckhoff
Affiliation:
School of Computer Science, St Andrews University, St Andrews. Fife KY16 9SS. Scotland, E-mail:[email protected]
Sara Negri
Affiliation:
Department of Philosophy, PL 24. Unioninkatu 40 B, 00014University of Helsinki, Finland, E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs, i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 4 , December 2000 , pp. 1499 - 1518
Copyright
Copyright © Association for Symbolic Logic 2000

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Avellone, A. and Ferrari, M., Almost duplication-free tableau calculi for propositional Lax logics, Theorem proving with analytic tableaux and related methods, Lecture Notes in Computer Science, vol. 1071, Springer-Verlag, 1996, pp. 48–65.CrossRefGoogle Scholar
[2]Barras, B., Boutin, S., et al., The Coq proof assistant reference manual, Technical report, INRIA, 1996, available from ftp.inria.fr.Google Scholar
[3]Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., and Zuber, W., Proof theory at work: Program development in the Minlog system, Automated deduction—A basis for applications, vol. II, Kluwer, 1998.CrossRefGoogle Scholar
[4]Dragalin, A. G., Mathematical intuitionism, Translations of Mathematical Monographs, vol. 67, American Mathematical Society, Providence, Rhode Island, 1988.Google Scholar
[5]Dyckhoff, R., Implementation of a decision procedure for intuitionistic propositional logic, available from http://www-theory.dcs.st-and.ac.uk/~rd/software/.Google Scholar
[6]Dyckhoff, R., Contraction-free sequent calculi for intuitionistic logic, this Journal, vol. 57 (1992), no. 3. pp. 795–807.Google Scholar
[7]Dyckhoff, R., Dragalin's proofs of cut-admissibility for the intuitionistic sequent calculiG3i and G3i′, Research Report CS/97/8, Computer Science Division, St Andrews University, 1997, available from http://www-theory.dcs.st-and.ac.uk/~rd/publications/.Google Scholar
[8]Dyckhoff, R. and Pinto, L., Implementation of a counter-model construction procedure for intuitionistic propositional logic, available from http://www-theory.dcs.st-and.ac.uk/~rd/software/.Google Scholar
[9]Heuerding, A.. Jäger, G., Schwendimann, S., and Seyfried, M., Propositional logics on the computer, Theorem proving with analytic tableaux and related methods, Lecture Notes in Computer Science, vol. 918, Springer-Verlag, 1995, pp. 310–323.CrossRefGoogle Scholar
[10]Hudelmaier, J., A Prolog program for intuitionistic logic, SNS-Bericht 88-28, University of TÜbingen, 1988.Google Scholar
[11]Hudelmaier, J., Bounds for cut elimination in intuitionistic propositional logic, Ph.D. thesis, University of TÜbingen, 1989.Google Scholar
[12]Hudelmaier, J., Bounds for cut elimination in intuitionistic propositional logic, Archive for Mathematical Logic, vol. 31 (1992). pp. 331–354.CrossRefGoogle Scholar
[13]Hudelmaier, J., An O(n log n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, vol. 3 (1993), pp. 63–76.CrossRefGoogle Scholar
[14]Hudelmaier, J., personal communication, 1994.Google Scholar
[15]Lincoln, P.. Scedrov, A., and Shankar, N., Linearizing intuitionistic implication, Sixth annual IEEE symposium on logic in computer science proceedings, Amsterdam 1991, 1991, pp. 51–62.Google Scholar
[16]Mendler, M.. A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits, Theorem proving with analytic tableaux and related methods, Lecture Notes in Computer Science, vol. 1071, Springer-Verlag, 1996, pp. 261–277.CrossRefGoogle Scholar
[17]Miglioli, P., Moscato, U., and Ornaghi, M., Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic, Logic Journal of the IGPL, vol. 5 (1997), no. 1, pp, 145–167.CrossRefGoogle Scholar
[18]Negri, S., Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic, vol. 38 (1999), no. 8, pp. 521–547.CrossRefGoogle Scholar
[19]Negri, S. and von Plato, J., From Kripke models to algebraic counter-valuations, Automated reasoning with analytic tableaux and related methods, proceedings (de Swart, H., editor), Lecture Notes in Artificial Intelligence, vol. 1397, Springer-Verlag, 1998, pp. 247–261.CrossRefGoogle Scholar
[20]Paulson, L., Isabelle: A generic theorem prover, Lecture Notes in Computer Science, vol. 828, Springer-Verlag, 1994.CrossRefGoogle Scholar
[21]Pinto, L. and Dyckhoff, R., Loop-free construction of counter-models for intuitionistic propositional logic, Symposia Gaussiana, Conf. A (Behara, , Fritsch, , and Lintz, , editors), Walter de Gruyter & Co., Berlin, 1995, pp. 225–232.CrossRefGoogle Scholar
[22]Pitts, A., On an interpretation of second-order quantification in first-order intuitionistic propositional logic, this Journal, vol. 57 (1992), no. 1, pp. 33–52.Google Scholar
[23]Schwichtenberg, H., personal communication, 1996.Google Scholar
[24]Stoughton, A., Porgi: a proof-or-refutation generator for intuitionistic propositional logic, Proceedings of the CADE-13 workshop on proof search in type-theoretic languages (Galmiche, D., editor), 1996, pp. 109–116.Google Scholar
[25]Tennant, N., Autologic, Edinburgh University Press, 1992.Google Scholar
[26]Troelstra, A. S. and Schwichtenberg, H., Basic proof theory, Cambridge University Press, 1996.Google Scholar
[27]von Plato, J., Positive Heyting algebras, manuscript, 1997.Google Scholar
[28]Vorob'ev, N. N., A new algorithm for derivability in the constructive propositional calculus, American Mathematical Society Translations, series 2, vol. 94, 1970, pp. 37–71.Google Scholar
[29]Weich, K., Beweissuche in der intuitionistischen Logik, Diplomarbeit, Institut fÜr Mathematik, University of Munich, 1995.Google Scholar
[30]Weich, K., Decision procedures for intuitionistic propositional logic by program extraction, Automated reasoning with analytic tableaux and related methods, proceedings (de Swart, H., editor), Lecture Notes in Artificial Intelligence, vol. 1397, Springer-Verlag, 1998, pp. 292–306.CrossRefGoogle Scholar