Completeness of Hoare Logic over Nonstandard Models

TL;DR

This paper introduces a new, mathematically elegant and practically useful nonstandard semantics for Hoare logic, ensuring soundness and completeness in nonstandard models of Peano arithmetic, and aligning with existing semantics.

Contribution

It develops a novel interpretation of while-programs in nonstandard models that maintains $ ext{Sigma}_1$-definability and proves the standard Hoare logic's soundness and completeness under this semantics.

Findings

New semantics aligns with standard Hoare logic.

Ensures $ ext{Sigma}_1$-definability of functions in nonstandard models.

Shows equivalence of Hungary and axiomatic semantics with the new semantics.

Abstract

The nonstandard approach to program semantics has successfully resolved the completeness problem of Floyd-Hoare logic. The known versions of nonstandard semantics, the Hungary semantics and axiomatic semantics, are so general that they are absent either from mathematical elegance or from practical usefulness. The aim of this paper is to exhibit a not only mathematically elegant but also practically useful nonstandard semantics. A basic property of computable functions in the standard model $N$ of Peano arithmetic $PA$ is $\Sigma_1$-definability. However, the functions induced by the standard interpretation of while-programs $S$ in nonstandard models $M$ of $PA$ are not always arithmetical. The problem consists in that the standard termination of $S$ in $M$ uses the finiteness in $N$, which is not the finiteness in $M$. To this end, we shall give a new interpretation of $S$ in $M$ such that the termination of $S$ uses $M$-finiteness, and the functions produced by $S$ in all models of $PA$ have the uniform $\Sigma_1$-definability. Then we define, based on the new semantics of while-programs, a new semantics of Hoare logic in nonstandard models of $PA$, and show that the standard axiom system of Hoare logic is sound and complete w.r.t. the new semantics. It will be established, in $PA$, that the Hungary semantics and axiomatic semantics coincide with the new semantics of while-programs. Moreover, various comparisons with the previous results, usefulness of the nonstandard semantics, and remarks on the completeness issues are presented.

Equations

