Аннотация:
Boxing of a modal predicate logic $L$ is defined as the minimal logic containing all formulas $\Box A$, where $A$ is a theorem of $L$. For axiomatization of boxing it is usually insufficient just to add $\Box$ to axioms of $L$. The general problem of axiomatization of boxing was put in our talk “Boxing modal logics” at Logical Perspectives 2021. This problem is solved in the paper “On Kripke completeness of modal predicate logics around quantifed K5” (forthcoming in APAL).
The recipe is the following: take all possible shifts of the axioms, then take their universal closures with $\Box$ added. An $n$-shift of a predicate formula $A$ is obtained by increasing arities of all predicate letters by $n$ and adding fixed $n$ new parameters to all atoms occurring in $A$. In general this yields infinitely many axioms, but in many cases (described in the same talk and paper) 1-shifts are sufficient, so boxing preserves finite axiomatizability.
Our conjecture is that boxing of the finitely axiomatizable logic $\mathrm{QKAlt}_1$ (where $\mathrm{Alt}_1$ is the axiom of unique successor) is not finitely axiomatizable. The proof of this conjecture probably requires a nontrivial model-theoretic technique. In the talk we describe the first step on the way to the proof: 1-shifts are insufficient in this case.
