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 booleans would automatically become specializations of these more general operations defined to accept kleeneans.