$$\Big{\lfloor}\frac{x}{y}\Big{\rfloor}=\left\{\begin{array}[]{ll}\mbox{the unique $z$ s.t.}\\ z\cdot y\leq x<(z+1)\cdot y,&\hbox{if $y\neq 0$;}\\ 0,&\hbox{if $y=0$.}\end{array}\right.$$

$$\Big{(}\frac{x}{y}\Big{)}=\left\{\begin{array}[]{ll}\mbox{the unique $z$ s.t.}\\ \exists w\leq x(y\cdot w+z=x\wedge z<y),&\hbox{if $y\neq 0$;}\\ x,&\hbox{otherwise.}\end{array}\right.$$

$$x-y=\left\{\begin{array}[]{ll}\mbox{the unique $z$ s.t.\ }x=y+z,&\hbox{if $y\leq x$;}\\ 0,&\hbox{otherwise.}\end{array}\right.$$

$$⟨x,y⟩$$

$$L(z)$$

$$R(z)$$

$$(x)_{i}=\Big{(}\frac{L(x)}{R(x)\cdot(i+1)+1}\Big{)}.$$

$$\begin{array}[]{l}\{p(E/x)\}x:=E\{p\}\end{array}$$

$$\begin{array}[]{c}\{p\}S_{1}\{r\},\{r\}S_{2}\{q\}\\ \hline\cr\{p\}S_{1};S_{2}\{q\}\end{array}$$

$$\begin{array}[]{c}\{p\wedge B\}S_{1}\{q\},\{p\wedge\neg B\}S_{2}\{q\}\\ \hline\cr\{p\}if\ B\ then\ S_{1}\ else\ S_{2}\ fi\{q\}\end{array}$$

$$\begin{array}[]{c}\{r\wedge B\}S_{0}\{r\}\\ \hline\cr\{r\}while\ B\ do\ S_{0}\ od\{r\wedge\neg B\}\end{array}$$

$$\begin{array}[]{c}p\rightarrow p_{1},\{p_{1}\}S\{q_{1}\},q_{1}\rightarrow q\\ \hline\cr\{p\}S\{q\}\end{array}$$

$$M$$

$${\phi }_{S_0}(\vec{x},y,\vec{z})::=\exists w(\overline{(w{)}_0}=\vec{x}\wedge \forall j<y{\alpha }_{S_0}(\overline{(w{)}_j},\overline{(w{)}_{j+1}})\wedge \overline{(w{)}_y}=\vec{z}).$$

$$C_S(i,w,\vec{x},\vec{y})$$

$${\alpha }_S^{\ast }(i,\vec{x},\vec{y})::=\exists w{C}_S(i,w,\vec{x},\vec{y})$$

$${\alpha }_S(\vec{x},\vec{y})::=\exists i{\alpha }_S^{\ast }(i,\vec{x},\vec{y})\wedge \neg B(\vec{y}/\vec{x}).$$

$$j\le i,w,w^{\prime }\in M$$

$$\displaystyle M\models\$$

$$\wedge {\alpha }_{S_0}(\overline{(w{)}_j},\overline{(w{)}_{j+1}}))\wedge \vec{b}=\overline{(w{)}_i}\wedge \neg B(\vec{b})$$

$$\displaystyle M\models\$$

$$\wedge {\alpha }_{S_0}(\overline{(w^{\prime }{)}_j},\overline{(w^{\prime }{)}_{j+1}}))\wedge \vec{c}=\overline{(w^{\prime }{)}_{i^{\prime }}}\wedge \neg B(\vec{c}).$$

$$M\models \forall i,\exists w(\overline{(w{)}_0}=\vec{x}\wedge \forall j<i\psi (\overline{(w{)}_j},\overline{(w{)}_{j+1}}))$$

$$M\models \exists i,w(\overline{(w{)}_0}=\vec{x}\wedge \forall j<i\psi (\overline{(w{)}_j},\overline{(w{)}_{j+1}})\wedge \neg \exists \vec{z}\psi (\overline{(w{)}_i},\vec{z})).$$

$$M\models \neg \exists w(\overline{(w{)}_0}=\vec{x}\wedge \forall j<i\psi (\overline{(w{)}_j},\overline{(w{)}_{j+1}}))$$

$$M\models \forall k<i,\exists w(\overline{(w{)}_0}=\vec{x}\wedge \forall j<k\psi (\overline{(w{)}_j},\overline{(w{)}_{j+1}})).$$

$$T\cup \{\theta (\infty )\}\cup \{\infty \ne n:n\in N\}$$

$$M\models \phi (\overrightarrow{s_0})\wedge \forall x(\phi (\overrightarrow{s_x})\to \phi (\overrightarrow{s_{x+1}}))\to \forall x\phi (\overrightarrow{s_x}).$$

$$M\models \phi (\vec{x},0,\overrightarrow{a_0})\wedge \forall j<i(\phi (\vec{x},j,\overrightarrow{a_j})\to \phi (\vec{x},j+1,\overrightarrow{a_{j+1}}))\to \forall j\le i\phi (\vec{x},j,\overrightarrow{a_j}).$$

Full text

Keywords: Hoare logic, Peano arithmetic, nonstandard models, nonstandard semantics, logical completeness

1 Introduction

Hoare logic is an axiomatic system of proving programs correct [1, 2, 3], which has had a significant impact upon the methods of both designing and verifying programs [4, 5, 6]. Hoare logic for the set $WP$ of while-programs with the first-order logical language $L$ and the first-order specification $T\subset L$ is denoted by $HL(T)$. Of special interest is the completeness of Hoare logic over nonstandard models.

The approach of using nonstandard models [7] in investigating Floyd-Hoare logic was started in [8, 9, 10], and pursued, refined by many authors since then, e.g., Csirmaz [11], Andreka et.al [12], Hortalá-González et.al [13], and Pasztor [14]. (For an extensive literature, see e.g. the references in [15].) It’s noteworthy that the Hungary semantics in [10] is defined over a particular class of infinite sequences of vectors of numbers that should satisfy the induction axioms for all formulas, and Floyd logic is logically complete w.r.t. this semantics. In addition, according to the Floyd-Hoare principle [2, 3], which states that the semantics of a programming language can be formally specified by the axioms and inference rules for proving the correctness of programs written in this language, an axiomatic semantics of while-programs has been suggested by Bergstra and Tucker [16] for which Hoare logic is logically complete. Observe that the Hungary semantics and axiomatic semantics are so general that they are absent either from mathematical elegance or from practical usefulness. It would be interesting, from a new perspective, to exhibit a not only mathematically elegant but also practically useful nonstandard semantics. In what follows, unless otherwise stated, let $L$ be the logical language of Peano arithmetic $PA$, and let $N$ be the standard model of $PA$.

The definability theorem [17, Chapter 16] says that a function in $N$ is computable (or equivalently $N$-computable [18]) iff it is $\Sigma_{1}$-definable in $N$ (i.e., the graph relation of this function is $\Sigma_{1}$), which means that a computable function should be “simple”. The proof of this theorem only considers a finite computation in $N$, which can be encoded as a natural number in a uniform way. In nonstandard models $M$ of $PA$ [19], a while-program $S$ produces a (pseudo-$M$-computable) function $\vec{y}=f_{S}^{M}(\vec{x})$. Intuitively we hope that $f_{S}^{M}$ is simple in $M$, that is, $\Sigma_{1}$-definable in $M$. However, it is hopeless, because for the while-program $S::=y:=0;while\ y<x\ do\ y:=y+1\ od$, $f_{S}^{M}$ is not $\Sigma_{1}$-definable, since the domain of $f_{S}^{M}$ is $N^{M}$, the standard part of $M$, which is not arithmetical by Robinson’s overspill lemma [17, Lemma 25.8]. The problem consists in the interpretation of while-programs in $M$, where the termination uses the finiteness in $N$ (i.e. the usual finiteness), which is not the finiteness in $M$. We shall introduce the concept of $M$-finiteness for the finiteness in $M$ and show that every $M$-finite sequence of vectors of numbers of $M$ can be coded uniformly as a number of $M$. Then a new interpretation of while-programs $S$ in all models $M$ of $PA$ such that the termination of $S$ uses $M$-finiteness will be given (the new input-output relation of $S$ in $M$ is denoted by $A_{S}^{M}$ in order to distinguish from the standard one $R_{S}^{M}$). It will be shown that $A_{S}^{M}$ produces a simple function $\vec{y}=g_{S}^{M}(\vec{x})$ in $M$. On the other hand, there exists a $\Sigma_{1}$-formula $\alpha_{S}(\vec{x},\vec{y})\in L$, dependent on $S$ but independent of any model of $PA$, that defines an (abstract) function $\vec{y}=g_{S}(\vec{x})$ in $PA$, i.e., $PA\vdash\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$. (Actually the formula $\alpha_{S}(\vec{x},\vec{y})$ can be chosen as one defining the $N$-computable function $f_{S}^{N}$ produced by $S$ in $N$.) It will be found that the interpretation of $g_{S}$ in $M$ coincides with $g_{S}^{M}$, for every $M\models PA$. To illustrates this, the following commutative diagram is shown.

Thus, the new interpretation of while-programs extend $N$-computability from $N$ to nonstandard models of $PA$ with the uniform $\Sigma_{1}$-definability. We can now define $M$-computability to be the computability induced by the new semantics of while-programs in $M$. In Subsection 4.2, the new semantics of while-programs is compared with the standard semantics; and Example 4.2.1 shows that $(x,0),$ $(x,1),$ $\ldots,$ $(x,x)$ is the unique sequence of vectors of $M$ computable by $S::=y:=0;while\ y<x\ do\ y:=y+1\ od$ with the input $(x,0)$ for the new semantics (i.e., $g_{S}^{M}(x,y)=(x,x)$).

We shall define, based on the new semantics of while-programs, a new semantics of Hoare logic in nonstandard models of $PA$. It will be proved that for any $PA\subseteq T\subseteq Th(N)$, the standard axiom system of $HL(T)$ is sound and complete w.r.t. the new semantics. It will be established, in $PA$, that the Hungary semantics and axiomatic semantics coincide with the new semantics of while-programs, and that the axiom system of Floyd logic is essentially the same as that of Hoare logic. Moreover, the reduction from $HL(T)$ to $T$ with $PA\subseteq T\subseteq Th(N)$ follows from the new completeness theorem of $HL(T)$, and the usefulness of the nonstandard semantics in Hoare logic is discussed. Finally, a detailed and thorough discussion of the completeness issues on Hoare logic is given.

The rest of this paper is structured as follows: some preliminary results are presented in Section 2; the concept of $M$-finiteness is introduced in Section 3; the definition of the new semantics of while-programs, and comparison with the standard and Hungary semantics are given in Section 4; the soundness and completeness of $HL(T)$ w.r.t. the new semantics, reduction from $HL(T)$ to $T$, and comparison with Floyd logic are shown in Section 5; the comparison with axiomatic semantics, and usefulness of nonstandard semantics in Hoare logic are shown in Section 6; remarks on the completeness issues of Hoare logic are given in Section 7; Section 8 concludes the paper.

2 Preliminaries

First some notations are introduced: in syntax, we write $\neg,\wedge,\vee,\rightarrow,\leftrightarrow,\forall,\exists$ to denote the negation, conjunction, disjunction, conditional, biconditional connectives and the universal, existential quantifiers; in semantics, we write $\sim,\&,|,\Rightarrow,\Leftrightarrow,\textbf{A},\textbf{E}$ to denote the corresponding connectives and quantifiers.

2.1 Peano arithmetic

Let $L$ be the logical language of $PA$ with the signature $\Sigma=\{+,\cdot,<,0,1\}$. For simplicity, the sum of $1$ with itself $n$ times is abbreviated as $n$. We use $n$ to denote both a closed term and a natural number, and use $M$ to denote both a model and its domain, which will be clear from the context. The formula $\varphi(t/x)$ stands for the result of simultaneously substituting $t$ for free occurrences of $x$ in $\varphi$; and $\varphi(t/x)$ will be denoted $\varphi(t)$ if the default variable $x$ is obvious. The denotation of a term $t$ at an assignment $v$ (for all the first order variables) over a model $M$ of $L$, denoted $t^{M,v}$, receives the standard meaning. The satisfaction of a formula $\varphi\in L$ at an assignment $v$ over a model $M$ of $L$, denoted $M,v\models\varphi$, is defined as usual; the satisfaction of $\varphi$ in $M$, denoted $M\models\varphi$, is defined such that for any assignment $v$ over $M$, $M,v\models\varphi$; the satisfaction of a theory $T\subset L$ in $M$, denoted $M\models T$, is defined such that for any $\varphi\in T$, $M\models\varphi$; the satisfaction of $\varphi$ in a theory $T\subset L$, denoted $T\models\varphi$, is defined such that for any $M\models T$, $M\models\varphi$. And the derivation of a formula $\varphi\in L$ from a theory $T\subset L$, denoted $T\vdash\varphi$, is defined as usual. The set of all theorems of $T\subset L$, denoted $Thm(T)$, is defined to be $Thm(T)::=\{\varphi\in L:T\vdash\varphi\}$. From Peano’s axioms, one can deduce the induction axiom scheme \varphi(0,\vec{y})\wedge\forall x\big{(}\varphi(x,\vec{y})\rightarrow\varphi(x+1,\vec{y})\big{)}\rightarrow\forall x\ \varphi(x,\vec{y}), the bounded induction scheme \varphi(0,\vec{y})\wedge\forall x<z\big{(}\varphi(x,\vec{y})\rightarrow\varphi(x+1,\vec{y})\big{)}\rightarrow\forall x\leq z\ \varphi(x,\vec{y}) and the least-number principle $\exists x\ \varphi(x,\vec{y})\rightarrow\exists z(\varphi(z,\vec{y})\wedge\forall u<z\ \neg\varphi(u,\vec{y}))$, where $\varphi(x,\vec{y})\in L$.

Gödel’s completeness theorem implies that for any $T\subset L$, $T\vdash\varphi$ iff $T\models\varphi$. The proof of this theorem shows that for any $T\subset L$ and any $\varphi\in L$, if $T\nvdash\varphi$ then there is a countable model $M$ of $L$ such that $M\models T$ and $M\nvDash\varphi$. This means that $T\models\varphi$ is equivalent to saying that for any countable $M\models T$, $M\models\varphi$ (the implication from left to right is trivial; for the opposite direction, assume that $T\nvDash\varphi$, by Gödel’s completeness theorem $T\nvdash\varphi$, then there exists a countable $M\models T$ such that $M\nvDash\varphi$, a contradiction), so in this paper only the countable models will be considered. Let $K$ be the set consisting of all natural numbers together with all pairs $(q,a)$ where $q$ is a rational number and $a$ an integer. Let $<_{K}$ be the order on $K$ in which the natural numbers come first, in their usual order, and the pairs afterward, ordered as follows: $(q,a)<_{K}(r,b)$ iff $q<r$ in the usual order on rational numbers, or $q=r$ and $a<b$ in the usual order on integers.

Lemma 2.1.1** (Cf. [17, p304]).**

The order relation on any countable nonstandard model of $PA$ is isomorphic to the ordering $<_{K}$ of $K$.

By a $\Delta_{0}$-formula (or alternatively rudimentary formula) of $L$ we mean a formula built up from atomic formulas using only negation, conjunction, disjunction, and bounded quantifications $\forall x<t$ and $\exists x<t$, where $t$ is a term of $L$ (possibly involving free variables). (Conditionals and biconditionals are allowed, too, since these officially are just abbreviations for certain constructions involving negation, conjunction, and disjunction. So are the bounded quantifiers $\forall x\leq t$ and $\exists x\leq t$, since these are equivalent to $\forall x<t+1$ and $\exists x<t+1$.) By a $\Sigma_{1}$-formula (or alternatively $\exists$-rudimentary formula) we mean a formula of form $\exists x\ F$ where $F$ is a $\Delta_{0}$-formula. It holds, in $PA$, that every generalized $\Sigma_{1}$-formula, obtainable from $\Delta_{0}$-formulas by conjunction, disjunction, bounded quantifications, and unbounded existential quantification, is logically equivalent to a $\Sigma_{1}$-formula. (The equivalence in $N$ is shown in [17, Proposition 16.10], and similarly for nonstandard models.)

2.2 Coding functions

Definition 2.2.1**.**

The following definitions (cf. [19, p54], [20, p42]) are thought of as taking place in $PA$.

(a) \Big{\lfloor}\frac{x}{y}\Big{\rfloor}(the integer part of $x$ divided by $y$) is the two-place function

[TABLE]

(b) \Big{(}\frac{x}{y}\Big{)}(the remainder on dividing $x$ by $y$) is given by

[TABLE]

(c) $x-y$ is defined by

[TABLE]

(d) $\sqrt{x}$ = the unique $y$ s.t. $y\cdot y\leq x<(y+1)\cdot(y+1)$.

The pairing function and unpairing functions in [20, p45] build a one-to-one correspondence between the set of ordered pairs of natural numbers and the set of natural numbers, and similarly for nonstandard models of $PA$. We formulate this by the following.

Definition 2.2.2**.**

Let T_{1}(z)::=\Big{\lfloor}\frac{\sqrt{8\cdot z+1}+1}{2}\Big{\rfloor}-1 and let $T_{2}(z)::=2\cdot z-T_{1}(z)\cdot T_{1}(z)$. We define $\langle x,y\rangle$, $L(z)$ and $R(z)$ by

[TABLE]

Lemma 2.2.3**.**

$PA$* proves that*

(a) $\langle L(z),R(z)\rangle=z$;

(b) $L(\langle x,y\rangle)=x$;

(c) $R(\langle x,y\rangle)=y$.

Notice that $\langle x,y\rangle$ is called extended pairing function and $L(z)$, $R(z)$ extended unpairing functions, each of which extends the classical counterpart from $N$ to nonstandard models of $PA$. For notational convenience, $(L(z),R(z))$ is denoted by $\overline{z}$. The extended pairing and unpairing functions can be generalized to $n$-tuples (for each $n\in N$) by setting $\langle x_{1},x_{2},\ldots,x_{n}\rangle=\langle x_{1},\langle x_{2},\ldots,x_{n}\rangle\rangle$ and $\overline{\langle x_{1},x_{2},\ldots,x_{n}\rangle}=(x_{1},\overline{\langle x_{2},\ldots,x_{n}\rangle})$.

Definition 2.2.4**.**

Define $(x)_{i}$ to be

[TABLE]

Such a function $(x)_{i}$ is usually called G$\ddot{o}$del’s $\beta$-function, but in the present context we obviously prefer the more suggestive term extended $\beta$-function. It’s easy to check, using Definition 2.2.4, that for every $M\models PA$ and every $w\in M$, there exists $i\in M$ such that $M\models\forall j>i((w)_{j}=(w)_{i})$. By the Chinese Remainder Theorem, $(x)_{i}$ can be used to code every finite sequence of natural numbers by choosing a suitable (but not unique) value for $x$: for every finite sequence $a_{0},a_{1},\ldots,a_{n}$ of natural numbers, there exists a natural number $w$ such that $N\models(w)_{i}=a_{i}$ for all $i\leq n$ [20, Theorem 2.4]. The following lemma formalizes this inside $PA$.

Lemma 2.2.5** (Cf. [19, p63]).**

$PA$* proves that*

(a) $\forall x,\exists y\ (y)_{0}=x$;

(b) $\forall x,y,z,\exists w((\forall i<z\ (w)_{i}=(y)_{i})\wedge(w)_{z}=x)$.

By Lemma 2.2.5, using mathematical induction, it follows that

Lemma 2.2.6** (Gödel’s Lemma, cf. [19, Lemma 5.9]).**

Let $M\models PA$, and let $n\in N$ with $x_{0}$, $x_{1}$, $\ldots$, $x_{n-1}\in M$. Then there exists $w\in M$ such that $M\models(w)_{i}=x_{i}$ for all $i<n$.

Note that these extended coding functions are all definable in $PA$ by $\Delta_{0}$-formulas of $L$.

2.3 Hoare logic

Based on the first-order logical language $L$, together with the program constructs ($:=$, ;, $if$, $then$, $else$, $fi$, $while$, $do$, $od$), a while-program $S$ is defined by $S::=x:=E\mid S_{1};S_{2}\mid if\ B\ then\ S_{1}\ else\ S_{2}\ fi\mid while\ B\ do\ S_{0}\ od$, where an expression $E$ is defined by $E::=0\mid 1\mid x\mid E_{1}+E_{2}\mid E_{1}\cdot E_{2}$, and a boolean expression $B$ is defined by $B::=E_{1}<E_{2}\mid\neg B_{1}\mid B_{1}\rightarrow B_{2}$. The set of all such while-programs is denoted $WP$. Without further declaration, for a while-program $S\in WP$, the vector $(x_{1},x_{2},\ldots,x_{n})$ of all $n$ program variables $x_{1},$ $x_{2},$ $\ldots,$ $x_{n}$ occurring in $S$ will be denoted by $\vec{x}$; the vector $(a_{1},a_{2},\ldots,a_{n})$ of $n$ numbers $a_{1},$ $a_{2},$ $\ldots,$ $a_{n}\in M$ will be denoted by $\vec{a}$; the connectives will be assumed to distribute over the components of the vectors (for instance, $\vec{a}\in M$ means $a_{1},$ $a_{2},$ $\ldots,$ $a_{n}\in M$, $\vec{x}=\vec{y}$ means $\bigwedge_{i=1}^{n}x_{i}=y_{i}$, and $\varphi(\vec{t}/\vec{x})$ means $\varphi(t_{1}/x_{1},t_{2}/x_{2},\ldots,t_{n}/x_{n})$). For an assignment $v$ over a model $M$ of $L$, let $v(\vec{x})$ be the vector of elements of $M$ assigned to $\vec{x}$ at $v$, and let $v(\vec{y}/\vec{x})$ be an assignment as $v$ except that $v(\vec{y}/\vec{x})(\vec{x})=\vec{y}$. For every $S\in WP$ and every model $M$ of $L$, the standard input-output relation $R_{S}^{M}$ of $S$ in $M$ is a binary relation on the set of assignments over $M$ inductively defined as follows:

• •

$(v,v^{\prime})\in R_{x:=E}^{M}$ $\Leftrightarrow$ $v^{\prime}=v(E^{M,v}/x)$;

• •

$(v,v^{\prime})\in R_{S_{1};S_{2}}^{M}$ $\Leftrightarrow$ $(v,v^{\prime})\in R_{S_{1}}^{M}\circ R_{S_{2}}^{M}$, where $(z,z^{\prime})\in R_{1}\circ R_{2}$ $\Leftrightarrow$ $\textbf{E}z^{\prime\prime}((z,z^{\prime\prime})\in R_{1}$ $\&$ $(z^{\prime\prime},z^{\prime})\in R_{2})$;

• •

$(v,v^{\prime})\in R_{if\ B\ then\ S_{1}\ else\ S_{2}\ fi}^{M}$ $\Leftrightarrow$ $M,v\models B$ $\&$ $(v,v^{\prime})\in R_{S_{1}}^{M}$ $|$ $M,v\not\models B$ $\&$ $(v,v^{\prime})\in R_{S_{2}}^{M}$;

• •

$(v,v^{\prime})\in R_{while\ B\ do\ S_{0}\ od}^{M}$ $\Leftrightarrow$ $\textbf{E}i\in N$, $\textbf{E}\vec{x_{0}},\ldots,\vec{x_{i}}\in M$ $(v(\vec{x})=\vec{x_{0}}$ $\&$ $\textbf{A}j<i(M,v(\vec{x_{j}}/\vec{x})\models B$ $\&$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in R_{S_{0}}^{M})$ $\&$ $v^{\prime}=v(\vec{x_{i}}/\vec{x})$ $\&$ $M,v^{\prime}\not\models B)$.

Given $S\in WP$ and a model $M$ of $L$, $R_{S}^{M}$ produces a vectorial function $\vec{y}=f_{S}^{M}(\vec{x})$ such that for any $\vec{a},\vec{b}\in M$, $f_{S}^{M}(\vec{a})=\vec{b}\Leftrightarrow\textbf{E}v,v^{\prime}(v(\vec{x})=\vec{a}\ \&\ v^{\prime}(\vec{x})=\vec{b}\ \&\ (v,v^{\prime})\in R_{S}^{M})$. Given a model $M$ of $L$ and an asserted program $\{p\}S\{q\}$, $\{p\}S\{q\}$ is satisfied at $M$ w.r.t. the standard semantics, denoted $M\models_{S}\{p\}S\{q\}$, iff for any assignment $v$ over $M$, M,v\models p\Rightarrow\textbf{A}v^{\prime}\big{(}(v,v^{\prime})\in R_{S}^{M}\Rightarrow M,v^{\prime}\models q\big{)}. Given a theory $T\subset L$ and an asserted program $\{p\}S\{q\}$, $\{p\}S\{q\}$ is satisfied at $T$ w.r.t. the standard semantics, denoted by $HL(T)\models_{S}\{p\}S\{q\}$, iff for any $M\models T$, $M\models_{S}\{p\}S\{q\}$.

Hoare logic $HL(T)$ for the set $WP$ of while-programs with the first-order logical language $L$ and the first-order specification $T\subset L$ has the standard axioms and inference rules [1, Section 2]: let $p,q,p_{1},q_{1},r\in L$, and let $S,$ $S_{0},$ $S_{1},$ $S_{2}\in WP$.

(1) Assignment Axiom Scheme: for $E$ an expression of $L$ and $x$ a variable of $L$, the asserted program

[TABLE]

is an axiom.

(2) Composition Rule:

[TABLE]

(3) Conditional Rule:

[TABLE]

(4) Iteration Rule:

[TABLE]

(5) Consequence Rule:

[TABLE]

And, in connection with (5),

(6) Specification Axiom: each theorem of $T$ is an axiom.

We write $HL(T)\vdash\{p\}S\{q\}$ to denote that the asserted program $\{p\}S\{q\}$ is provable from $HL(T)$. By the logical completeness of $HL(T)$ w.r.t. the standard semantics is meant that for any asserted program $\{p\}S\{q\}$, $HL(T)\vdash\{p\}S\{q\}$ iff $HL(T)\models_{S}\{p\}S\{q\}$.

3 The concept of $M$-finiteness

To begin with, the notion of pseudo-$M$-finiteness is introduced.

Definition 3.1**.**

Let $M\models PA$. A sequence of numbers of $M$ is pseudo-$M$-finite if it is indexed by an initial segment of $M$. That is, every sequence of numbers $a_{0},a_{1},\ldots,a_{i}\in M$ with $i\in M$ is pseudo-$M$-finite.

The sequences as defined above behave like finite sequences as far as the underlying model is concerned, but they may be infinite sequences when viewed from the outside world: let $i\in M\models PA$ be nonstandard; the pseudo-$M$-finite sequence of numbers [math], $1$, $\ldots$, $i$ is infinite. In particular, every pseudo-$N$-finite (or equivalently finite) sequence of natural numbers can be coded as a natural number by extended $\beta$-function. However, this property doesn’t hold for nonstandard models.

Proposition 3.2**.**

Every countable nonstandard model $M$ of $PA$ has a pseudo-$M$-finite sequence of numbers that can’t be coded as a number by extended $\beta$-function.

Proof.

Let $i\in M$ be nonstandard. We consider the set $A$ $=$ $\{$ $<$ $a_{0}$, $a_{1}$, $\ldots$, $a_{i}$ $>$ $:$ for each $j\leq i$, $a_{j}=0$ or $1$ $\}$ of pseudo-$M$-finite sequences of numbers of $M$. It’s obvious that $A$ is uncountable. However, $M$ has only a countable number of elements used as codes. This means that one of elements of $A$ can’t be coded as a number of $M$ by extended $\beta$-function. ∎

Definition 3.3**.**

Let $M\models PA$. A pseudo-$M$-finite sequence $\vec{a_{0}}$, $\vec{a_{1}}$, $\ldots$, $\vec{a_{i}}$ of vectors of numbers of $M$ is $M$-finite if there exist $\psi(\vec{x},y,\vec{z})\in L$ (the arguments $\vec{x}$, $y$ could be dummy) and $\vec{a}\in M$ such that for all $j$ smaller than or equal to $i$ there is a unique $\vec{z}\in M$ satisfying $M\models\psi(\vec{a},j,\vec{z})$, and this $\vec{z}$ happens to be $\vec{a_{j}}$, in symbols $M\models\forall j\leq i(\exists!\vec{z}\ \psi(\vec{a},j,\vec{z})\wedge\psi(\vec{a},j,\vec{a_{j}}))$.

For the sequence $\vec{x_{0}}$, $\vec{x_{1}}$, $\ldots$, $\vec{x_{n}}\in M\models PA$ with $n\in N$, by Lemmas 2.2.3 and 2.2.6, there exist $\psi(x,y,\vec{z})::=\overline{(x)_{y}}=\vec{z}$ and $x\in M$ such that $M\models\forall j\leq n(\exists!\vec{z}\ \psi(x,j,\vec{z})\wedge\psi(x,j,\vec{x_{j}}))$. For the sequence [math], $1$, $\ldots$, $i$ with $i\in M\models PA$ being nonstandard, there exist $\psi(x,y,z)::=z=y$ and $x\in M$ such that $M\models\forall j\leq i(\exists!z\ \psi(x,j,z)\wedge\psi(x,j,j))$. Observe from the above that the concept of finiteness is equal to that of $N$-finiteness (in symbols, finiteness $=$ $N$-finiteness) and, for any nonstandard $M\models PA$, the concept of finiteness is strictly less than that of $M$-finiteness (in symbols, finiteness $<$ $M$-finiteness).

The following theorem shows that for any $M\models PA$, every $M$-finite sequence of vectors of numbers of $M$ can be coded as a number of $M$ by extended coding functions.

Theorem 3.4**.**

Let $\psi(\vec{x},y,\vec{z})\in L$ and $M\models PA$. Then we have

[TABLE]

Proof.

Fix $\vec{x}\in M$. It suffices to prove that $M\models\forall y(\forall i\leq y,\exists!\vec{z}\ \psi(\vec{x},i,\vec{z})\rightarrow\exists w,\forall i\leq y,\forall\vec{z}(\psi(\vec{x},i,\vec{z})\rightarrow\overline{(w)_{i}}=\vec{z}))$ by induction on $y$ in the formula $\forall i\leq y,\exists!\vec{z}\ \psi(\vec{x},i,\vec{z})\rightarrow\exists w,\forall i\leq y,\forall\vec{z}(\psi(\vec{x},i,\vec{z})\rightarrow\overline{(w)_{i}}=\vec{z})$.

Suppose that $M\models\forall i\leq 0,\exists!\vec{z}\ \psi(\vec{x},i,\vec{z})$ for $y=0$. Then there exists a unique $\vec{z}\in M$ such that $M\models\psi(\vec{x},0,\vec{z})$. Using Lemmas 2.2.3 and 2.2.5, there is $w\in M$ such that $M\models\overline{(w)_{0}}=\vec{z}$. It follows that $M\models\exists w,\forall i\leq 0,\forall\vec{z}(\psi(\vec{x},i,\vec{z})\rightarrow\overline{(w)_{i}}=\vec{z})$. Thus we have

[TABLE]

As the induction hypothesis, suppose

[TABLE]

for any $y\in M$. Then we consider the case for $y+1$. Assume that $M\models\forall i\leq y+1,\exists!\vec{z}\ \psi(\vec{x},i,\vec{z})$. That is, there exists a unique sequence $\vec{z_{0}},\ldots,\vec{z_{y}},\vec{z_{y+1}}\in M$ such that $M\models\forall i\leq y+1\ \psi(\vec{x},i,\vec{z_{i}})$. By the induction hypothesis there exists $w\in M$ such that $M\models\forall i\leq y,\forall\vec{z}(\psi(\vec{x},i,\vec{z})\rightarrow\overline{(w)_{i}}=\vec{z})$. That is, $M\models\forall i\leq y\ \overline{(w)_{i}}=\vec{z_{i}}$. Using Lemmas 2.2.3 and 2.2.5, there exists $w^{\prime}\in M$ such that $M\models\forall i<y+1\ (w^{\prime})_{i}=(w)_{i}\wedge\overline{(w^{\prime})_{y+1}}=\vec{z_{y+1}}$ and hence we have $M\models\exists w,\forall i\leq y+1,\forall\vec{z}(\psi(\vec{x},i,\vec{z})\rightarrow\overline{(w)_{i}}=\vec{z})$, so it follows that

[TABLE]

∎

It’s noteworthy, in Definition 3.3, that the uniqueness condition $\exists!\vec{z}$ in the assertion $M\models\forall j\leq i(\exists!\vec{z}\ \psi(\vec{a},j,\vec{z})\wedge\psi(\vec{a},j,\vec{a_{j}}))$ is extremely important: let $\psi(\vec{x},y,z)::=(z=0)\vee(z=1)$; each element $<a_{0},a_{1},\ldots,a_{i}>$ of $A$, as defined in the proof of Proposition 3.2, satisfies the property $M\models\forall j\leq i\ \psi(\vec{a},j,a_{j})$ for arbitrary $\vec{a}\in M$; yet there exists such an element that can’t be coded as a number of $M$.

Defining $\psi(x,y,\vec{z})$ by $\psi(x,y,\vec{z})::=\overline{(x)_{y}}=\vec{z}$, it’s easy to see that every pseudo-$M$-finite sequence of vectors of numbers of $M$ coded as a number of $M$ by extended coding functions is $M$-finite. Hence the concept of $M$-finiteness captures precisely what can be coded in $M$ by extended coding functions; so it could be taken as an ideal extension to the usual concept of finiteness. We can say, in the sense of the above, that Theorem 3.4 extends Gödel’s Lemma (cf. Lemma 2.2.6) into a general setting.

4 The X-semantics of while-programs

4.1 The definition of the X-semantics

Definition 4.1.1** (The X-semantics of while-programs).**

Let $M\models PA$, and $S\in WP$ with program variables $\vec{x}=(x_{1},x_{2},\ldots,x_{n})$. The new input-output relation $A_{S}^{M}$ for $S$ on the set of assignments over $M$, and the formula $\alpha_{S}(\vec{x},\vec{y})\in L$ for $S$, where $\vec{y}=(y_{1},y_{2},\ldots,y_{n})$ is disjoint from $\vec{x}$, are defined inductively in (a) and (b) as follows:

Assignment: $S\equiv x_{i}:=E$.

(a) $(v,v^{\prime})\in A_{S}^{M}$ $\Leftrightarrow$ $v^{\prime}$ = $v(E^{M,v}/x_{i})$.

(b) $\alpha_{S}(\vec{x},\vec{y})::=y_{i}=E(\vec{x})\wedge\bigwedge_{1\leq j\leq n}^{j\neq i}y_{j}=x_{j}$.

Composition: $S\equiv S_{1};S_{2}$.

(a) $(v,v^{\prime})\in A_{S}^{M}$ $\Leftrightarrow$ $(v,v^{\prime})\in A_{S_{1}}^{M}\circ A_{S_{2}}^{M}$.

(b) $\alpha_{S}(\vec{x},\vec{y})::=\exists\vec{z}(\alpha_{S_{1}}(\vec{x},\vec{z}/\vec{y})\wedge\alpha_{S_{2}}(\vec{z}/\vec{x},\vec{y}))$.

Conditional: $S\equiv if\ B\ then\ S_{1}\ else\ S_{2}\ fi$.

(a) $(v,v^{\prime})\in A_{S}^{M}$ $\Leftrightarrow$ $M,v\models B$ $\&$ $(v,v^{\prime})\in A_{S_{1}}^{M}$ $|$ $M,v\not\models B$ $\&$ $(v,v^{\prime})\in A_{S_{2}}^{M}$.

(b) $\alpha_{S}(\vec{x},\vec{y})::=(B(\vec{x})\wedge\alpha_{S_{1}}(\vec{x},\vec{y}))\vee(\neg B(\vec{x})\wedge\alpha_{S_{2}}(\vec{x},\vec{y}))$.

Iteration: $S\equiv while\ B\ do\ S_{0}\ od$.

We define the formula $\varphi_{S_{0}}(\vec{x},y,\vec{z})\in L$ by

[TABLE]

(a) $(v,v^{\prime})\in A_{S}^{M}$ $\Leftrightarrow$ E $i,$ $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ $[$ $M\models\forall j\leq i\ \varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ $\&$ $v(\vec{x})=\vec{x_{0}}$ $\&$ A $j<i$ $($ $M,v(\vec{x_{j}}/\vec{x})\models B$ $\&$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in A_{S_{0}}^{M}$ $)$ $\&$ $v^{\prime}(\vec{x})=\vec{x_{i}}$ $\&$ $M,v^{\prime}\not\models B$ $]$.

(b) We first let

[TABLE]

then set

[TABLE]

and finally define

[TABLE]

Note that, in Definition 4.1.1, the definitions of $A_{S}^{M}$ and $\alpha_{S}(\vec{x},\vec{y})$ proceed simultaneously by induction on $S$, in that for the iteration case, $\varphi_{S_{0}}(\vec{x},y,\vec{z})$ is constructed from $\alpha_{S_{0}}$, and the definition of $A_{S}^{M}$ refers to $\varphi_{S_{0}}(\vec{x},y,\vec{z})$; for the role of $\varphi_{S_{0}}(\vec{x},y,\vec{z})$, we shall show in Claim 4.1.5 that any sequence $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}$ of vectors of numbers of $M$ such that $M\models\forall j\leq i\ \varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ is $M$-finite. Note also that a particular $M$-finite sequence of vectors of numbers of $M$ is adopted here rather than the more natural one, that is the sequence $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}$ such that $M\models\vec{x_{0}}=\vec{x}\wedge\forall j<i~{}\alpha_{S_{0}}(\vec{x_{j}},\vec{x_{j+1}})$ with $i,\vec{x}\in M$, because it has not been proved or disproved that the latter can be coded as a number of $M$ by extended coding functions. (If such a sequence satisfies the induction axioms for all formulas, then it is $M$-finite; for more details, cf. Definition 4.3.2 and Theorem 4.3.5.)

