A deterministic terminating sequent calculus for Godel-Dummett logic
Roy Dyckhoff · Logic Journal of IGPL · 1999
We give a short proof-theoretic treatment of a terminating contraction-free calculus G4-LC for the zero-order Gödel-Dummett logic LC. This calculus is a slight variant of a calculus given by Avellone et al, who show its completeness by model-theoretic techniques. In our calculus, all the rules of G4-LC are invertible, thus allowing a deterministic proof-search procedure. Keywords:sequent calculus, contraction-free, terminating, Gödel-Dummett logic