On strictly arithmetical completeness in logics of programs (Q2277248)

A notion of strictly arithmetical completeness of an axiom system is introduced as the completeness w.r.t. strictly arithmetical interpretations. An interpretation is called to be strictly arithmetical if it contains the sort of natural numbers (with 0, 1, \(+\), and *), while all other of its sorts are effectively encodable by natural numbers. Thus strictly arithmetical interpretations form a proper subclass of the arithmetical ones (considered by David Harel and others). The author proposes a uniform technique to obtain the strictly arithmetical complete axiomatization for logics of programs, and exemplifies it by systems for algorithmic logic, concurrent dynamic logic, and temporal logic.