Proposition 4.1.2**.**

For every $S\in WP$, it is the case that in $PA$, $\alpha_{S}(\vec{x},\vec{y})$ and $\varphi_{S}(\vec{x},y,\vec{z})$ are logically equivalent to a $\Sigma_{1}$-formula.

Proof.

Let $S\in WP$. It’s easy to check, by induction on $S$, that $\alpha_{S}(\vec{x},\vec{y})$ and $\varphi_{S}(\vec{x},y,\vec{z})$ are generalized $\Sigma_{1}$-formulas, so, in $PA$, each is logically equivalent to a $\Sigma_{1}$-formula. ∎

Definition 4.1.3**.**

For every $S\in WP$ and every $M\models PA$, $\vec{y}=g_{S}^{M}(\vec{x})$ is defined such that for any $\vec{a},\vec{b}\in M$, $g_{S}^{M}(\vec{a})=\vec{b}\Leftrightarrow\textbf{E}v,v^{\prime}(v(\vec{x})=\vec{a}\ \&\ v^{\prime}(\vec{x})=\vec{b}\ \&\ (v,v^{\prime})\in A_{S}^{M})$.

Theorem 4.1.4**.**

For every $S\in WP$ and every $M\models PA$, $\vec{y}=g_{S}^{M}(\vec{x})$ is a function such that for any $\vec{a},\vec{b}\in M$, $g_{S}^{M}(\vec{a})=\vec{b}$ iff $M\models\alpha_{S}(\vec{a},\vec{b})$.

Proof.

To prove the theorem, by Definition 4.1.3, it suffices to prove that, for every $S\in WP$ and every $M\models PA$, $(v,v^{\prime})\in A_{S}^{M}$ iff $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$ in (a), and $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$ in (b). Fix $M\models PA$. The argument proceeds by induction on $S$.

Assignment: $S\equiv x_{i}:=E$.

