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

2013/11/19 by Zhaowei Xu, Xu, Zhaowei
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO

paper · pdf · doi:10.48550/arxiv.1311.4617

arxiv created 2013/11/19 · openalex publication_date 2013/11/19 · arxiv updated 2013/11/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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∈ L and S be any while-program. The arithmetical definability of N-computable function f_S^N leads to separate S from SP(p,S), which defines the strongest postcondition of p and S over 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.

Related

• Completeness of Hoare Logic over Nonstandard Models
• On Completeness Results of Hoare Logic Relative to the Standard Model
• Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
• PA is instantiationally complete, but algorithmically incomplete: An alternative interpretation of Goedelian incompleteness under Church's Thesis that links formal logic and computability
• On the Consistency of Peano Arithmetic in a Proof-theoretic Semantics for Classical Logic