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 threevalued 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.
‹ atom 
  Return to Type System    object › 