Preservation of expressive completeness in temporal models (Q1090324)

The paper deals with the problem of expressive completeness of tense logic. Time model is a partially ordered structure \(<T,<,=>\), where T is a nonempty set (of moments of time). A wff of a temporal propositional calculus is built in an obvious manner. The concept of (generalized) truth tables is used. It is a flexible tool for semantic interpretation of temporal connectives. Intuitively, it is a rule of computing the value \(\| \#(A_ 1,...,A_ n)\|_ t^ h\) from values of \(\| A_ i\|^ h_ s\), where {\#} is an n-ary connective, t, s are moments of time, h is an assignment (a function from atoms to subsets of T). The truth table is defined as a predicate logic formula over \(<T,<,=>\). The concept of a table \(\psi_{\#}\) defining a connective {\#} is introduced. The problem (of expressive completeness) is: Is there a finite set C of connectives with which for any given table \(\psi_ A\) a corresponding wff A can be built? Some previous results are presented in the paper: there is no expressive completeness over the general ordered model; expressive completeness was shown over linear models. The authors have investigated some extensions of linear time models preserving the expressive completeness. The concept of a lexicographic product of time models is defined. The main results are: a lexicographic product of expressively complete time models is expressively complete; a constructive proof of this fact enables a description of the set of connectives expressively complete over the lexicographic product. A technique based on the concept of H-dimension (the minimal number of various bound variables needed in a table over \(<T,<,=>)\) is used. The equivalence of a finite H-dimension and expressive completeness holds in the case of m-dimensional connectives (connectives whose interpretation refers to m moments of time). A syntactic separation of variables corresponding to various basic time models is used. The preservation of finite H-dimensions is demonstrated using such separated (called mixed) formulas.