(a) Consider $(v,v^{\prime})\in A_{S}^{M}$ as follows: by the definition of $A_{S}^{M}$, it is equivalent to $v^{\prime}(x_{i})=E^{M,v}$ $\&$ A $1\leq j\leq n$, $j\neq i$ $v^{\prime}(x_{j})=v(x_{j})$; then it is equivalent to $M\models v^{\prime}(x_{i})=E(v(\vec{x})/\vec{x})$ $\&$ A $1\leq i\leq n$, $j\neq i$ $v^{\prime}(x_{j})=v(x_{j})$; by the definition of $\alpha_{S}(\vec{x},\vec{y})$, it is equivalent to $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$.

(b) It’s trivial that $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$.

Composition: $S\equiv S_{1};S_{2}$.

(a) Consider $(v,v^{\prime})\in A_{S}^{M}$ as follows: by the definition of $A_{S}^{M}$, it is equivalent to $(v,v^{\prime})\in A_{S_{1}}^{M}\circ A_{S_{2}}^{M}$; by the definition of $\circ$, it is equivalent to $\textbf{E}v^{\prime\prime}$ $[$ $(v,v^{\prime\prime})\in A_{S_{1}}^{M}$ $\&$ $(v^{\prime\prime},v^{\prime})\in A_{S_{2}}^{M}$ $]$; by the induction hypothesis, it is equivalent to E $v^{\prime\prime}$ $[$ $M\models\alpha_{S_{1}}(v(\vec{x}),v^{\prime\prime}(\vec{x}))$ $\&$ $M\models\alpha_{S_{2}}(v^{\prime\prime}(\vec{x}),v^{\prime}(\vec{x}))$ $]$; by the definition of $\alpha_{S}(\vec{x},\vec{y})$, it is equivalent to $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$.

(b) Applying the induction hypothesis to $S_{1}$ (resp. $S_{2}$) yields $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{1}}(\vec{x},\vec{y})\wedge\alpha_{S_{1}}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$ (resp. $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{2}}(\vec{x},\vec{y})\wedge\alpha_{S_{2}}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$). By the definition of $\alpha_{S}(\vec{x},\vec{y})$, we have that $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$.

Conditional: $S\equiv if\ B\ then\ S_{1}\ else\ S_{2}\ fi$.

(a) Consider $(v,v^{\prime})\in A_{S}^{M}$ as follows: by the definition of $A_{S}^{M}$, it is equivalent to $M,v\models B$ $\&$ $(v,v^{\prime})\in A_{S_{1}}^{M}$ $|$ $M,v\not\models B$ $\&$ $(v,v^{\prime})\in A_{S_{2}}^{M}$; by the induction hypothesis, it is equivalent to $M\models B(v(\vec{x}))$ $\&$ $M\models\alpha_{S_{1}}(v(\vec{x}),v^{\prime}(\vec{x}))$ $|$ $M\not\models B(v(\vec{x}))$ $\&$ $M\models\alpha_{S_{2}}(v(\vec{x}),v^{\prime}(\vec{x}))$; by the definition of $\alpha_{S}(\vec{x},\vec{y})$, it is equivalent to $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$.

(b) Similar to the composition case.

Iteration: $S\equiv while\ B\ do\ S_{0}\ od$.

We begin with

Claim 4.1.5*.*

Let $i,\vec{x},\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ with $M\models\forall j\leq i\ \varphi_{S_{0}}(\vec{x},j,\vec{x_{j}})$. Then it is the case that

(1)

$M\models\forall j\leq i(\exists!\vec{z}\ \varphi_{S_{0}}(\vec{x},j,\vec{z})\wedge\varphi_{S_{0}}(\vec{x},j,\vec{x_{j}}))$;

(2)

$M\models\exists w,\forall j\leq i\ \overline{(w)_{j}}=\vec{x_{j}}$.

The proof of Claim 4.1.5 is shown as follows:

Proof of (1). By the premise, it suffices to prove the uniqueness of $\vec{z}$ in $M\models\forall j\leq i,\exists\vec{z}\ \varphi_{S_{0}}(\vec{x},j,\vec{z})$. suppose

[TABLE]

by the induction hypothesis we have $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{0}}(\vec{x},\vec{y})\wedge\alpha_{S_{0}}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$, then by induction on $k$ up to $j$ we can see that $M\models\forall k\leq j\ \overline{(w)_{k}}=\overline{(w^{\prime})_{k}}$ and hence in particular $M\models\overline{(w)_{j}}=\overline{(w^{\prime})_{j}}$, so it follows that $M\models\forall j\leq i,\vec{z},\vec{z^{\prime}}(\varphi_{S_{0}}(\vec{x},j,\vec{z})\wedge\varphi_{S_{0}}(\vec{x},j,\vec{z^{\prime}})\rightarrow\vec{z}=\vec{z^{\prime}})$.

Proof of (2). Immediate from (1) and Theorem 3.4.

We next give the main proof of this case:

(a) Consider $(v,v^{\prime})\in A_{S}^{M}$ as follows: by the definition of $A_{S}^{M}$, it is equivalent to E $i,$ $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ $[$ $M\models\forall j\leq i~{}\varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ $\&$ $v(\vec{x})=\vec{x_{0}}$ $\&$ A $j<i$ $($ $M,v(\vec{x_{j}}/\vec{x})\models B$ $\&$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in A_{S_{0}}^{M}$ $)$ $\&$ $v^{\prime}(\vec{x})=\vec{x_{i}}$ $\&$ $M,v^{\prime}\not\models B$ $]$; by the induction hypothesis, it is equivalent to E $i,$ $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ $[$ $M\models\forall j\leq i~{}\varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ $\&$ $v(\vec{x})=\vec{x_{0}}$ $\&$ $M\models\forall j<i(B(\vec{x_{j}})\wedge\alpha_{S_{0}}(\vec{x_{j}},\vec{x_{j+1}}))$ $\&$ $v^{\prime}(\vec{x})=\vec{x_{i}}$ $\&$ $M\not\models B(v^{\prime}(\vec{x}))$ $]$; using Claim 4.1.5, it is equivalent to E $i,w\in M$ $[$ $M\models v(\vec{x})=\overline{(w)_{0}}$ $\&$ $M\models\forall j<i(B(\overline{(w)_{j}})\wedge\alpha_{S_{0}}(\overline{(w)_{j}},\overline{(w)_{j+1}}))$ $\&$ $M\models v^{\prime}(\vec{x})=\overline{(w)_{i}}$ $\&$ $M\not\models B(v^{\prime}(\vec{x}))$ $]$; by the definition of $\alpha_{S}(\vec{x},\vec{y})$, it is equivalent to $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$.

(b) Suppose $\vec{a},\vec{b},\vec{c}\in M$ with $M\models\alpha_{S}(\vec{a},\vec{b})\wedge\alpha_{S}(\vec{a},\vec{c})$. Then we have to prove that $\vec{b}=\vec{c}$. By the supposition, together with the definition of $\alpha_{S}$, there exist $i,w,i^{\prime},w^{\prime}\in M$ such that

[TABLE]

and

[TABLE]

To prove $\vec{b}=\vec{c}$, by (1) and (2), it is enough to prove that $i=i^{\prime}$ and $M\models\overline{(w)_{i}}=\overline{(w^{\prime})_{i^{\prime}}}$. By the order relation of $M$ (cf. Lemma 2.1.1), it follows that $i\leq^{M}i^{\prime}$ or $i^{\prime}\leq^{M}i$. Without loss of generality, let $i\leq^{M}i^{\prime}$. By (1) and (2), we have that $M\models\overline{(w)_{0}}=\overline{(w^{\prime})_{0}}$. Suppose $j<^{M}i$ and $M\models\overline{(w)_{j}}=\overline{(w^{\prime})_{j}}$, then by the induction hypothesis we immediately have $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{0}}(\vec{x},\vec{y})\wedge\alpha_{S_{0}}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$ and hence by (1), (2) it follows that $M\models\overline{(w)_{j+1}}=\overline{(w^{\prime})_{j+1}}$, so we can see $M\models\forall j\leq i\ \overline{(w)_{j}}=\overline{(w^{\prime})_{j}}$ by induction on $j$ up to $i$. Suppose for a contradiction that $i<^{M}i^{\prime}$. This, together with (2), implies $M\models B(\overline{(w^{\prime})_{i}})$. From (1), we immediately have $M\not\models B(\overline{(w)_{i}})$. This, together with the fact $M\models\overline{(w)_{i}}=\overline{(w^{\prime})_{i}}$, implies $M\not\models B(\overline{(w^{\prime})_{i}})$, a contradiction. Thus we have $i=i^{\prime}$ and finally it follows that $M\models\overline{(w)_{i}}=\overline{(w^{\prime})_{i^{\prime}}}$. ∎

Note that in the proof of Theorem 4.1.4, the proof for that $(v,v^{\prime})\in A_{S}^{M}$ iff $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$, and the proof for that $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$ proceed simultaneously by induction on $S$, in that for the iteration case, the proof for that $(v,v^{\prime})\in A_{S}^{M}$ iff $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$ employs Claim 4.1.5, whose proof uses the induction hypothesis $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{0}}(\vec{x},\vec{y})\wedge\alpha_{S_{0}}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$.

Let $S\equiv while\ B\ do\ S_{0}\ od$ and $M\models PA$. The X-semantics of while-programs (cf. Definition 4.1.1) shows that every run $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}$ of $S$ in $M$ should satisfy the constraint $M\models\forall j\leq i\ \varphi_{S_{0}}(\vec{x_{0}},j,\vec{x_{j}})$. By Claim 4.1.5, on giving the input $\vec{x_{0}}$, this run will be uniquely determined by the constraint. Thus the natural way to decide whether a given sequence $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ (typically given by a formula with the argument $\vec{x_{0}}$) is a run of $S$ is to prove $M\models\forall j\leq i\ \varphi_{S_{0}}(\vec{x_{0}},j,\vec{x_{j}})$ by induction on $j$ up to $i$ in the formula $\varphi_{S_{0}}(\vec{x_{0}},j,\vec{x_{j}})$ using Lemmas 2.2.3 and 2.2.5.

Proposition 4.1.6**.**

Let $\psi(\vec{x},\vec{y})\in L$ and $M\models PA$ with $M\models\forall\vec{x},\vec{y},\vec{z}(\psi(\vec{x},\vec{y})\wedge\psi(\vec{x},\vec{z})\rightarrow\vec{y}=\vec{z})$. Then for any $\vec{x}\in M$, we have that either

[TABLE]

or

[TABLE]

Proof.

Fix $\vec{x}\in M$. Suppose that (3) doesn’t hold. Then we have to prove (4). By the supposition, we have that $M\models\exists i,\neg\exists w(\overline{(w)_{0}}=\vec{x}\wedge\forall j<i\ \psi(\overline{(w)_{j}},\overline{(w)_{j+1}}))$. Using the least number principle (cf. the Preliminaries), there exists $i\in M$ such that

[TABLE]

and

[TABLE]

Then $M\models i>0$, otherwise contradicting (5) using Lemma 2.2.5, and hence by (6) there exists $w\in M$ such that $M\models\overline{(w)_{0}}=\vec{x}\wedge\forall j<i-1\ \psi(\overline{(w)_{j}},\overline{(w)_{j+1}})$. To prove (4), it suffices to prove $M\models\neg\exists\vec{z}\ \psi(\overline{(w)_{i-1}},\vec{z})$. Assume for a contradiction that $M\nvDash\neg\exists\vec{z}\ \psi(\overline{(w)_{i-1}},\vec{z})$. Then there exists $\vec{z}\in M$ such that $M\models\psi(\overline{(w)_{i-1}},\vec{z})$, using Lemmas 2.2.3 and 2.2.5 there exists $w^{\prime}\in M$ such that $M\models\forall j<i\ (w^{\prime})_{j}=(w)_{j}\wedge\overline{(w^{\prime})_{i}}=\vec{z}$, hence $M\models\overline{(w^{\prime})_{0}}=\vec{x}\wedge\forall j<i\ \psi(\overline{(w^{\prime})_{j}},\overline{(w^{\prime})_{j+1}})$, a contradiction to (5), and so (4) holds. ∎

Corollary 4.1.7**.**

Let $M\models PA$, $v$ be an assignment over $M$, and $S::=while\ B\ do\ S_{0}\ od$ with $S_{0}\in WP$. Then either of the following two cases holds.

(1)

A* $i\in M$, E $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ $[$ $M\models\forall j\leq i~{}\varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ $\&$ $v(\vec{x})=\vec{x_{0}}$ $\&$ A $j<i$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in A_{S_{0}}^{M}$ $]$;*

(2)

E* $i,$ $\vec{x_{0}},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}\in M$ $[$ $M\models\forall j\leq i~{}\varphi_{S_{0}}(v(\vec{x}),j,\vec{x_{j}})$ $\&$ $v(\vec{x})=\vec{x_{0}}$ $\&$ A $j<i$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in A_{S_{0}}^{M}$ $\&$ $\sim\textbf{E}$ $\vec{z}\in M$ $(v(\vec{x_{i}}/\vec{x}),v(\vec{z}/\vec{x}))\in A_{S_{0}}^{M}$ $]$.*

Proof.

By Proposition 4.1.6, the definition of $\varphi_{S_{0}}$ (cf. Definition 4.1.1), and the fact that for any $S\in WP$ and any $M\models PA$, $(v,v^{\prime})\in A_{S}^{M}$ iff $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$, and $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S}(\vec{x},\vec{y})\wedge\alpha_{S}(\vec{x},\vec{z}/\vec{y})\rightarrow\vec{y}=\vec{z})$ (cf. Theorem 4.1.4). ∎

Observe from Corollary 4.1.7 that in Definition 4.1.1, for the iteration case, the definition of $A_{S}^{M}$, though restricted, can still exhaust the sequences of vectors of numbers of $M$ computable by $S_{0}$ that we are concerned with.

Proposition 4.1.8** (The induction of $M$-finiteness).**

Let $\vec{x},\vec{y},\vec{z}\in M\models PA$ and $S_{0}\in WP$. Then it is the case that

(i)

