Semantic Incompleteness of Liberman et al. (2020)'s Hilbert-style System for Term-modal Logic K with Equality and Non-rigid Terms
Takahiro Sawasaki
TL;DR
The paper demonstrates the semantic incompleteness of the Hilbert-style system $\mathsf{H}\mathbf{K}$ for the minimal normal term-modal logic with equality and non-rigid terms by introducing a non-standard Kripke semantics in which constant and function meanings depend on relation meanings. It shows that the crucial first-order formula $x = c \to (P(x) \to P(c))$ is valid under the standard term-modal semantics but not derivable in $\mathsf{H}\mathbf{K}$, using a carefully constructed non-standard model $N = \langle D,W,R,J \rangle$ to separate semantic validity from provability. The result clarifies that semantic incompleteness is orthogonal to the term-modal aspects and motivates pursuit of sound and complete Hilbert-style systems for such logics, potentially via modifications of established first-order modal axioms. It also suggests the non-standard semantics as a tool for analysing context-dependent denotations in natural language.
Abstract
In this paper, we prove the semantic incompleteness of the Hilbert-style system for the minimal normal term-modal logic with equality and non-rigid terms that was proposed in Liberman et al. (2020) "Dynamic Term-modal Logics for First-order Epistemic Planning." Term-modal logic is a family of first-order modal logics having term-modal operators indexed with terms in the first-order language. While some first-order formula is valid over the class of all frames in the Kripke semantics for the term-modal logic proposed there, it is not derivable in Liberman et al. (2020)'s Hilbert-style system. We show this fact by introducing a non-standard Kripke semantics which makes the meanings of constants and function symbols relative to the meanings of relation symbols combined with them.