Soundness Proofs for Rules - LS-Lab/KeYmaeraX-release GitHub Wiki

To show that a proof rule is sound, we assume that all the premisses are valid (true in every state), and then show that the conclusion is valid (true in every state). This is subtly different from showing that an axiom is sound. Consider the rule G:

P
---- G
[a]P

Theorem (G is sound): Assume P is valid for some formula P, i.e. for all states omega, omega |= P. Want to show that [a]P is valid, or equivalently, for all states nu, mu if (nu,mu) in [a](/LS-Lab/KeYmaeraX-release/wiki/a) then mu |= P. But by assumption omega |= P for all omega so we can just pick omega = mu, regardless of the fact (nu,mu) in [a](/LS-Lab/KeYmaeraX-release/wiki/a), which completes the proof.

For this rule it is essential that P was true in every state, because we need to know it was true in some state mu that was different from the start state omega. Compare this with the similar-looking axiom, called V:

p ->[a]p

In this case we are saying that if p is true specifically in the start state for a then it is true in the end state as well. This axiom is only sound if a does not modify any of the variables that appear in p. In contrast, the rule G is sound all the time.

For a more involved example of the structure for rule soundness proofs, consider the rule for loop induction (where G is a context of assumptions and D is a context of conclusions):

G |- J, D     J |- [a]J    J |- P
---------------------------------
G |- [a*]P, D

Proof of soundness: Assume:

  1. For all states omega, omega |= (G |- J, D), (where omega |= (G |- D) is notation for "if omega |= F for all formulas F in G, then omega |= F for at least one F in D").
  2. For all states omega, omega |= (J |- [a]J)
  3. For all states omega, omega |= (J |- P)

Now show omega |= (G |- [a*]P, D) for all omega. So fix some arbitrary omega and

  1. assume \omega |= && G (the conjunction of all formulas in G).

Then by (1) either (a) omega |= J or (b) omega |= || D (the disjunction of formulas in D).

  • Case (b): (omega |= (|| D)) then we're done because we have shown omega |= (G |- D) and thus omega |= (G |- [a*]P,D).

  • Case (a): We now know (5) J holds initially (omega |= J) and want to show [a*]P, i.e. for all nu if (omega,nu) in [a*](/LS-Lab/KeYmaeraX-release/wiki/a*) then nu |= P. Then pick arbitrary nu in [a*](/LS-Lab/KeYmaeraX-release/wiki/a*). Recall [a*](/LS-Lab/KeYmaeraX-release/wiki/a*) = Union_{i in N} [a^i](/LS-Lab/KeYmaeraX-release/wiki/a^i), so induct on i.

    • Case i = 0: then [a^0](/LS-Lab/KeYmaeraX-release/wiki/a^0) = {(mu,mu) | mu in S} so suffices to show omega |= J which is true by (5).
    • Case i = k + 1:
      • IH: For all (nu,mu) in [a^k](/LS-Lab/KeYmaeraX-release/wiki/a^k) if nu |= J then mu |= J
      • Show for all mu if (nu,mu) in [a^i](/LS-Lab/KeYmaeraX-release/wiki/a^i) if nu |= J then mu |= J
      • Proof: Since (nu,mu) in [a^i](/LS-Lab/KeYmaeraX-release/wiki/a^i) then (nu,mu) in [a^k+1](/LS-Lab/KeYmaeraX-release/wiki/a^k+1) so by definition, exists mu' where (nu, mu') in [a](/LS-Lab/KeYmaeraX-release/wiki/a) and (mu', mu) in [a^k](/LS-Lab/KeYmaeraX-release/wiki/a^k). Since nu |= J then by (2) mu' |= J and by IH mu |= J, which completes the case and also the proof.