information:classification, structural:reformatting
Logic and predicates

By convention, the following two definitions (known as Church Booleans) are used for the Boolean values TRUE and FALSE:

Then, with these two lambda terms, we can define some logic operators (these are just possible formulations; other expressions could be equally correct):

We are now able to compute some logic functions, for example:

and we see that AND TRUE FALSE is equivalent to FALSE.

A predicate is a function that returns a Boolean value. The most fundamental predicate is ISZERO, which returns TRUE if its argument is the Church numeral 0, but FALSE if its argument were any other Church numeral:

The following predicate tests whether the first argument is less-than-or-equal-to the second:

and since m = n, if LEQ m n and LEQ n m, it is straightforward to build a predicate for numerical equality.

The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "if-then-else" expressions in lambda calculus. For example, the predecessor function can be defined as:

which can be verified by showing inductively that n (λ g.λ k.ISZERO (g 1) k (PLUS (g k) 1)) (λ v.0) is the add n − 1 function for n > 0.