Strongly cantorian domains are supported in two ways by Watson.
The explicit support for strongly Cantorian domains is bound up with the properties of the built-in operator :, which signals the application of a retraction with strongly Cantorian range. A predeclared axiom TYPES: (?t:?t:?x) = ?t:?x ensures that type labels have the effect of retractions. The stratification facility will raise and lower the relative type of the right subterm of a term of the form ?t:?x as needed to stratify the context. It is not the case that all relative type information from such a subterm is suppressed: the difference between the relative types of two bound variables may be determined by information internal to such a term, and will cause a stratification error if it conflicts with other information derived in attempting to stratify the term.
Implicit support for strongly Cantorian domains is provided by the ``scin/scout'' features of the prover. An operator may be declared ``scout'' (for ``strongly Cantorian output'') if a theorem has been proved to the effect that the output of the operator will belong to a fixed strongly Cantorian domain. Similarly, an operator may be declared ``scin'' (for ``strongly Cantorian input'') if a theorem has been proved to the effect that all of its (one or two) inputs will belong to fixed strongly Cantorian domains. A term which is scout will have its type raised or lowered if necessary for purposes of stratification; a term which is scin will have the type(s) of its immediate subterms raised or lowered (independently of one another if there are two of them) if necessary for purposes of stratification. Functions may also be declared scin or scout.
These two features together greatly reduce the rigidity of the stratification criterion of Watson; in particular, the declaration of the propositional connectives and quantifiers as scin or scout as appropriate enables the fluent handling of first-order logic (avoiding stratification difficulties illustrated in an example above).