Proof theory of witnessed Godel logic: A negative result

摘要

We introduce a first sequent-style calculus for witnessed Godel 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 Godel logic, (fragments of) Lukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic.