Incompleteness and the Barcan formula (Q1896788)

A normal system of propositional modal logic is said to be complete iff it can be characterized by a class of Kripke frames. Moreover, if a system of predicate modal logic is complete, then it is characterized by the class of all frames for the propositional logic on which it is based. Furthermore, if a propositional modal logic S is incomplete, then so is its predicate extension LPC+S which is obtained, basically, by adding to S the two quantifier rules: \(\forall 1\)\ \ If \(\alpha\) is any wff and \(x\) and \(y\) variables and \(\alpha [y/x ]\) is \(\alpha\) with free \(y\) replacing every free \(x\), then \(\forall x\alpha\supset [y/x ]\) is an axiom of LPC+S. \(\forall 2\)\ \ If \(\alpha \supset \beta\) is a theorem of LPC+S and \(x\) is not free in \(\alpha\), then \(\alpha \supset \forall x\beta\) is a theorem of LPC+S. The aim of the paper is to show conversely that there are several complete propositional modal logics which have incomplete predicate extensions (either with or without the Barcan formula \[ \text{BF} \quad \forall xL\alpha \supset L\forall x\alpha). \] For example, the predicate extension of the so-called system KG1, i.e. Kripke's basic system K plus axiom G1, \[ \text{G1} \quad MLp \supset LMp, \] (which is characterized by ``convergent'' frames satisfying condition \[ \forall ww' w'' (wRw' \wedge wRw'' \supset \exists w''' (w' Rw''' \wedge w'' Rw''')) \] for the accessibility relation \(R\)) turns out to be incomplete if it contains the Barcan formula. On the other hand, the predicate extension of, e.g., S4.4= S4+R1, \[ \text{R1} \quad p\supset (MLp \supset Lp), \] turns out to be incomplete if it does not contains BF. In addition to these results, a general semantics for modal predicate logic is outlined in ``Appendix 2'' of the paper.