Nondeterministic three-valued logic: Isotonic and guarded truth-functions

Nondeterministic programs occurring in recently developed programming languages define nondeterminate partial functions. Formulas (Boolean expressions) of such nondeterministic languages are interpreted by a nonempty subset of {T (“true”), F (“false”), U (“undefined)}. As a semantic basis for the propositional part of a corresponding nondeterministic three-valued logic we study the notion of a truth-function over {T, F, U} which is computable by a nondeterministic evaluation procedure. The main result is that these truth-functions are precisely the functions satisfying four basic properties, called ( subseteq ) -isotonic, ( subseteq ) ^?-isotonic, hereditarily guarded, and hereditarily guard-using, and that a function satisfies these properties iff it is explicitly definable (in a certain normal form) from “if..then..else..fi”, binary choice, and constants.