A Hypersequent System for Godel-Dummett Logic with Non-constant Domains

Godel-Dummett logic is an extension of first-order intuitionistic logic with the linearity axiom (A superset of B) boolean OR (B superset of A), and the so-called "quantifier shift" axiom for all x(A boolean OR B(x)) superset of A boolean OR for all xB(x). Semantically, it can be characterised as a logic for linear Kripke frames with constant domains. Godel-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 Godel-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.