Proof theory of witnessed Gödel logic: A negative result
Matthias Baaz, Agata Ciabattoni · Journal of Logic and Computation · 2013
We introduce a first sequent-style calculus for witnessed Gödel logic. Our calculus makes use of the cut rule. We show that this is inescapable by establishing a general result on the non-existence of suitable analytic calculi for a large class of first-order logics. These include witnessed Gödel logic, (fragments of) Łukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic.