In this chapter, we define and analyze the four basic logical operations: the unary “not”, or complement, and the binary “and”, “inclusive or” and “exclusive or”. These are commonly known as bit-wise operations, as each one may be computed by performing a certain computation on each bit of its argument (in the unary case) or each pair of corresponding bits of its arguments (for binary operations). For example, the logical “and” of bit vectors and may be specified in a bit-wise manner as the bit vector such that for all , iff .
In the context of our formalization, however, the logical operations are more naturally defined as arithmetic functions: the complement is constructed as an arithmetic difference and the binary operations are defined by recursive formulas, which facilitate inductive proofs of their relevant properties. Among these are the bit-wise characterizations, as represented by Lemmas 3.1.14 and 3.2.5.