Hostname: page-component-745bb68f8f-lrblm Total loading time: 0 Render date: 2025-02-05T22:45:08.941Z Has data issue: false hasContentIssue false
  • English
  • Français

A NOTE ON THE SEQUENT CALCULI ${{{\bf G3}[{\bf mic}]}}^{=}$

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  02 July 2020

FRANCO PARLAMENTO  and
FLAVIO PREVIALE
FRANCO PARLAMENTO
Affiliation:
DEPARTMENT OF MATHEMATICS, COMPUTER SCIENCE AND PHYSICS UNIVERSITY OF UDINE VIA DELLE SCIENZE 206, 33100 UDINE, ITALYE-mail: franco.parlamento@uniud.it
FLAVIO PREVIALE
Affiliation:
DEPARTMENT OF MATHEMATICS UNIVERSITY OF TURIN VIA CARLO ALBERTO 10, 10123 TORINO, ITALYE-mail: flavio.previale@unito.it
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 show that the replacement rule of the sequent calculi ${\bf G3[mic]}^= $ in [8] can be replaced by the simpler rule in which one of the principal formulae is not repeated in the premiss.

Keywords

sequent calculusequalityreplacement rulesadmissibility

MSC classification

Primary: 03F05: Cut-elimination and normal-form theorems
Type
Research Article
Information
The Review of Symbolic Logic , Volume 15 , Issue 2 , June 2022 , pp. 537 - 551
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

References

BIBLIOGRAPHY

Dragalin, A. (1988). Mathematical Intuitionism: Introduction to Proof Theory. Translation of Mathematical Monographs 67, Russian Original of 1979. Providence, RI: American Mathematical Society.CrossRefGoogle Scholar
Kleene, S.C. (1952). Introduction to Metamathematics. Amsterdam: North Holland.Google Scholar
Negri, S. & von Plato, J. (1998). Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4(4), 418–435 CrossRefGoogle Scholar
Negri, S. & von Plato, J. (2001). Structural Proof Theory. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
Parlamento, F. & Previale, F. (2019). The elimination of atomic cuts and the semishortening property for Gentzen’s sequent calculus with equality. Review of Symbolic Logic. doi.org/10.1017/S175502031900039X.Google Scholar
Takeuti, G. (1987). Proof Theory. Studies in Logic and the Foundations of Mathematics, Vol. 81 (second edition). Amsterdam: North Holland.Google Scholar
Troelstra, A. S. & Schwichtenberg, H. (1996). Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, Vol. 43. Cambridge: Cambridge University Press.Google Scholar
Troelstra, A. S. & Schwichtenberg, H. (2000). Basic Proof Theory (second edition). Cambridge: Cambridge University Press.CrossRefGoogle Scholar