Go backward to Predicates as Actions
Go up to Top
Go forward to Rigid Variables and Quantifiers

Validity and Provability

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$ )
Formula F is provable (|- F)
- Formal derivation by rules of logic.
Soundness of the logic.
- Every provable formula is valid.
- |- $F$ $=>$ |= $F$ .

Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine