Preservation of expressive completeness in temporal models

DOI10.1016/0890-5401(87)90051-4MaRDI QIDQ1090324zbMATH OpenOpenAlexFDO

Authors Amihood Amir, Dov Gabbay

Publication date 1987

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0890-5401(87)90051-4

zbMATH Keywords

expressive completenesslexicographic product of time modelsm-dimensional connectivestemporal propositional calculustense logictruth table

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Review text

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.

Recommendations

• Separation in nonlinear time models
• Expressive completeness of temporal logic of trees
• Expressiveness of Metric modalities for continuous time
• scientific article; zbMATH DE number 757647
• scientific article; zbMATH DE number 747023

Cites work

• scientific article; zbMATH DE number 3827831 (Why is no real title available?)
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 3263218 (Why is no real title available?)
• Investigations in modal and tense logics with applications to problems in philosophy and linguistics

Cited in

(7)

• Finite \(H\)-dimension does not imply expressive completeness
• scientific article; zbMATH DE number 510781 (Why is no real title available?)
• scientific article; zbMATH DE number 1536553 (Why is no real title available?)
• Separation in nonlinear time models
• The \(k\)-variable property is stronger than H-dimension \(k\)
• SnS can be modally characterized
• Definability with bounded number of bound variables

This page was built for publication: Preservation of expressive completeness in temporal models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1090324)