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

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$.