Arithmetical axiomatization of first-order temporal logic (Q1101100): Difference between revisions
From MaRDI portal
Latest revision as of 16:45, 18 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Arithmetical axiomatization of first-order temporal logic |
scientific article |
Statements
Arithmetical axiomatization of first-order temporal logic (English)
0 references
1987
0 references
The paper is devoted to a syntactic characterization of first-order temporal formulae valid in Kripke structures that contain arithmetics of natural numbers. It is impossible to provide a finitistic and complete axiomatization of first-order temporal logic with linear and discrete time. In another paper the author has presented a complete but infinitary proof system. In order to deal with finitistic proof rules, one can consider arithmetical proof systems. A new method of obtaining arithmetical axiomatizations of logics of programs is introduced. A many sorted first-order language with equality, \(at\) oerator (A \(at B\) means that A holds in the next state that B holds), local and global variables, nexttime operator \({\mathcal O}\) applied to local variables is considered. Two proof systems are presented: the first one, PN, for logic \(L_ 0\) with the only temporal modality \({\mathcal O}\). The second one, PA, for logic \(L_{at}\)- a full temporal logic contaning \(at\), too. It is shown that PN is sound and complete, and that inductive defnitions do not add to the logical contents of arithmetical temporal theories based on \(L_ 0\). The proof system PA is shown to be arithmetically sound and arithmetically complete.
0 references
arithmetical completeness
0 references
arithmetical soundness
0 references
Kripke structures
0 references
first-order temporal logic
0 references
arithmetical proof systems
0 references
arithmetical axiomatizations of logics of programs
0 references