Completeness for Weak Inquisitive First-Order Logic

Inquisitive logic extends classical logic to allow the formalization of questions. While its propositional variant has been axiomatized, it is still an open question whether the standard system of first-order inquisitive logic (InqBQ) is entailment compact and whether its validities are recursively enumerable. Sound and complete proof systems have been determined for syntactical fragments of the system. In this paper, we develop a sound and strongly complete proof system for the inquisitive logic InqWQ, which extends first-order classical logic with an inquisitive disjunction. We frame this logic as a fragment of InqBQ that excludes the inquisitive existential quantifier from its language. InqWQ occupies an intermediate position between propositional inquisitive logic and full InqBQ, while still retaining significant expressivity due to its first-order nature. To prove completeness, we adapt the methods described in Ciardelli and Grilletti (2022), where a sound and complete proof system is developed for entailments with conclusions in the restricted existential fragment. Unlike their system, our calculus is internal to the logic: its rules and derivations involve only InqWQ formulas.