Propositional inquisitive logic is the limit of its n-bounded approximations. In the predicate setting, however, this does not hold anymore, as discovered by Ciardelli and Grilletti [11], who also found complete axiomatizations of n-bounded inquisitive logics InqBQn, for every fixed n. We introduce cut-free labelled sequent calculi for these logics. We illustrate the intricacies of schematic validity in such systems by showing that the well-known Casari formula is atomically valid in (a weak sublogic of) predicate inquisitive logic InqBQ, fails to be schematically valid in it, and yet is schematically valid under the finite boundedness assumption. The derivations in our calculi, however, are guaranteed to be schematically valid whenever a single specific rule is not used. © The Author(s) 2026.

This paper proposes cut-free sequent calculi for Wansing (1995)'s expansions of Nelson's logics N4(perpendicular to) (Odintsov 2005) and N3(perpendicular to) with the consistency operator M which was originally studied in Gabbay (1982). A key semantic feature of the logics is the failure of the persistency condition in the Kripke semantics, and, as a result, the deduction theorem fails. Reflecting this aspect, we formulate the right rule for intuitionistic implication simi larly to the right rule for the strict implication for modal logic S4. Our calculus, with the cut rule, is sound, and its cut-free calculus is complete for the intended Kripke semantics. As a corollary, the cut-elimination theorem is established semantically. We also extract a Hilbert system from the sequent calculus. Unlike Omori (2016), we do not assume the existence of a root point in a Kripke model. Therefore, our Hilbert system is also semantically complete for the class of models that may lack the root point.