A tableau proof theory for CWPL

Abstract

In a recent paper, I presented a logic accommodating crossworld predication (crossworld predication logic, CWPL). Crossworld predication is the ascription of relations to objects, each of which is associated with a possible world (intuitively, an object associated with a possible world is the object as it is in the possible world). CWPL is a first-order modal logic with equality and λ-operator. Its advantage over other logics for crossworld predication I am familiar with (in particular, the ones elaborated by Butterfield and Stirling, Wehmeier, and Kocurek) is that it is based on the standard first-order modal vocabulary. Semantically, it is based on crossworld interpretation of predicates that assigns extensions to each n-ary predicate with respect to n-tuples of possible worlds rather than single possible worlds. To be able to employ crossworld interpretation of predicates when evaluating formulae, truth values are relativized to partial functions from variables to possible worlds. In the article mentioned above, I described the syntax and semantics of CWPL; the aim of the present paper is elaborating a tableau proof theory for CWPL and establishing its weak soundness and completeness.