$M\models\varphi_{S_{0}}(\vec{x},0,\vec{y})\leftrightarrow\vec{x}=\vec{y}$;

(ii)

$M\models\varphi_{S_{0}}(\vec{x},i,\vec{y})\wedge\alpha_{S_{0}}(\vec{y},\vec{z})\leftrightarrow\varphi_{S_{0}}(\vec{x},i+1,\vec{z})$.

Proof.

(i) Consider $M\models\varphi_{S_{0}}(\vec{x},0,\vec{y})$ as follows: by the definition of $\varphi_{S_{0}}$, it is equivalent to saying that there exists $w\in M$ such that $M\models\overline{(w)_{0}}=\vec{x}\wedge\overline{(w)_{0}}=\vec{y}$; using Lemmas 2.2.3 and 2.2.5, it is equivalent to $M\models\vec{x}=\vec{y}$.

(ii) Consider $M\models\varphi_{S_{0}}(\vec{x},i,\vec{y})\wedge\alpha_{S_{0}}(\vec{y},\vec{z})$ as follows. By the definition of $\varphi_{S_{0}}$, it is equivalent to saying that there exists $w\in M$ such that $M\models\overline{(w)_{0}}=\vec{x}\wedge\forall j<i\ \alpha_{S_{0}}(\overline{(w)_{j}},\overline{(w)_{j+1}})\wedge\overline{(w)_{i}}=\vec{y}\wedge\alpha_{S_{0}}(\vec{y},\vec{z})$. Using Lemmas 2.2.3 and 2.2.5, it is equivalent to saying that there exist $w,w^{\prime}\in M$ such that $M\models\overline{(w)_{0}}=\vec{x}\wedge\forall j<i\ \alpha_{S_{0}}(\overline{(w)_{j}},\overline{(w)_{j+1}})\wedge\overline{(w)_{i}}=\vec{y}\wedge\alpha_{S_{0}}(\vec{y},\vec{z})$ and $M\models\forall j<i+1\ (w^{\prime})_{j}=(w)_{j}\wedge\overline{(w^{\prime})_{i+1}}=\vec{z}$. Using Claim 4.1.5 ($\Leftarrow$. Let $w=w^{\prime}$. $\overline{(w)_{i}}$ is the unique value of $\vec{y}$), it is equivalent to saying that there exists $w^{\prime}\in M$ such that $M\models\overline{(w^{\prime})_{0}}=\vec{x}\wedge\forall j<i+1\ \alpha_{S_{0}}(\overline{(w^{\prime})_{j}},\overline{(w^{\prime})_{j+1}})\wedge\overline{(w^{\prime})_{i+1}}=\vec{z}$. By the definition of $\varphi_{S_{0}}$, it is equivalent to $M\models\varphi_{S_{0}}(\vec{x},i+1,\vec{z})$. ∎

Corollary 4.1.9** (The induction of loop programs).**

Let $\vec{x},\vec{y},\vec{z}\in M\models PA$, and $S$ $::=$ $while$ $B$ $do$ $S_{0}$ $od$ with $S_{0}\in WP$. Then it is the case that

(i) $M\models\alpha_{S}^{*}(0,\vec{x},\vec{y})\leftrightarrow\vec{x}=\vec{y}$;

(ii) $M\models\alpha_{S}^{*}(i,\vec{x},\vec{y})\wedge(B(\vec{y}/\vec{x})\wedge\alpha_{S_{0}}(\vec{y}/\vec{x},\vec{z}/\vec{y}))\leftrightarrow\alpha_{S}^{*}(i+1,\vec{x},\vec{z}/\vec{y})$.

Proof.

By Proposition 4.1.8, together with the definitions of $\varphi_{S_{0}}$ and $\alpha_{S}^{*}$ (cf. Definition 4.1.1). ∎

4.2 Comparison with the standard semantics

In this subsection, the connections between the standard semantics and X-semantics of while-programs are built: to illustrate the similarity and difference of the two semantics, an example is shown; for the general relationship of the two semantics, two propositions are given ; the reasons why the standard semantics is “complex” in logic are discussed.

Example 4.2.1** (Identity functions).**

Let $S::=y:=0;while\ y<x\ do\ y:=y+1\ od$. For every $x,y\in N$, $f_{S}^{N}(x,y)$ = $g_{S}^{N}(x,y)$ = $(x,x)$. For every nonstandard $M\models PA$, and every $x,y\in M$, $f_{S}^{M}(x,y)=(x,x)$ if $x$ is a standard number of $M$, and $f_{S}^{M}$ is undefined for $(x,y)$ otherwise; in contrast, $g_{S}^{M}(x,y)=(x,x)$.

Proof.

Fix $x,y\in M\models PA$. The value of $f_{S}^{M}$ for the input $(x,y)$ is easy to calculate. It remains to show that $g_{S}^{M}(x,y)=(x,x)$. Let $S_{0}::=y:=y+1$. To prove $g_{S}^{M}(x,y)=(x,x)$, by X-semantics of while-programs (cf. Definition 4.1.1), it suffices to prove that $M\models\forall y\leq x\ \varphi_{S_{0}}((x,0),y,(x,y))$ by induction on $y$ up to $x$ in the formula $\varphi_{S_{0}}((x,0),y,(x,y))$. Using Lemmas 2.2.3 and 2.2.5, we have $M\models\exists w\ \overline{(w)_{0}}=(x,0)$, so it follows that $M\models\varphi_{S_{0}}((x,0),0,(x,0))$. Suppose $x>y\in M$ and $M\models\varphi_{S_{0}}((x,0),y,(x,y))$. By definition of $\varphi_{S_{0}}$, there exists $w\in M$ such that $M\models\overline{(w)_{0}}=(x,0)\wedge\forall j<y\ \alpha_{S_{0}}(\overline{(w)_{j}},\overline{(w)_{j+1}})\wedge\overline{(w)_{y}}=(x,y)$. Using Lemmas 2.2.3 and 2.2.5, there is $w^{\prime}\in M$ such that $M\models\forall j<y+1\ (w^{\prime})_{j}=(w)_{j}\wedge\overline{(w^{\prime})_{y+1}}=(x,y+1)$, so $M\models\varphi_{S_{0}}((x,0),y+1,(x,y+1))$ follows. ∎

Proposition 4.2.2**.**

For every $S\in WP$, $R_{S}^{N}=A_{S}^{N}$.

Proof.

Let $S\in WP$. To prove $R_{S}^{N}=A_{S}^{N}$, by Theorem 4.1.4, it suffices to prove that $(v,v^{\prime})\in R_{S}^{N}$ iff $N\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$, which is easy for the reader to verify. ∎

Proposition 4.2.3**.**

Let $M\models PA$ be nonstandard. For every $S\in WP$, $R_{S}^{M}\subseteq A_{S}^{M}$. Moreover, for particular choices of $S$, both $R_{S}^{M}=A_{S}^{M}$ and $R_{S}^{M}\subsetneqq A_{S}^{M}$ are able to hold.

Proof.

Let $S\in WP$. The proof for $R_{S}^{M}\subseteq A_{S}^{M}$ proceeds by induction on $S$: the cases for assignment, composition and conditional are easy; for the iteration case, by Theorem 4.1.4, it suffices to prove that $(v,v^{\prime})\in R_{S}^{M}$ $\Rightarrow$ $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$; this is the case due to Corollary 4.1.9. Moreover, for $S\equiv x:=x+1$, we have that $R_{S}^{M}=A_{S}^{M}$; for $S$ as defined in Example 4.2.1, we can see that $R_{S}^{M}\subsetneqq A_{S}^{M}$. ∎

Perhaps the most significant difference between the two semantics is that the X-semantics in nonstandard models is “simple” (or equivalently $\Sigma_{1}$-definable) while the standard semantics in nonstandard models is not always so. It appears that Robinson’s Overspill Lemma, which says that the finiteness in $N$ (defined by $\textbf{E}i\in N$) is not arithmetical, leads to this. Actually, the finiteness in $N$ is not defined in first-order logic: introducing more first-order ingredients into $PA$ is of no help.

Theorem 4.2.4** (Undefinability of the finiteness in $N$).**

The set of standard numbers is not defined in first-order logic.

Proof.

Suppose that $T$ is any first-order consistent extension of $PA$. Then we have to prove that the set of standard numbers is not defined in $T$. Assume for a contradiction that there exists $\theta(x)$ in the language of $T$ that defines the set of standard numbers in all models of $T$. As in the existence proof of nonstandard models of arithmetic, add a constant $\infty$ to the language of $T$ and apply the Compactness Theorem [17, Theorem 12.15] to the theory

[TABLE]

to conclude that it has a model. The denotation of $\infty$ in any such model will be a nonstandard element, contradicting the assumption. ∎

4.3 Comparison with the Hungary semantics

By a labeled program we understand a finite sequence of commands of the type $(i:u)$ ($i\in N$ is the label, and $u$ is either an assignment statement $x\hookleftarrow E$ or a conditional goto statement $if\ B\ goto\ j$, where $E$, $B$ are defined as for while-programs, and $j\in N$), in which no two members have the same label. Formally, a labeled program $P$ can be written as $P$ $=$ $<(i_{0},u_{0}),(i_{1},u_{1}),\ldots,(i_{n},u_{n})>$, where $\textbf{A}a<b\leq n\ i_{a}\neq i_{b}$. Let $M\models PA$. A trace of $P$ in $M$ is a sequence $s::=<\vec{s_{a}}>_{a\in M}$ indexed by the elements of $M$ such that $\vec{s_{a}}$ is a vector of numbers of $M$ assigned to the program variables of $P$ (including the control variable $\lambda$ used to denote the labels), and $s$ is a run of $P$; $P$ is said to halt at $\vec{s_{i}}$ if $\vec{s_{i}}(\lambda)\not\in\{i_{m}\ :\ m\leq n\}$ and $\textbf{A}j\geq^{M}i\ \vec{s_{j}}=\vec{s_{i}}$. (For more details, the reader refers to [10].)

Definition 4.3.1** (Cf. [10, pp165]).**

Let $M\models PA$. The sequence $<\vec{s_{a}}>_{a\in M}$ in $M$ is continuous if it satisfies the induction axiom scheme, that is, for any $\varphi(\vec{x})\in L$,

[TABLE]

By a continuous trace of $P$ in $M$ we understand a trace $<\vec{s_{a}}>_{a\in M}$ of $P$ which is continuous. The semantics of labeled programs over continuous traces is called the Hungary semantics.

Note that a continuous sequence in $M$ is $M$-infinite, which means that it is indexed by all elements of $M$, so it might not be coded as a number by extended coding functions (consider, e.g., the sequence $<a>_{a\in M}$). As while-programs are structured (by contrast labeled programs are unstructured), this definition of continuous sequences (cf. Definition 4.3.1) is not appropriate for building the continuous semantics of while-programs. In the present context, we prefer to adopt the following definition of continuous sequences.

Definition 4.3.2**.**

Let $i\in M\models PA$. A pseudo-$M$-finite sequence $\vec{a_{0}}$, $\vec{a_{1}}$, $\ldots$, $\vec{a_{i}}$ of vectors of numbers of $M$ is $M$-continuous if it satisfies the induction axiom scheme, that is, for any $\varphi(\vec{x},y,\vec{z})\in L$ and any $\vec{x}\in M$,

[TABLE]

It is inessential that the parameters $\vec{x}$, $y$ in $\varphi(\vec{x},y,\vec{z})$ are explicit in Definition 4.3.2, yet not in Definition 4.3.1. In particular, every finite sequence of vectors of natural numbers is $N$-continuous.

Proposition 4.3.3**.**

Every countable nonstandard model $M$ of $PA$ has an $M$-continuous sequence of numbers that cannot be coded as a number by extended $\beta$-function.

Proof.

Let $i\in M$ be nonstandard. Consider the set $A$ $=$ $\{$ $<$ $a_{0}$, $a_{1}$, $\ldots$, $a_{i}$ $>$ : $a_{0}=0$, $a_{1}=1$, and for each $2\leq j\leq i$, $a_{j}=0$ or $1$ $\}$. It’s easy to check that each element of $A$ is $M$-continuous. Note that $A$ is uncountable. However, $M$ has only countably many elements used as codes. This means that one of elements of $A$ can’t be coded as a number of $M$ by extended $\beta$-function. ∎

Proposition 4.3.4**.**

Let $M\models PA$. Every $M$-finite sequence $\vec{a_{0}}$, $\vec{a_{1}}$, $\ldots$, $\vec{a_{i}}$ of vectors of numbers of $M$ is $M$-continuous.

Proof.

Follows from the definition of $M$-finiteness (cf. Definition 3.3) and the induction axiom scheme of $PA$. ∎

Observe from Theorem 3.4 and Propositions 4.3.3, 4.3.4 that the concept of $M$-finiteness is strictly less than that of $M$-continuousness (in symbols, $M$-finiteness $<$ $M$-continuousness).

In order to distinguish from the known semantics of while-programs, for the continuous semantics of while-programs, we use $C_{S}^{M}$ to denote the input-output relation of $S\in WP$ in $M\models PA$. For any $S\in WP$ and any $M\models PA$, $C_{S}^{M}$ is defined as in the standard semantics except for the iteration case:

$(v,v^{\prime})\in C_{while\ B\ do\ S_{0}\ od}^{M}$ $\Leftrightarrow$ E an $M$-continuous sequence $\vec{x_{0}}$, $\ldots$, $\vec{x_{i}}\in M$ $[$ $v(\vec{x})=\vec{x_{0}}$ $\&$ $\textbf{A}j<i(M,v(\vec{x_{j}}/\vec{x})\models B$ $\&$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in C_{S_{0}}^{M})$ $\&$ $v^{\prime}=v(\vec{x_{i}}/\vec{x})$ $\&$ $M,v^{\prime}\not\models B$ $]$.

It’s not difficult to prove the equivalence of the Hungary semantics to the continuous semantics of while-programs: the equivalence in $N$ is shown in [21, Section 3-3.1]; and similarly for nonstandard models. To show the equivalence of the Hungary semantics to the X-semantics of while-programs, it suffices to show the equivalence of the continuous semantics to the X-semantics.

