Abstract
Gödel-Dummett logic is an extension of first-order intuitionistic logic with the linearity axiom \((A \supset B) \lor (B \supset A)\), and the so-called “quantifier shift” axiom \(\forall x(A \lor B(x)) \supset A \lor \forall x B(x).\) Semantically, it can be characterised as a logic for linear Kripke frames with constant domains. Gödel-Dummett logic has a natural formalisation in hypersequent calculus. However, if one drops the quantifier shift axiom, which corresponds to the constant domain property, then the resulting logic has to date no known hypersequent formalisation. We consider an extension of hypersequent calculus in which eigenvariables in the hypersequents form an explicit part of the structures of the hypersequents. This extra structure allows one to formulate quantifier rules which are more refined. We give a formalisation of Gödel-Dummett logic without the assumption of constant domain in this extended hypersequent calculus. We prove cut elimination for this hypersequent system, and show that it is sound and complete with respect to its Hilbert axiomatic system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avellone, A., Ferrari, M., Miglioli, P.: Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics. In: Logic Journal of the IGPL, vol. 7(4), pp. 447–480 (1999)
Avellone, A., Ferrari, M., Miglioli, P., Moscato, U.: A tableau calculus for Dummett predicate logic. In: Proc. of the Eleventh Brazilian Conference on Mathematical Logic 1996. Contemporary Mathematics, vol. 235, pp. 135–150. American Mathematical Society, Providence (1999)
Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4, 225–248 (1991)
Baaz, M., Ciabattoni, A.: A schütte-tait style cut-elimination proof for first-order gödel logic. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 24–37. Springer, Heidelberg (2002)
Baaz, M., Ciabattoni, A., Fermüller, C.G.: Hypersequent calculi for Gödel logics - a survey. J. Log. Comput. 13(6), 835–861 (2003)
Baaz, M., Iemhoff, R.: Gentzen calculi for the existence predicate. Studia Logica 82(1), 7–23 (2006)
Brünnler, K.: Cut elimination inside a deep inference system for classical predicate logic. Studia Logica 82(1), 51–71 (2006)
Brünnler, K.: How to universally close the existential rule. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 172–186. Springer, Heidelberg (2010)
Ciabattoni, A.: A proof-theoretical investigation of global intuitionistic (fuzzy) logic. Arch. Math. Log. 44(4), 435–457 (2005)
Corsi, G.: A cut-free calculus for Dummett’s LC quantified. Zeitschr. f. math. Logik und Grundlagen d. Math. 35, 289–301 (1989)
Corsi, G.: Completeness theorem for Dummett’s LC quantified and some of its extensions. Studia Logica 51(2), 317–336 (1992)
Dummett, M.: A propositional calculus with denumerable matrix. J. Symbolic Logic 24(2), 97–106 (1959)
Dyckhoff, R.: A deterministic terminating sequent calculus for Gödel-Dummett logic. Logic Journal of the IGPL 7(3), 319–326 (1999)
Gödel, K.: On the intuitionistic propositional calculus. In: Feferman, S., Dawson Jr, S.W., Kleene, S.C., Moore, G.H., Solovay, R.M., van Heijenoort, J. (eds.) Collected Works, vol. 1. Oxford University Press, Oxford (1986)
Iemhoff, R.: A note on linear Kripke models. J. Log. Comput. 15(4), 489–506 (2005)
McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theor. Comput. Sci. 232(1-2), 91–119 (2000)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991)
Poggiolesi, F.: The tree-hypersequent method for modal propositional logic. Trends in Logic: Towards Mathematical Philsophy, 9–30 (2009)
Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves. Lecture Notes in Mathematics, vol. 753, pp. 660–696. Springer, Berlin (1979)
Slaney, J.K.: Solution to a problem of Ono and Komori. Journal of Philosophical Logic 18, 103–111 (1989)
Sonobe, O.: A Gentzen-type formulation of some intermediate propositional logics. J. Tsuda College 7, 7–14 (1975)
Tiu, A.: A local system for intuitionistic logic. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 242–256. Springer, Heidelberg (2006)
Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996)
van Dalen, D.: Logic and Structure. Springer, Heidelberg (2004)
Wansing, H.: Displaying Modal Logic. Kluwer Academic Publishers, Boston (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiu, A. (2011). A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains. In: Brünnler, K., Metcalfe, G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2011. Lecture Notes in Computer Science(), vol 6793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22119-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-22119-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22118-7
Online ISBN: 978-3-642-22119-4
eBook Packages: Computer ScienceComputer Science (R0)