Naming worlds in modal and temporal logic (Q5960007)

Predicate modal and temporal logics are studied in which a locality predicate \(W\) is added which gives names to worlds (or time points). An equal time predicate \(D(x,y)\) is also added which states that two time points are at the same distance from the root. Complete axiomatizations are provided for the systems studied. The completeness proofs use a procedure similar to a Henkin completion mixed with a tableau construction. The expressive power of the systems considered is highlighted by simulating other logics.