Theorem 4.3.5**.**

Let $M\models PA$ and $\psi(\vec{x},\vec{y})\in L$ with $M\models\forall\vec{x},\vec{y},\vec{z}(\psi(\vec{x},\vec{y})\wedge\psi(\vec{x},\vec{z})\rightarrow\vec{y}=\vec{z})$. Every $M$-continuous sequence $\vec{a_{0}},\vec{a_{1}},\ldots,\vec{a_{i}}$ of vectors of numbers of $M$ with $M\models\forall j<i\ \psi(\vec{a_{j}},\vec{a_{j+1}})$ can be coded as a number of $M$ by extended coding functions.

Proof.

Let $\varphi(\vec{x},y,\vec{z})::=\exists w(\overline{(w)_{0}}=\vec{x}\wedge\forall u<y\ \psi(\overline{(w)_{u}},\overline{(w)_{u+1}})\wedge\overline{(w)_{y}}=\vec{z})$. Using Lemmas 2.2.3 and 2.2.5, it’s easy to see that $M\models\varphi(\vec{a_{0}},0,\vec{a_{0}})\wedge\forall j<i(\varphi(\vec{a_{0}},j,\vec{a_{j}})\rightarrow\varphi(\vec{a_{0}},j+1,\vec{a_{j+1}}))$. Since the sequence $\vec{a_{0}},\vec{a_{1}},\ldots,\vec{a_{i}}$ is $M$-continuous, we have that $M\models\varphi(\vec{a_{0}},0,\vec{a_{0}})\wedge\forall j<i(\varphi(\vec{a_{0}},j,\vec{a_{j}})\rightarrow\varphi(\vec{a_{0}},j+1,\vec{a_{j+1}}))\rightarrow\forall j\leq i\ \varphi(\vec{a_{0}},j,\vec{a_{j}})$. Then it follows that $M\models\forall j\leq i\ \varphi(\vec{a_{0}},j,\vec{a_{j}})$. It’s easy to prove, similar to the proof of Claim 4.1.5 (1), that $M\models\forall j\leq i,\forall\vec{s},\vec{t}(\varphi(\vec{a_{0}},j,\vec{s})\wedge\varphi(\vec{a_{0}},j,\vec{t})\rightarrow\vec{s}=\vec{t})$. Then we have $M\models\forall j\leq i(\exists!\vec{z}\ \varphi(\vec{a_{0}},j,\vec{z})\wedge\varphi(\vec{a_{0}},j,\vec{a_{j}}))$. By Theorem 3.4, it follows that $\vec{a_{0}},\vec{a_{1}},\ldots,\vec{a_{i}}$ can be coded as a number of $M$ by extended coding functions. ∎

Note that, in Theorem 4.3.5, the premise $M\models\forall\vec{x},\vec{y},\vec{z}(\psi(\vec{x},\vec{y})\wedge\psi(\vec{x},\vec{z})\rightarrow\vec{y}=\vec{z})$ is essential for the conclusion to hold. Let $\psi(x,y)::=y=0\vee y=1$. Let $A$ be as defined in the proof of Proposition 4.3.3. It’s trivial that each element $<a_{0},a_{1},\ldots,a_{i}>$ of $A$ satisfies $M\models\forall j<i\ \psi(\vec{a_{j}},\vec{a_{j+1}})$. However, one of elements of $A$ can’t be coded as a number of $M$ by extended coding functions.

Theorem 4.3.6**.**

For every $S\in WP$ and every $M\models PA$, $A_{S}^{M}=C_{S}^{M}$.

Proof.

Let $S\in WP$ and let $M\models PA$. The proof of $A_{S}^{M}=C_{S}^{M}$ proceeds by induction on $S$. The cases for assignment, composition and conditional are easy. For the iteration case, let $S\equiv while\ B\ do\ S_{0}\ od$ with $S_{0}\in WP$. To prove $A_{S}^{M}=C_{S}^{M}$, it suffices to prove that $A_{S}^{M}\subseteq C_{S}^{M}$ and $A_{S}^{M}\supseteq C_{S}^{M}$. By Claim 4.1.5, together with Proposition 4.3.4, it’s easy to see that $A_{S}^{M}\subseteq C_{S}^{M}$. To prove $A_{S}^{M}\supseteq C_{S}^{M}$, by Theorem 4.1.4, it suffices to prove that $(v,v^{\prime})\in C_{S}^{M}$ $\Rightarrow$ $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$. Suppose that $(v,v^{\prime})\in C_{S}^{M}$. Then we have to prove that $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$. By the definition of $C_{S}^{M}$, we have that E an $M$-continuous sequence $\vec{x_{0}}$, $\ldots$, $\vec{x_{i}}\in M$ $[$ $v(\vec{x})=\vec{x_{0}}$ $\&$ $\textbf{A}j<i(M,v(\vec{x_{j}}/\vec{x})\models B$ $\&$ $(v(\vec{x_{j}}/\vec{x}),v(\vec{x_{j+1}}/\vec{x}))\in C_{S_{0}}^{M})$ $\&$ $v^{\prime}=v(\vec{x_{i}}/\vec{x})$ $\&$ $M,v^{\prime}\not\models B$ $]$. By the induction hypothesis, together with Theorem 4.1.4, it follows that $(v,v^{\prime})\in C_{S_{0}}^{M}$ $\Leftrightarrow$ $M\models\alpha_{S_{0}}(v(\vec{x}),v^{\prime}(\vec{x}))$. Then we have that E an $M$-continuous sequence $\vec{x_{0}}$, $\ldots$, $\vec{x_{i}}\in M$ $[$ $v(\vec{x})=\vec{x_{0}}$ $\&$ $\textbf{A}j<i(M\models B(\vec{x_{j}})$ $\&$ $M\models\alpha_{S_{0}}(\vec{x_{j}},\vec{x_{j+1}}))$ $\&$ $v^{\prime}(\vec{x})=\vec{x_{i}}$ $\&$ $M\not\models B(v^{\prime}(\vec{x}))$ $]$. By Theorem 4.3.5, together with the fact $M\models\forall\vec{x},\vec{y},\vec{z}(\alpha_{S_{0}}(\vec{x},\vec{y})\wedge\alpha_{S_{0}}(\vec{x},\vec{z})\rightarrow\vec{y}=\vec{z})$ (cf. Theorem 4.1.4), we have that E $i,w\in M$ $[$ $M\models v(\vec{x})=\overline{(w)_{0}}$ $\&$ $M\models\forall j<i(B(\overline{(w)_{j}})\wedge\alpha_{S_{0}}(\overline{(w)_{j}},\overline{(w)_{j+1}}))$ $\&$ $M\models v^{\prime}(\vec{x})=\overline{(w)_{i}}$ $\&$ $M\not\models B(v^{\prime}(\vec{x}))$ $]$. By the definition of $\alpha_{S}$, it follows that $M\models\alpha_{S}(v(\vec{x}),v^{\prime}(\vec{x}))$. ∎

Summarizing the above results, we conclude that the X-semantics of while-programs is equivalent to the Hungary semantics. Moreover, the use of $M$-finiteness in the definition of the nonstandard semantics has an advantage over the use of $M$-continuousness: $M$-finiteness enables us to construct a $\Sigma_{1}$-formula to uniquely determine the sequence of computation, whereas in the Hungary semantics, we have to verify whether a sequence satisfies the induction axioms for all formulas.

5 Soundness and completeness of Hoare logic

5.1 Soundness and Completenss of $HL(T)$

Definition 5.1.1**.**

Given a model $M\models PA$ and an asserted program $\{p\}S\{q\}$, $\{p\}S\{q\}$ is satisfied at $M$ w.r.t. the X-semantics, denoted

[TABLE]

iff for every assignment $v$ over $M$,

[TABLE]

Definition 5.1.2**.**

Given a theory $PA\subseteq T\subseteq Th(N)$ and an asserted program $\{p\}S\{q\}$, $\{p\}S\{q\}$ is satisfied at $T$ w.r.t. the X-semantics, denoted

[TABLE]

iff for every model $M\models T$,

[TABLE]

Definition 5.1.3**.**

Let $p\in L$, $S\in WP$ and $M\models PA$. The strongest postcondition $sp_{X}^{M}(p,S)$ of $S$ relative to $p$ w.r.t. the X-semantics on the set $V$ of assignments over $M$ is defined by

[TABLE]

The formal strongest postcondition $SP(p,S)(\vec{x})$ of $S$ relative to $p$ is defined by

[TABLE]

Lemma 5.1.4** (Strongest Postcondition Lemma).**

Let $p\in L$, $S\in WP$ and $M\models PA$. It is the case that

(i) $v\in sp_{X}^{M}(p,S)$ $\Leftrightarrow$ $M,v\models SP(p,S)$;

(ii) $M\models_{X}\{p\}S\{SP(p,S)\}$;

(iii) $M\models_{X}\{p\}S\{q\}$ $\Leftrightarrow$ $M\models SP(p,S)\rightarrow q$.

Proof.

Immediate from Theorem 4.1.4. ∎

Definition 5.1.5**.**

Let $p\in L$, $S::=while\ B\ do\ S_{0}\ od$ and $M\models PA$. The loop invariant $inv_{X}^{M}(p,S)$ of $S$ relative to $p$ w.r.t. the X-semantics on the set $V$ of assignments over $M$ is defined by

[TABLE]

The formal loop invariant $INV(p,S)(\vec{x})$ of $S$ relative to $p$ is defined by

[TABLE]

Lemma 5.1.6** (Loop Invariant Lemma).**

Let $p\in L$, $S::=while\ B\ do\ S_{0}\ od$ and $M\models PA$. It is the case that

(i) $v\in inv_{X}^{M}(p,S)$ $\Leftrightarrow$ $M,v\models INV(p,S)(\vec{x})$;

(ii) $M\models p\rightarrow INV(p,S)$;

(iii) $M\models_{X}\{INV(p,S)\wedge B\}S_{0}\{INV(p,S)\}$;

(iv) $M\models_{X}\{p\}S\{q\}$ $\Leftrightarrow$ $M\models INV(p,S)(\vec{x})\wedge\neg B(\vec{x})\rightarrow q(\vec{x})$.

Proof.

Follows from Theorem 4.1.4 and Corollary 4.1.9. ∎

Definition 5.1.7**.**

Given a theory $PA\subseteq T\subseteq Th(N)$, $HL(T)$ is sound and complete w.r.t. the X-semantics iff for any $p,q\in L$ and any $S\in WP$,

[TABLE]

We are now positioned to state the main theorem of this paper.

Theorem 5.1.8** (Soundness and Completeness of $HL(T)$).**

Let $PA\subseteq T\subseteq Th(N)$. Then the Hoare logic $HL(T)$ is sound and complete w.r.t. the X-semantics. That is, for any $p,q\in L$ and any $S\in WP$,

[TABLE]

Proof.

Let $p,q\in L$ and $S\in WP$. The proof of this theorem is partitioned into two parts: the “only if” part ($\Rightarrow$) and the “if” part ($\Leftarrow$).

$(\Rightarrow)$. Suppose that $HL(T)\vdash\{p\}S\{q\}$. Then we have to prove that $HL(T)\models_{X}\{p\}S\{q\}$. The argument proceeds by induction on the length of the proof of $\{p\}S\{q\}$ in $HL(T)$, where the last step is divided into the following cases.

Assignment Axiom Scheme: $S\equiv x_{i}:=E$ and $HL(T)\vdash\{p\}S\{q\}$. By the Assignment Axiom Scheme, we have that $p\equiv q(E/x_{i})$. This together with the X-semantics of $S$ (cf. Definition 4.1.1) gives that $HL(T)\models_{X}\{p\}S\{q\}$.

Composition Rule: $S\equiv S_{1};S_{2}$ and $HL(T)\vdash\{p\}S\{q\}$. By the Composition Rule, there exists $r(\vec{x})\in L$ such that $HL(T)\vdash\{p\}S_{1}\{r\}$ and $HL(T)\vdash\{r\}S_{2}\{q\}$. By the induction hypothesis, it follows that $HL(T)\models_{X}\{p\}S_{1}\{r\}$ and $HL(T)\models_{X}\{r\}S_{2}\{q\}$. By the X-semantics of $S$ (cf. Definition 4.1.1), we have $HL(T)\models_{X}\{p\}S\{q\}$.

Conditional Rule: $S\equiv if\ B\ then\ S_{1}\ else\ S_{2}\ fi$ and $HL(T)\vdash\{p\}S\{q\}$. By the Conditional Rule, we have that $HL(T)\vdash\{p\wedge B\}S_{1}\{q\}$ and $HL(T)\vdash\{p\wedge\neg B\}S_{2}\{q\}$. By the induction hypothesis, it follows that $HL(T)\models_{X}\{p\wedge B\}S_{1}\{q\}$ and $HL(T)\models_{X}\{p\wedge\neg B\}S_{2}\{q\}$. By the X-semantics of $S$ (cf. Definition 4.1.1), we have $HL(T)\models_{X}\{p\}S\{q\}$.

Iteration Rule: $S\equiv while\ B\ do\ S_{0}\ od$ and $HL(T)\vdash\{p\}S\{q\}$. By the Iteration Rule, we have that $HL(T)\vdash\{p\wedge B\}S_{0}\{p\}$ and $q\equiv p\wedge\neg B$. By the induction hypothesis, it follows that $HL(T)\models_{X}\{p\wedge B\}S_{0}\{p\}$. Let $M\models T$. By Theorem 4.1.4, we have that $M\models p(\vec{x})\wedge B(\vec{x})\wedge\alpha_{S_{0}}(\vec{x},\vec{y})\rightarrow p(\vec{y}/\vec{x})$. Assuming that $M\models p(\vec{x})\wedge\alpha_{S}(\vec{x},\vec{y})$, by the X-semantics of $S$ (cf. Definition 4.1.1) and Theorem 4.1.4 there exist $i,$ $\vec{x_{0}}=\vec{x},$ $\vec{x_{1}},$ $\ldots,$ $\vec{x_{i}}=\vec{y}$ $\in$ $M$ with $M\models\forall j\leq i(\exists!\vec{z}\ \varphi_{S_{0}}(\vec{x},j,\vec{z})\wedge\varphi_{S_{0}}(\vec{x},j,\vec{x_{j}}))$ such that $M\models\forall j<i(B(\vec{x_{j}})\wedge\alpha_{S_{0}}(\vec{x_{j}},\vec{x_{j+1}}))\wedge\neg B(\vec{x_{i}})$, then by induction on $j$ up to $i$ it’s easy to see $M\models\forall j\leq i\ p(\vec{x_{j}}/\vec{x})$ and hence we have $M\models p(\vec{y}/\vec{x})\wedge\neg B(\vec{y}/\vec{x})$, so $M\models q(\vec{y}/\vec{x})$. Then $M\models p(\vec{x})\wedge\alpha_{S}(\vec{x},\vec{y})\rightarrow q(\vec{y}/\vec{x})$. By Theorem 4.1.4, it follows that $M\models_{X}\{p\}S\{q\}$. Since $M\models T$ is arbitrary, we have that $HL(T)\models_{X}\{p\}S\{q\}$.

