Theorem 15 (Soundness of H) Γ 'H C implies Γt =AX Ct
Proof. We need to check that axioms and rules of the Hoare-Gentzen Calculus
continue to hold if we replace every 'H by =AX and every asserted program
C by its translation Ct. For example, Composition is translated to:
Γ1 ∀ij((Fιt(i) ∧ Pιt(hi, ji)) → F))
Γ2 ∀ij((F2(i) ∧ P'i)) → F))
Γ1, Γ2 =aχ ∀ij ((Ft(i) ∧∃k(P1t(hi,⅛i) ∧ P2t(hMi))) → F3t(j))
This is easily seen to be valid on the force of predicate logic alone. Similarly,
the structural rules, the Test axiom, Choice and Consequence lead to trans-
lations whose validity is easily verified. The soundness of the Recursion rule
follows almost directly from Scott Induction.
This leaves it for us to verify the soundness of the Assignment axiom. We
must check that
=AX ∀ij((([N∕xk]F )t (i) ∧ i[S k(0)]j ∧ V (Sk (0))(j) = N t(i)) → F t(j))
Using Lemma 4 and the notation that was defined in that lemma, we find
that this is equivalent with
=AX ∀ij ((([N/xk ]F )i ∧ i[Sk (0)]j ∧ V (Sk (0))(j) = Ni) → Fj)
Letting F0 be the result of substituting V(Sn (0))(i) for xn in F, for each
n 6= k , we see that the latter is equivalent with
=AX ∀ij ((([N i/xk ]F0) ∧ i[Sk (0)] j ∧ V (Sk (0))(j) = Ni) → Fj)
in its turn. But this last statement is easily seen to hold on the basis of the
definition of i[Sk(0)]j. □
9 The Union Theorem
The main theorem of this section, and indeed of the paper, is Theorem 23
below, which states that the meaning of a program is equal to the union of
the meanings of all linear programs deriving it. Before we prove the theorem
itself, it will be expedient to consider a series of lemmas and a proposition.
The lemma and the proposition below establish the soundness of the calculus
C and are therefore of interest in themselves.
26
More intriguing information
1. The name is absent2. The name is absent
3. Population ageing, taxation, pensions and health costs, CHERE Working Paper 2007/10
4. The name is absent
5. Restructuring of industrial economies in countries in transition: Experience of Ukraine
6. THE EFFECT OF MARKETING COOPERATIVES ON COST-REDUCING PROCESS INNOVATION ACTIVITY
7. Labour Market Flexibility and Regional Unemployment Rate Dynamics: Spain (1980-1995)
8. The name is absent
9. Review of “The Hesitant Hand: Taming Self-Interest in the History of Economic Ideas”
10. Revisiting The Bell Curve Debate Regarding the Effects of Cognitive Ability on Wages