A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics
A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper...
An Arithmetically Complete Predicate Modal Logic
Page 1