A Multiple-Conclusion Calculus for First-Order Godel Logic
Ori Lahav

Abstract We present a multiple-conclusion hypersequent system for the
standard first-order Godel logic.  We provide a constructive, direct,
and simple proof of the completeness of the cut-free part of this
system, thereby proving both completeness for its standard semantics,
and the admissibility of the cut rule in the full system. The results
also apply to derivations from assumptions (or ``non-logical axioms"),
showing that such derivations can be confined to those in which cuts
are made only on formulas which occur in the assumptions. Finally, the
results about the multiple-conclusion system are used to show that the
usual single-conclusion system for the standard first-order Godel
logic also admits (strong) cut-admissibility.

Joint work with Arnon Avron.