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 in St:
- |= forall in St:
- True regardless of what values are substituted for primed and unprimed
- ( in Nat) ( )
- Formula is provable (|- )
- Formal derivation by rules of logic.
- Soundness of the logic.
- Every provable formula is valid.
- |- |= .
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine