Go backward to Predicates as ActionsGo up to TopGo forward to Rigid Variables and Quantifiers |

- Action
`A`is valid (|=`A`)- Every step is an
`A`step. - |=
`A`*<=>**forall**s,t*in**St**:*s*[[`A`]]*t* - |=
*P**<=>**forall**s*in**St**:*s*[[*P*]] - True regardless of what values are substituted for primed and unprimed variables.
- (
*x'+y*in**Nat**)*=>*(*2(x'+y)**>=**x'+y*)

- Every step is an
- Formula
*F*is provable (|-*F*)- Formal derivation by rules of logic.

- Soundness of the logic.
- Every provable formula is valid.
- |-
*F**=>*|=*F*.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998