Predicate logics on display (Q1283134)

Display systems introduced by N. Belnap treat the modality \(\square\) using an ``inverse'' connective \(\bigcirc\) (sometimes in the past) and the following rules: \(\bigcirc A\to X/A\to\square X\) and \(A\to X/\square A\to\bigcirc X\). The author extends this treatment to predicate logic using \(\bigcirc_x\) indexed by variable \(x\). Additional modal-like operations \(S_{xy}\) modeling substitution \([x/y]\) are introduced. As always in display logic, numerous structural rules are needed.