A cut-free proof system for a predicate extension of the logic of provability

In this paper, we introduce a proof system NQGL for a Kripke complete predicate extension of the logic GL of provability. While GL is defined by K and the L¨ob formula ✷(✷p ⊃ p) ⊃ ✷p, NQGL does not have the L¨ob formula as its axiom, but has a non-compact rule, that is, a derivation rule with countably many premises, instead. We show that NQGL enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.

---

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).