Nondeterministic three-valued logic: isotonic and guarded truth-functions (Q792750)

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.