3. Church Booleans and Logical Connectives

Contents

Working System

This chapter uses untyped lambda encodings (Church booleans), executed as Python higher-order functions.

3. Church Booleans and Logical Connectives#

Goal. Encode booleans as lambda terms and build logical connectives from functions alone.

You will learn

  • Church booleans as branch selectors (TRUE, FALSE, IF)

  • How to encode NOT, AND, OR, and IMPLIES as higher-order functions

  • What it means for two boolean terms to be extensionally equal

  • How to validate boolean identities by exhaustive truth-table checks

Roadmap#

  1. Define TRUE, FALSE, and IF as choice operators.

  2. Define the standard logical connectives and test them on inputs.

  3. State and validate basic laws (commutativity, associativity, De Morgan).

  4. Use truth tables to justify equivalences that will reappear later (Curry-Howard and Church arithmetic).

Definition (Church Booleans)

We encode booleans as choice operators.

  • TRUE  ≡ λt. λf. t

  • FALSE ≡ λt. λf. f

TRUE = lambda t: (lambda f: t)
FALSE = lambda t: (lambda f: f)

IF = lambda b: (lambda t: (lambda f: b(t)(f)))

def to_bool(b):
    return b(True)(False)

def from_bool(b):
    return TRUE if b else FALSE

Remark (Equality of Church Booleans)

Boolean identities in this chapter are extensional: two Church booleans are equal when they choose the same branch for all inputs.

Remark (Evaluation Strategy)

Church-style IF behaves lazily under normal-order reduction. Python is eager; Chapter 6 introduces thunk-based conditionals (IF_THUNK) for recursive definitions.

Definition (Logical Connectives)

Using only functions, we define:

  • AND p q = p q p

  • OR p q  = p p q

  • NOT p   = p FALSE TRUE

  • IMPLIES p q = p q TRUE

AND = lambda p: (lambda q: p(q)(p))
OR = lambda p: (lambda q: p(p)(q))
NOT = lambda p: p(FALSE)(TRUE)
IMPLIES = lambda p: (lambda q: p(q)(TRUE))
XOR = lambda p: (lambda q: p(NOT(q))(q))

Example (Truth Table)

Compute the truth table for AND and OR using Python.

values = [TRUE, FALSE]
for p in values:
    for q in values:
        print("p=", to_bool(p), "q=", to_bool(q),
              "AND=", to_bool(AND(p)(q)),
              "OR=", to_bool(OR(p)(q)),
              "IMPLIES=", to_bool(IMPLIES(p)(q)))

p= True q= True AND= True OR= True IMPLIES= True
p= True q= False AND= False OR= True IMPLIES= False
p= False q= True AND= False OR= True IMPLIES= True
p= False q= False AND= False OR= False IMPLIES= True

Lemma (De Morgan)

NOT (AND p q) is equivalent to OR (NOT p) (NOT q).

def eq_bool(p, q):
    return to_bool(p) == to_bool(q)

for p in values:
    for q in values:
        left = NOT(AND(p)(q))
        right = OR(NOT(p))(NOT(q))
        print(to_bool(p), to_bool(q), eq_bool(left, right))

True True True
True False True
False True True
False False True

Exercise

  1. Define NAND using only AND and NOT.

  2. Prove by computation that IMPLIES p q is equivalent to OR (NOT p) q.

  3. Define XOR and verify its truth table.

  4. Verify by computation that AND is commutative and associative. See solution: Exercise 3 (Church Booleans)

Summary#

  • Church booleans are functions that choose between two branches.

  • Logical connectives are definable purely by function application.

  • Boolean equivalences are best read extensionally: two terms are equal if they choose the same branch on all inputs.

  • Truth-table evaluation gives an executable way to validate logical laws.

  • Operationally: define a new connective (like XOR) and use a small exhaustive loop to test it.

  • Next: we will reconstruct proofs as programs via types (Curry-Howard / STLC) in Chapter 4.

Contents