## `boolean ≝ {true, false}ᵀ` Rather than being a specialized type, `boolean` is simply the name given to the enumeration of the special atoms `true` and `false`: `{true, false}ᵀ`. These atoms are defined and exported by the virtual machine for use by programmers. Every primitive interrogative method, such as `"_=_"` or `"_≤_"`, uses classical (Boolean) bivalence, and every stable primitive interrogative obeys the three classical (Aristotelian) laws of thought.

Bivalent logic assigns either `true` or `false` as the unique truth value of every proposition. A primitive interrogative method is stable iff it reliably answers either `true` or `false` for a given set of arguments.

The classical laws of thought are:

• The law of identity, that every proposition `P` implies itself: `P → P`. For every stable primitive interrogative method `"prim_,_"`, then `∀A,B : (prim A, B = prim A, B) = true`.
• The law of noncontradiction, that both a proposition `P` and its negation `¬P` are not mutually true: `¬(P ∧ ¬P)`. For every stable primitive interrogative method `"prim_,_"`, then `∀A,B : (prim A, B ∧ ¬prim A, B) = false`.
• The law of excluded middle, that either a proposition `P` or its negation `¬P` is uniquely true: `P ∨ ¬P`. For every primitive interrogative method `"prim_,_"`, then `∀A,B : ((prim A, B = true) ∨ (prim A, B = false)) = true`.

Remember that values may be instances of many types. This means that Avail directly supports other logical systems, such as Kleene's three-valued logic of indeterminacy, whose truth values are `true`, `false`, and `unknown`. Assuming the introduction of an atom to represent `unknown`, then `kleenean ≝ {true, false, unknown}ᵀ`. Clearly `kleenean` is a supertype of `boolean`, since `{true, false, unknown}ᵀ ⊇ {true, false}ᵀ`. New logical operations could be written in terms of `kleenean`, and preexisting logical operations defined to accept `boolean`s would automatically become specializations of these more general operations defined to accept `kleenean`s.

/* A proof that boolean is merely a type comprising only true and false: */ Assert: boolean = {true, false}ᵀ; /* Introduce an atom named "unknown" into the current module's context. */ "unknown" is a new atom; /* Define the "kleenean" type; boolean ∪ (unknown's type) would also have * worked. */ kleenean ::= {true, false, unknown}ᵀ; Assert: boolean ⊆ kleenean; /* Define a method "truth index of_" that accepts a Kleenean truth value and * answers an appropriate index into one of the truth tables below. */ Abstract method "truth index of_" is [kleenean]→[1..3]; Method "truth index of_" is [p : true's type | 1]; Method "truth index of_" is [p : unknown's type | 2]; Method "truth index of_" is [p : false's type | 3]; /* * In each of the truth tables, whether the subscript applies to a row or a * column, a subscript of 1 means "true", 2 means "unknown", and 3 means * "false". */ notTable ::= <false, unknown, true>; andTable ::= < <true, unknown, false>, <unknown, unknown, false>, <false, false, false> >; orTable ::= < <true, true, true>, <true, unknown, unknown>, <true, unknown, false> >; /* * And here are the logical operators themselves. */ /* Kleenean NOT. */ Method "¬_" is [ a : kleenean | notTable[truth index of a] ] : kleenean; /* Kleenean AND. */ Method "_∧_" is [ a : kleenean, b : kleenean | andTable[truth index of a][truth index of b] ] : kleenean; /* Kleenean OR. */ Method "_∨_" is [ a : kleenean, b : kleenean | orTable[truth index of a][truth index of b] ] : kleenean; /* The first assertion invokes the boolean versions of "¬_" and "_∧_", but the * second one invokes the kleenean version of "_∨_". So booleans and kleeneans * interoperate nicely. */ p : boolean := true; q : kleenean := unknown; Assert: (p ∧ false) = false; Assert: (p ∨ q) = true;
 ‹ `atom` | Return to Type System | `object` ›