A Decidable Predicate Logic of Knowledge

The language we consider is that of classical first order logic augmented with the unary modal operator □. Sentences of this language are regarded as true or false in a knowledge-base KB, which is any finite set of □-free formulas. Truth of □α in KB is understood as that α is true in all classical models of KB and this interpretation is intended to capture the intuition "we know that α" behind □α. The resulting logic is, in general, undecidable and not even semidecidable. However, there is a natural fragment of the above language, called the constructive language, which yields a decidable logic. The only syntactic constraint in the constructive language is that there exists x should always be followed by □. That is, we are not allowed to simply say "there is x such that ..." and we can only say "there is x for which we know that ...". Under this constraint, truth of there existsxα(x) will always imply that an object x for which α(x) holds not only exists, but can be effectively found. This is generally what we want of there exists in practical applications: knowing that "there exists a combination c that opens safe S" has no significance unless such a combination c can actually be found, which, in our semantics, will be equivalent to saying that there is c for which we know that c opens S. So, it is only truth of the sentence there existsc□OPENS(c,S) that really matters, and the latter, unlike there existsc□OPENS(c,S) is a perfectly legal formula of the constructive language. I introduce a decidable sequent system C K N in the constructive language and prove its soundness and completeness with respect to the above semantics.