Consequence Rule: $HL(T)\vdash\{p\}S\{q\}$. By the Consequence Rule, there exist $p_{1},q_{1}\in L$ such that $T\vdash p\rightarrow p_{1}$, $HL(T)\vdash\{p_{1}\}S\{q_{1}\}$ and $T\vdash q_{1}\rightarrow q$. By soundness of first-order logic, we have $T\models p\rightarrow p_{1}$ and $T\models q_{1}\rightarrow q$. By the induction hypothesis, it follows that $HL(T)\models_{X}\{p_{1}\}S\{q_{1}\}$. Then we have $HL(T)\models_{X}\{p\}S\{q\}$.

$(\Leftarrow)$. Suppose that $HL(T)\models_{X}\{p\}S\{q\}$. Then we have to prove that $HL(T)\vdash\{p\}S\{q\}$. The argument is by induction on the structure of $S$.

Assignment: $S\equiv x_{i}:=E$. Suppose that $HL(T)\models_{X}\{p\}S\{q\}$. By the X-semantics of $S$ (cf. Definition 4.1.1), we have that $T\models p\rightarrow q(E/x_{i})$. By completeness of first-order logic, it follows that $T\vdash p\rightarrow q(E/x_{i})$. By the Assignment Axiom Scheme, we have $HL(T)\vdash\{q(E/x_{i})\}S\{q\}$. By the Consequence Rule, it follows that $HL(T)\vdash\{p\}S\{q\}$.

Composition: $S\equiv S_{1};S_{2}$. Suppose that $HL(T)\models_{X}\{p\}S\{q\}$. By the Strongest Postcondition Lemma (cf. Lemma 5.1.4), we have that $HL(T)\models_{X}\{p\}S_{1}\{SP(p,S_{1})\}$ and $HL(T)\models_{X}\{SP(p,S_{1})\}S_{2}\{q\}$. Applying the induction hypothesis to $S_{1}$ and $S_{2}$ yields $HL(T)\vdash\{p\}S_{1}\{SP(p,S_{1})\}$ and $HL(T)\vdash\{SP(p,S_{1})\}S_{2}\{q\}$. By the Composition Rule, it follows that $HL(T)\vdash\{p\}S\{q\}$.

Conditional: $S\equiv if\ B\ then\ S_{1}\ else\ S_{2}\ fi$. Suppose that $HL(T)\models_{X}\{p\}S\{q\}$. By the X-semantics of $S$ (cf. Definition 4.1.1), we have that $HL(T)\models_{X}\{p\wedge B\}S_{1}\{q\}$ and $HL(T)\models_{X}\{p\wedge\neg B\}S_{2}\{q\}$. By the induction hypothesis applied to $S_{1}$ and $S_{2}$, it follows that $HL(T)\vdash\{p\wedge B\}S_{1}\{q\}$ and $HL(T)\vdash\{p\wedge\neg B\}S_{2}\{q\}$. By the Conditional Rule, we have $HL(T)\vdash\{p\}S\{q\}$.

Iteration: $S\equiv while\ B\ do\ S_{0}\ od$. Suppose that $HL(T)\models\{p\}S\{q\}$. By the Loop Invariant Lemma (cf. Lemma 5.1.6), it follows that $T\models p\rightarrow INV(p,S)$, $HL(T)\models_{X}\{INV(p,S)\wedge B\}S_{0}\{INV(p,S)\}$ and $T\models INV(p,S)\wedge\neg B\rightarrow q$. By completeness of first-order logic, we have that $T\vdash p\rightarrow INV(p,S)$ and $T\vdash INV(p,S)\wedge\neg B\rightarrow q$. Applying the induction hypothesis to $S_{0}$ yields $HL(T)\vdash\{INV(p,S)\wedge B\}S_{0}\{INV(p,S)\}$. By the Iteration Rule, it follows that $HL(T)\vdash\{INV(p,S)\}S\{INV(p,S)\wedge\neg B\}$. By the Consequence Rule, we have that $HL(T)\vdash\{p\}S\{q\}$.

This completes the proof. ∎

5.2 Reduction from $HL(T)$ to $T$

The reduction from $HL(T)$ to $T$ with $PA\subseteq T\subseteq Th(N)$ has been established by Bergstra and Tucker as the main theorem in [22], and is shown as follows.

Theorem 5.2.1**.**

Given an assertion $p\in L$ and program $S\in WP$ one can effectively calculate an assertion $SP(p,S)\in L$ such that

(1) $SP(p,S)$ defines the strongest postcondition of $S$ relative to $p$ on the set of states over $N$;

(2) $HL(PA)\vdash\{p\}S\{SP(p,S)\}$;

And, for any refinement $T$ of Peano arithmetic, including $PA$ itself,

(3) $HL(T)\vdash\{p\}S\{q\}$ if and only if $T\vdash SP(p,S)\rightarrow q$.

In Theorem 5.2.1, statement (1) explains the meaning of $SP(p,S)$ in $N$; statement (2) is a preliminary result for statement (3), and it can be taken as a special case of (3) with $SP(p,S)$ in place of $q$; (3) is the core, and it establishes the reduction from $HL(T)$ to $T$ by using $SP(p,S)$.

The main results having been developed in this paper can be used to derive the above theorem:

Proof of Theorem 5.2.1.

By Theorem 4.1.4 and Proposition 4.2.2, it follows that for any $\vec{n},\vec{m}\in N$, $f_{S}^{N}(\vec{n})=\vec{m}$ iff $N\models\alpha_{S}(\vec{n},\vec{m})$. The formal strongest postcondition $SP(p,S)$, here, can be defined by $SP(p,S)(\vec{x})::=\exists\vec{u}(p(\vec{u}/\vec{x})\wedge\alpha_{S}(\vec{u}/\vec{x},\vec{x}/\vec{y}))$. Then statement (1) of Theorem 5.2.1 follows. To prove Theorem 5.2.1, it remains to prove statement (3). Let $PA\subseteq T\subseteq Th(N)$, $p,q\in L$, and $S\in WP$. Consider $HL(T)\vdash\{p\}S\{q\}$ as follows: by Theorem 5.1.8, it is equivalent to $HL(T)\models_{X}\{p\}S\{q\}$; by Theorem 4.1.4, it is equivalent to $T\models p(\vec{x})\wedge\alpha_{S}(\vec{x},\vec{y})\rightarrow q(\vec{y}/\vec{x})$; by definition of $SP(p,S)$, it is equivalent to $T\models SP(p,S)\rightarrow q$; by soundness and completeness of first-order logic, it is equivalent to $T\vdash SP(p,S)\rightarrow q$. ∎

Observing the axiom system of $HL(T)$, we remark that the crucial and perhaps the most difficult step of finding a proof of $\{p\}S\{q\}$ in $HL(T)$ is to guess the corresponding intermediate assertions when applying the Composition and Iteration Rules. As Lemmas 5.1.4, 5.1.6 and the proof of Theorem 5.1.8 show, the intermediate assertions involved in this proof can be easily constructed, and their roles in guaranteeing the correctness of Theorem 5.2.1 are implicit. The real strength of Theorem 5.2.1 is due to the fact that it provides us a readily-operating means to deciding whether $\{p\}S\{q\}$ is provable in $HL(T)$: one simply needs to decide whether $SP(p,S)\rightarrow q$ is provable in $T$.

5.3 Comparison with Floyd logic

This Subsection is considered as a continuation to Subsection 4.3. The following definitions concerning Floyd logic come from [10, p165-166].

Let $PA\subseteq T\subseteq Th(N)$, $M\models T$, $P::=<(i_{0}:u_{0}),...,(i_{n}:u_{n})>$ and $\psi\in L$.

The dynamic formula $\Box(P,\psi)$ is said to be valid in $M$ w.r.t. continuous traces if ($\ast$) below holds.

($\ast$) For any continuous trace $<\vec{s_{a}}>_{a\in M}$ of $P$ in $M$ and for any $a\in M,\vec{s_{a}}(\lambda)\not\in\{i_{m}:m\leq n\}$ implies $M\models\psi[\vec{s_{a}}].$

$M\models\Box(P,\psi)$ denotes that $\Box(P,\psi)$ is valid in $M$ w.r.t continuous traces; $T\models\Box(P,\psi)$ denotes that for every $M\models T$, $M\models\Box(P,\psi)$.

The Floyd logic serves to derive statements $\Box(P,\psi)$ from $T$. The set $lab(P)$ of labels of $P$ is defined as follows:

[TABLE]

A Floyd derivation of $\Box(P,\psi)$ from $T$ consists of: a mapping $\Phi:lab(P)\rightarrow L$ together with the classical first-order derivations listed in (i)-(iv) below. Notation: When $z\in lab(P)$ we write $\Phi_{z}$ instead of $\Phi(z)$.

(i) A derivation: $T\vdash\Phi_{i_{0}}$.

(ii) To each command $i_{m}:x_{j}\hookleftarrow E$ occurring in $P$, a derivation: $T\vdash\Phi_{i_{m}}\rightarrow\Phi_{i_{m+1}}(E/x_{j})$.

(iii) To each command $i_{m}:if\ B\ goto\ v$ occurring in $P$, two derivations: $T\vdash(B\land\Phi_{i_{m}})\rightarrow\Phi_{v}$ and $T\vdash(\lnot B\land\Phi_{i_{m}})\rightarrow\Phi_{i_{m+1}}$.

(iv) To each $z\in(lab(P)-\{i_{m}:m\leq n\})$, a derivation: $T\vdash\Phi_{z}\rightarrow\psi$.

Now the existence of a Floyd derivation of $\Box(P,\psi)$ from $T$ is denoted by $T\vdash\Box(P,\psi)$. The soundness and completeness of Floyd logic relative to $T$ has been established by H. Andréka, et.al., as the main theorem in [10], and is shown as follows.

Theorem 5.3.1** (Soundness and completeness of Floyd logic).**

Let $PA\subseteq T\subseteq Th(N)$. For every labeled program $P$, and every $\psi\in L$, it is the case that $T\vdash\Box(P,\psi)$ iff $T\models\Box(P,\psi)$.

To build the relationship of Hoare logic with Floyd logic, we remark that for each $S\in WP$, there is a labeled program $P$ such that the X-semantics of $S$ is equivalent to the semantics of $P$ in $PA$, and vice versa.

Theorem 5.3.2**.**

Let $PA\subseteq T\subseteq Th(N)$. For every $S\in WP$, every labeled program $P$, and every $q\in L$, if the X-semantics of $S$ is equivalent to the semantics of $P$ in $PA$, then it is the case that $HL(T)\vdash\{true\}S\{q\}$ iff $T\vdash\Box(P,q)$.

Proof.

Immediate from Theorems 5.1.8 and 5.3.1. ∎

Intuitively Hoare logic can be thought of as a special first-order multi-modal logic with programs viewed as modalities; and the axiom system of Floyd logic looks more like a first-order logical system. Although these two axiom systems appear different, they are essentially the same first-order logical system, as Theorems 5.3.2 and 5.2.1 show.

6 The X-semantics revisited

6.1 Comparison with the axiomatic semantics

The axiomatic semantics of while-programs is a relational semantics determined by Hoare logic. The following definition is as in [22, p303] except that the side effects on non-program variables are explicitly ruled out.

Definition 6.1.1**.**

Let $L^{\prime}$ be a first-order logical language, let $WP^{\prime}$ be the set of while-programs based on $L^{\prime}$, and let $T$ be a first-order theory of $L^{\prime}$. For any $S\in WP^{\prime}$ with program variables $\vec{x}$, the axiomatic semantics $AX(T)_{M}(S)$ of $S$ in a model $M$ of $T$ is a binary relation on the set $V$ of assignments over $M$ defined as follows:

[TABLE]

Observe from the above definition that $AX(T)_{M}(S)$ is the maximal input-output relation for $S$ over $M$ such that $HL(T)$ is sound in $M$ with respect to all the specifications of $S$. Although this definition of axiomatic semantics appears mathematically elegant, it is too abstract, and the general properties of its are not always nice, e.g. nondeterminism. (For more details, the reader refers to [22].) Surprisingly, when restricting the first-order theory $T$ to $PA\subseteq T\subseteq Th(N)$, the axiomatic semantics is exactly what we pursue in this paper.

Theorem 6.1.2**.**

Let $PA\subseteq T\subseteq Th(N)$. For every $M\models T$, and every $S\in WP$, $AX(T)_{M}(S)=A_{S}^{M}$.

Proof.

Let $M\models T$, let $V$ be the set of assignments over $M$, and let $S\in WP$ with program variables $\vec{x}$. To prove $AX(T)_{M}(S)=A_{S}^{M}$, it suffices to prove that $AX(T)_{M}(S)\supseteq A_{S}^{M}$ and $AX(T)_{M}(S)\subseteq A_{S}^{M}$.

