Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-12-01T11:31:36.569Z 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
Get access Rights & Permissions [Opens in a new window]

Abstract

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 

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

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