A New Perspective for Hoare's Logic and Peano's Arithmetic

Abstract

Hoare's logic is an axiomatic system of proving programs correct, which has been extended to be a separation logic to reason about mutable heap structure. We develop the most fundamental logical structure of strongest postcondition of Hoare's logic in Peano's arithmetic \(PA\). Let \(p\in L\) and \(S\) be any while-program. The arithmetical definability of \(\textbf{N}\)-computable function \(f_S^{\textbf{N}}\) leads to separate \(S\) from \(SP(p,S)\), which defines the strongest postcondition of \(p\) and \(S\) over \(\textbf{N}\), achieving an equivalent but more meaningful form in \(PA\). From the reduction of Hoare's logic to PA, together with well-defined underlying semantics, it follows that Hoare's logic is sound and complete relative to the theory of \(PA\), which is different from the relative completeness in the sense of Cook. Finally, we discuss two ways to extend computability from the standard structure to nonstandard models of \(PA\).