Arithmetical axiomatization of first-order temporal logic (Q1101100): Difference between revisions

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.