Hostname: page-component-745bb68f8f-s22k5 Total loading time: 0 Render date: 2025-02-11T10:29:17.874Z Has data issue: false hasContentIssue false
  • English
  • Français

CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION

Published online by Cambridge University Press:  21 December 2018

ROY DYCKHOFF
ROY DYCKHOFF*
Affiliation:
SCHOOL OF COMPUTER SCIENCE UNIVERSITY OF ST ANDREWS ST ANDREWS KY16 9AJ, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We present a much-shortened proof of a major result (originally due to Vorob’ev) about intuitionistic propositional logic: in essence, a correction of our 1992 article, avoiding several unnecessary definitions.

Keywords

03F0303F50sequent calculusintuitionistic propositional logictermination
Type
Articles
Information
The Journal of Symbolic Logic , Volume 83 , Issue 4 , December 2018 , pp. 1680 - 1682
Copyright
Copyright © The Association for Symbolic Logic 2018 

References

REFERENCES

Dyckhoff, R., Contraction-free sequent calculi for intuitionistic logic, this Journal, vol. 57 (1992), pp. 795–807.Google Scholar
Dyckhoff, R., Intuitionistic decision procedures since Gentzen, Advances in Proof Theory (Kahle, R., Strahm, T., and Studer, T., editors), Birkhäuser, Basel, 2016, pp. 245–267.CrossRefGoogle Scholar
Pitts, A., On an interpretation of second order quantification in first order intuitionistic propositional logic, this Journal, vol. 57 (1992), pp. 33–52.Google Scholar
Troelstra, A. S. and Schwichtenberg, H., Basic Proof Theory, Cambridge University Press, Cambridge, 1996 and 2001.Google Scholar