Free-Variable Tableaux for Constant-Domain Quantified Modal Logic with Rigid and Non-rigid Designation

This paper presents a sound and complete free-variable tableau calculus for constant-domain quantified modal logics, with a propositional analytical basis, i.e. one of the systems K, D, T, K4, S4. The calculus is obtained by addition of the classical free-variable γ-rule and the "liberalized" δ+-rule to a standard set of propositional rules. Thus, the proposed system characterizes proof-theoretically the constant-domain semantics, which cannot be captured by "standard" (non-prefixed, non-annotated) ground tableau calculi. The calculi are extended so as to deal also with non-rigid designation, by means of a simple numerical annotation on functional symbols, conveying some semantical information about the worlds where they are meant to be interpreted.