Coherence in inquisitive first-order logic

Inquisitive first-order logic, InqBQ, is a conservative extension of classical first-order logic with questions. Formulas of InqBQ are interpreted with respect to information states---essentially, sets of relational structures over a common domain. It is unknown whether entailment in InqBQ is compact, and whether validities are recursively enumerable. In this paper, we study the semantic property of finite coherence: a formula of InqBQ is finitely coherent if in order to determine whether it is satisfied by a state, it suffices to check substates of a fixed finite size. We show that finite coherence has interesting implications. Most strikingly, entailment towards finitely coherent conclusions is compact. We identify a broad syntactic fragment of the language, the rex fragment, where all formulas are finitely coherent. We give a natural deduction system which is complete for InqBQ- entailments with rex conclusions, showing in particular that rex validities are recursively enumerable. On the way to this result, we study approximations of InqBQ obtained by restricting to information states of a fixed cardinality. We axiomatize the finite approximations and show that, in contrast to the situation in the propositional setting, InqBQ does not coincide with the limit of its finite approximations, settling a question posed by Sano.