Part III - Metatheory
Published online by Cambridge University Press: 06 January 2010
Summary
Part III initiates the study of a few issues concerned with the first-order theory of Boolean categories. “Formulas” are summands expressible in the language PBC of Boolean categories introduced in Section 11. The fundamental completeness theorem 11.15 asserts that a formula is universally valid if and only if it is true in the classical example of Mfn. A similar result holds for ranged Boolean categories. Using a completion by ideals developed in Section 13, the forward predicate transformers are seen to be categorically dual to the inverse ones, at least in the preadditive case. Section 14 provides the equational theory for 3-valued if-then-else in a Boolean category.
- Type
- Chapter
- Information
- Predicate Transformer Semantics , pp. 146Publisher: Cambridge University PressPrint publication year: 1992