Bounded Lukasiewicz Logics.
Agata Ciabattoni, George Metcalfe · Theorem Proving with Analytic Tableaux and Related Methods · 2003
In this work we investigate bounded Lukasiewicz logics, characterised as the intersection of the k-valued Lukasiewicz logics for k = 2, . . . , n (n ≥ 2). These logics formalise a generalisation of Ulam’s game with applications in Information Theory. Here we provide an analytic proof calculus G LBn for each bounded Lukasiewicz logic, obtained by adding a single rule to G L, a hypersequent calculus for Lukasiewicz infinite-valued logic. We give a first cut-elimination proof for G L with (suitable forms of) cut rules. We then prove completeness for G LBn with cut and show that cut can also be eliminated in this case.