Abstract
We present a Schütte-Tait style cut-elimination proof for the hypersequent calculus HIF for first-order Gödel logic. This proof allows to bound the depth of the resulting cut-free derivation by 4 ÇdÇρ(d) , where |d| is the depth of the original derivation and ρ(d) the maximal complexity of cut-formulas in it. We compare this Schütte-Tait style cut-elimination proof to a Gentzen style proof.
Research supported by EC Marie Curie fellowship HPMF-CT-1999-00301
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Avron: A constructive analysis of RM. J. Symbolic Logic, 52: 939–951, 1987.
A. Avron: Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence, 4: 225–248, 1991.
A. Avron: The Method of Hypersequents in the Proof Theory of Propositional Nonclassical Logics. In W. Hodges, M. Hyland, C. Steinhorn and J. Truss editors, Logic: from Foundations to Applications, European Logic Colloquium Oxford Science Publications. Clarendon Press. Oxford. 1–32. 1996.
M. Baaz, A. Ciabattoni, C. Fermüller: Cut-Elimination in a Sequents-of-Relations Calculus for Gödel Logic. In International Symposium on Multiple Valued Logic (ISMVL’2001), 181–186. IEEE. 2001.
M. Baaz, A. Ciabattoni, C. Fermüller: Herbrand’s Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving. In Proceedings of Logic for Programming and Automated Reasoning (LPAR’2001), LNAI 2250, 201–216. 2001.
M. Baaz, A. Ciabattoni, C. Fermüller: Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics. In M. Fitting and E. Orlowska editors, Theory and applications of Multiple-Valued Logics. To appear.
M. Baaz, A. Leitsch: Comparing the complexity of cut-elimination methods. In Proceedings of Proof Theory in Computer Science, LNCS 2183, 49–67. 2001.
M. Baaz, R. Zach: Hypersequents and the proof theory of intuitionistic fuzzy logic. In Proceedings of Computer Science Logic (CSL’2000), LNCS 1862, 187–201. 2000.
M. Dummett: A Propositional Logic with Denumerable Matrix. J. of Symbolic Logic, 24: 96–107. 1959.
G. Gentzen: Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift, 39: 176–210, 405–431. 1934.
K. Gödel: Zum Intuitionistischen Aussagenkalkul. Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. 1933.
P. Hájek: Metamathematics of Fuzzy Logic. Kluwer. 1998.
K. Schütte: Beweistheorie. Springer Verlag. 1960.
W.W. Tait: Normal derivability in classical logic. In The Sintax and Semantics of infinitary Languages, LNM 72, 204–236. 1968.
G. Takeuti: Proof Theory. North-Holland. 1987.
G. Takeuti, T. Titani: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. of Symbolic Logic, 49: 851–866. 1984.
A.S. Troelstra and H. Schwichtenberg: Basic Proof Theory. Cambridge University Press. 1996
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baaz, M., Ciabattoni, A. (2002). A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic. In: Egly, U., Fermüller, C.G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2002. Lecture Notes in Computer Science(), vol 2381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45616-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-45616-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43929-5
Online ISBN: 978-3-540-45616-2
eBook Packages: Springer Book Archive