$(\supseteq)$. Let $(\sigma,\tau)\in A_{S}^{M}$. By Definition 4.1.1, it’s easy to see that $\textbf{A}y\not\in\vec{x}(\sigma(y)=\tau(y))$. To prove $(\sigma,\tau)\in AX(T)_{M}(S)$, by Definition 6.1.1, it suffices to prove that $\textbf{A}p,q\in L,v\in V(HL(T)\vdash\{p\}S\{q\}\ \&\ M,v(\sigma(\vec{x})/\vec{x})\models p\Rightarrow M,v(\tau(\vec{x})/\vec{x})\models q)$. Let $p,q\in L$ and $v\in V$ with $HL(T)\vdash\{p\}S\{q\}$ and $M,v(\sigma(\vec{x})/\vec{x})\models p$. It remains to show that $M,v(\tau(\vec{x})/\vec{x})\models q$. By soundness of $HL(T)$ w.r.t. the X-semantics (cf. Theorem 5.1.8), it follows that $HL(T)\models_{X}\{p\}S\{q\}$. Then we have $M\models_{X}\{p\}S\{q\}$. From the premise $(\sigma,\tau)\in A_{S}^{M}$, by Definition 4.1.1, it follows that $(v(\sigma(\vec{x})/\vec{x}),v(\tau(\vec{x})/\vec{x}))\in A_{S}^{M}$. Since $M,v(\sigma(\vec{x})/\vec{x})\models p$, we have that $M,v(\tau(\vec{x})/\vec{x})\models q$.

$(\subseteq)$. Let $(\sigma,\tau)\in AX(T)_{M}(S)$. Let $p(\vec{u},\vec{x})::=\vec{u}=\vec{x}$, $q(\vec{u},\vec{x})::=\alpha_{S}(\vec{u},\vec{x})$, and $v::=\sigma(\sigma(\vec{x})/\vec{u})$, where $\vec{u}$ is disjoint from $\vec{x}$. Then we have $T\models p(\vec{u},\vec{x})\wedge\alpha_{S}(\vec{x},\vec{y})\rightarrow q(\vec{u},\vec{y})$. By Theorem 4.1.4, it follows that $HL(T)\models_{X}\{p\}S\{q\}$. Using completeness of $HL(T)$ w.r.t. the X-semantics (cf. Theorem 5.1.8), we have that $HL(T)\vdash\{p\}S\{q\}$. By definitions of $v$ and $p$, we have that $M,v(\sigma(\vec{x})/\vec{x})\models p$. By the definition of $AX(T)_{M}(S)$ (cf. Definition 6.1.1), it follows that $\textbf{A}y\not\in\vec{x}(\sigma(y)=\tau(y))$ and $M,v(\tau(\vec{x})/\vec{x})\models q$. By definitions of $v$ and $q$, we have $M\models\alpha_{S}(\sigma(\vec{x}),\tau(\vec{x}))$. By Theorem 4.1.4, it follows that $(\sigma,\tau)\in A_{S}^{M}$. ∎

Observe from the foregoing theorem that the axiomatic semantics of while-programs on every model of $T$ with $PA\subseteq T\subseteq Th(N)$ is independent of the choice of $T$. It has been justified by the Uniqueness Theorem [22, p304] that in a general setting, the axiomatic semantics of while-programs on a structure $M$ of a first-order theory $T$ is independent of the choice of $T$. We can now say that for any $M\models PA$, the axiomatic semantics of while-programs on $M$ coincides with the X-semantics of while-programs on $M$.

6.2 Usefulness of nonstandard semantics in Hoare logic

Properties of nonstandard models are sometimes very useful to decide whether a Hoare’s triple is provable, especially when such a triple is true in the standard model. Let $PA\subseteq T\subseteq Th(N)$, $p,q\in L$, and $S\in WP$. Suppose that $N\models_{S}\{p\}S\{q\}$ (or equivalently $N\models_{X}\{p\}S\{q\}$) and $HL(T)\not\vdash\{p\}S\{q\}$. Then, by Theorem 5.1.8, there should be a nonstandard $M\models T$ such that $M\not\models_{X}\{p\}S\{q\}$. This means that the X-semantics of while-programs in $M$ could be useful in deciding whether $\{p\}S\{q\}$ is provable in $HL(T)$. To show the usefulness of nonstandard semantics in Hoare logic, the following example is illustrated.

Theorem 6.2.1** (Cf. [16, Theorem 4.3]).**

Let $S::=y:=0;while\ y<x\ do\ y:=y+1\ od$, let $T\supseteq PA$ such that $Thm(T)\subsetneqq Th(N)$, and let $\varphi(x)\in L$ such that $T\vdash\varphi(n)$ for each $n\in N$ and $T\nvdash\forall x\ \varphi(x)$ (There always exists such a $\varphi$ for any such $T$). It is the case that $HL(T)\models_{S}\{\neg\varphi(x)\}S\{false\}$ but $HL(T)\nvdash\{\neg\varphi(x)\}S\{false\}$.

Theorem 6.2.1 shows the incompleteness of $HL(T)$ with $T\supseteq PA$ and $Thm(T)\subsetneqq Th(N)$ w.r.t. the standard semantics. The original proof of Theorem 6.2.1 in [16, the proof of Theorem 4.3] exploits the proof concept of $HL(T)$ to derive a contradiction, yet it seems to be cumbersome. Using the X-semantics of while-programs, a concise proof of Theorem 6.2.1 is shown below.

Proof of Theorem 6.2.1.

Let $S$, $T$ and $\varphi(x)$ be as defined in Theorem 6.2.1. It’s trivial that $HL(T)\models_{S}\{\neg\varphi(x)\}S\{false\}$. Thus it remains to prove $HL(T)\nvdash\{\neg\varphi(x)\}S\{false\}$. Since $N\models_{X}\{\neg\varphi(x)\}S\{false\}$, by Theorem 5.1.8, it suffices to prove that for some nonstandard $M\models T$, $M\not\models_{X}\{\neg\varphi(x)\}S\{false\}$. By the definition of $\varphi(x)$, together with completeness of first-order logic, it follows that there exists a nonstandard $M\models T$ such that $M\models\exists x\ \neg\varphi(x)$. Let $M$ be such a model. By Example 4.2.1, we have that for any $x,y\in M$, $g_{S}^{M}(x,y)=(x,x)$. Then $M\not\models_{X}\{\neg\varphi(x)\}S\{false\}$ follows. ∎

7 Remarks on the completeness issues

The most popular completeness form we have known for Hoare logic is the relative completeness (for a complete knowledge of relative completeness, the reader refers to the distinguished survey article [1]):

Let $L^{\prime}$ be a first-order logical language, and let $M$ be a model of $L^{\prime}$. Hoare logic is complete for while-programs relative to $M$ iff for all asserted programs $\Phi$, if $M\models_{H}\Phi$, then $Th(M)\vdash_{H}\Phi$, where $\models_{H}$ and $\vdash_{H}$ denote the satisfaction and derivation relations of Hoare logic.

Cook [23] considered the relative completeness of Hoare logic with the expressiveness condition (for the incompleteness due to inexpressiveness, and the completeness with inexpressiveness, the reader refers to [24] and [25] respectively):

Let $L^{\prime}$ and $M$ be as defined above. If $L^{\prime}$ is expressive for while-programs relative to $M$ (i.e., for all assertions $p\in L^{\prime}$ and all while-programs $W$ based on $L^{\prime}$, there exists an assertion $q\in L^{\prime}$ that defines the strongest postcondition of $W$ relative to $p$ on the set of assignments over $M$), then Hoare logic is complete for while-programs relative to $M$.

Unfortunately, there are only two kinds of expressive structures for while-programs w.r.t. the standard semantics: the standard model $N$ and finite structures [26]. In contrast, as Theorem 4.1.4 and Lemmas 5.1.4, 5.1.6 imply, $L$ is expressive for while-programs w.r.t. the X-semantics relative to every model of $PA$, so the new semantics of Hoare logic extends the applicability of Cook’s completeness theorem from $N$ to nonstandard models of $PA$. Except for the paucity of expressive structures, the relative completeness of Hoare logic has a theoretical weakness that we can’t come to terms with: for each expressive structure $M$ it has to pick out the complete theory $Th(M)$ as the specification axioms to derive the whole set of true asserted programs in $M$. Consider for example the case $M\equiv N$. Let $T\supseteq PA$ with $Thm(T)\subsetneqq Th(N)$. Then there exists a sentence $p\in L$ such that $N\models p$ and $T\nvdash p$. It’s easy to see that $N\models_{S}\{true\}x:=x\{p\}$ (or equivalently $N\models_{X}\{true\}x:=x\{p\}$) and $HL(T)\nvdash\{true\}x:=x\{p\}$ (by the choice of $p$ and completeness of first-order logic, there exists $M\models T$ such that $M\nvDash p$; then we have $HL(T)\nvDash_{X}\{true\}x:=x\{p\}$; by completeness of $HL(T)$ w.r.t. the X-semantics, it follows that $HL(T)\nvdash\{true\}x:=x\{p\}$). From the above analysis, we achieve that $Th(N)$ is the only extension $T$ of $PA$ such that $HL(T)$ is complete relative to $N$ w.r.t. both the standard semantics and the X-semantics. However, by Gödel’s incompleteness theorem, $Th(N)$ is not recursively enumerable (even not arithmetical [17, Lemma 17.3]), which means that it is far beyond the power of any mechanical device to enumerate the elements of $Th(N)$. To fix up this drawback, we have studied the completeness issues of Hoare logic relative to $N$ by restricting assertions to subclasses of arithmetical formulas [27] (and by restricting inputs to $N$ [28]): arithmetical extensions of $PA$ suffice to act as the assertion theory, and the lower the level of the assertions in the arithmetical hierarchy the lower the level of the required assertion theory is.

Historically, logical completeness of the first-order Hoare logic, which as an important completeness form stems from completeness of first-order logic, was studied extensively:

Let $L^{\prime}$ be a first-order logical language, and let $T$ be a first-order theory of $L^{\prime}$. Hoare logic is complete for while-programs relative to $T$ iff for all asserted programs $\Phi$, if $T\models_{H}\Phi$, then $T\vdash_{H}\Phi$, where $T\models_{H}\Phi$ denotes that for any $M\models T$, $M\models_{H}\Phi$.

Bergstra and Tucker [25] have pointed out that $Th(N)$ is the unique extension $T$ of $PA$ for which $HL(T)$ is logically complete w.r.t. the standard semantics. (The incompleteness of $HL(T)$ with $T\supseteq PA$ and $Thm(T)\subsetneqq Th(N)$ w.r.t. the standard semantics has been shown in Theorem 6.2.1.) To remedy this unsatisfying completeness result, we have investigated the logical completeness of Hoare logic with inputs over the standard model [29]: a particular extension $PA^{+}$ of $PA$ suffices to prove all valid Hoare’s triples requiring that the input has a standard value; moreover $PA^{+}$ is shown to be minimal with the property. To see the essential difference of the completeness theorem of Bergstra and Tucker from that presented in this paper, we remark that the only factor leading to the difference is the semantics. Let $T\supseteq PA$ with $Thm(T)\subsetneqq Th(N)$. By Propositions 4.2.2 and 4.2.3, for any $M\models T$, and any $S\in WP$, we have that $R_{S}^{M}$ is a (sometimes proper) subset of $A_{S}^{M}$. By the semantics of Hoare logic, it follows that $\{\{p\}S\{q\}:p,q\in L,S\in WP,HL(T)\models_{X}\{p\}S\{q\}\}$ is properly contained in $\{\{p\}S\{q\}:p,q\in L,S\in WP,HL(T)\models_{S}\{p\}S\{q\}\}$. As is shown in Subsection 6.1, the X-semantics of while-programs is an axiomatic semantics, which means that for any $M\models PA$ and any $S\in WP$, $A_{S}^{M}$ is the maximal input-output relation for $S$ over $M$ such that $HL(T)$ is sound in $M$ with respect to all the specifications of $S$ (in contrast, $R_{S}^{M}$ is not always maximal in this sense). Hence among all the semantics of while-programs that make $HL(T)$ sound in every model of $T$ (including the standard semantics), the axiomatic semantics makes the set $\{\{p\}S\{q\}:p,q\in L,S\in WP,HL(T)\models_{X}\{p\}S\{q\}\}$ be minimal and naturally coincide with the set $\{\{p\}S\{q\}:p,q\in L,S\in WP,HL(T)\vdash\{p\}S\{q\}\}$. Furthermore, Bergstra and Tucker established the logical completeness of Hoare logic based on the axiomatic semantics in a general setting [16].

The Hungary School [8, 9, 10] provides an alternative approach to characterizing the maximal semantics of programs for which Floyd logic is sound, i.e. the Hungary semantics, and shows that Floyd logic is logically complete w.r.t. this semantics. In Subsections 4.3 and 5.3, a detailed comparison of this technique with that presented in this paper has been given. Csirmaz [11], and Hortalá-González et.al. [13] extended this technique into a general situation. For the relationship of the general Floyd logic with weak second order logic, the reader refers to the literature [15]. Moreover, Andréka et.al. [12], and Pasztor [14] used many-sorted logic (i.e. Henkin semantics [30]) to define Floyd-Hoare logic, thus obtaining the completeness of Floyd-Hoare logic immediately from that of many-sorted logic.

Kozen and Tiuryn [31] viewed Hoare logic as a special propositional modal logic by abstracting assertions and programs to propositional symbols, and gained the completeness of this propositional Hoare logic.

8 Conclusion

In this paper, for nonstandard models $M$ of $PA$, we have introduced the concept of $M$-finiteness as the desired finiteness as far as $M$ is concerned; we have exhibited an explicit axiomatic semantics for while-programs in nonstandard models of $PA$, and proven that it coincides with the Hungary semantics; based on this semantics, we have defined a new semantics of Hoare logic, and shown the soundness and completeness of its axiom system w.r.t. the new semantics; various comparisons have shown that our approach is not only mathematically elegant, but also practically useful.

Acknowledgement

The authors would like to thank the 973 Program of China (Grant No. 2014CB340701), the National Natural Science Foundation of China (Grant Nos. 61672504 and 61472474), and the CAS-SAFEA International Partnership Program for Creative Research Teams for the financial support. The authors would also like to thank the anonymous referees for their valuable suggestions and comments that helped improving this paper.