Craig DeLancey · A Concise Introduction to Logic, Ch. 8 · CC BY-SA 4.0
Identity (=) lets us say two names refer to the same object. Combined with quantifiers, it expresses uniqueness ("there is exactly one") and definite descriptions ("the x such that"). Functions in logic map each input to exactly one output.
Equality
The identity predicate x = y means x and y are the same object. It obeys reflexivity (a = a), symmetry (if a = b then b = a), and transitivity (if a = b and b = c then a = c). It also obeys substitution: if a = b, then anything true of a is true of b.
Scheme
; Identity: reflexive, symmetric, transitive, substitutive; Reflexivity
(display "a = a: ") (display (= 55)) (newline)
; Symmetry
(display "a = b implies b = a: ")
(let ((a 5) (b 5))
(display (equal? (= a b) (= b a)))) (newline)
; Transitivity
(display "a=b and b=c implies a=c: ")
(let ((a 5) (b 5) (c 5))
(display (and (= a b) (= b c) (= a c)))) (newline)
; Substitution: if a = b and P(a), then P(b)
(define (even? n) (= 0 (modulo n 2)))
(let ((a 4) (b 4))
(display "a=b and even(a) implies even(b): ")
(display (and (= a b) (even? a) (even? b))))
Uniqueness: "there exists exactly one"
∃!x P(x) means "there exists exactly one x such that P(x)." It is defined as: ∃x(P(x) ∧ ∀y(P(y) → y = x)). There is a witness, and anything else satisfying P must be that same witness.
Scheme
; "There exists exactly one" = exists + unique
(define (exists-unique pred domain)
; Find all elements satisfying pred
(let loop ((d domain) (witnesses (list)))
(if (null? d)
(= (length witnesses) 1)
(loop (cdr d)
(if (pred (car d))
(cons (car d) witnesses)
witnesses)))))
(define domain (list 12345678910))
(define (is-five? x) (= x 5))
(define (even? x) (= 0 (modulo x 2)))
(display "Exists unique x=5 in 1..10: ")
(display (exists-unique is-five? domain)) (newline)
(display "Exists unique even in 1..10: ")
(display (exists-unique even? domain))
(display " (multiple evens exist)")
Python
# Exists-unique
domain = list(range(1, 11))
def exists_unique(pred, domain):
witnesses = [x for x in domain if pred(x)]
returnlen(witnesses) == 1print(f"Unique x=5: {exists_unique(lambda x: x == 5, domain)}")
print(f"Unique even: {exists_unique(lambda x: x % 2 == 0, domain)}")
Definite descriptions
"The x such that P(x)" presupposes exactly one such x exists. In logic, "the even prime" means ∃!x(even(x) ∧ prime(x)), and the description refers to that unique witness.
Scheme
; Definite description: "the x such that P(x)"; Only meaningful when exactly one x satisfies P
(define (the pred domain)
(let loop ((d domain) (found #f))
(cond
((null? d)
(if found found "undefined: no element found"))
((pred (car d))
(if found
"undefined: not unique"
(loop (cdr d) (car d))))
(else (loop (cdr d) found)))))
(define (prime? n)
(if (< n 2) #f
(let loop ((d 2))
(cond ((> (* d d) n) #t)
((= 0 (modulo n d)) #f)
(else (loop (+ d 1)))))))
(define domain (list 12345678910))
(display "The even prime: ")
(display (the (lambda (x) (and (= 0 (modulo x 2)) (prime? x))) domain)) (newline)
(display "The prime > 5 and < 10: ")
(display (the (lambda (x) (and (prime? x) (> x 5) (< x 10))) domain))
Functions in logic
A function f from domain D to codomain C assigns each element of D exactly one element of C. In predicate logic: ∀x ∃!y f(x) = y. Every input has exactly one output.
Scheme
; A function: every input maps to exactly one output; We verify this property
(define (f x) (* x x)) ; f(x) = x^2; Check: for each x, f(x) is well-defined (always returns one value)
(define inputs (list -3-2-10123))
(display "f(x) = x^2 outputs: ")
(display (map f inputs)) (newline)
; Is f injective (one-to-one)? forall x,y: f(x)=f(y) -> x=y; No: f(-2) = f(2) = 4
(display "f(-2) = ") (display (f -2)) (newline)
(display "f(2) = ") (display (f 2)) (newline)
(display "f(-2) = f(2) but -2 != 2: not injective")