Craig DeLancey · A Concise Introduction to Logic, Ch. 7 · CC BY-SA 4.0
Predicate logic proofs add four quantifier rules to natural deduction: universal instantiation (plug in a specific value), universal generalization (prove for arbitrary, conclude for all), existential instantiation (name the witness), and existential generalization (from a specific case, conclude something exists).
Universal instantiation (∀E)
From ∀x P(x), conclude P(c) for any constant c. If something holds for everything, it holds for any particular thing.
Scheme
; Universal instantiation: from "for all x, P(x)" derive P(c); A universally quantified statement is a function from any value to a proof
(define domain (list 12345))
; "For all x in domain, x > 0"
(define (forall-positive x) (> x 0))
; Universal instantiation: apply to specific value
(display "forall x>0, instantiate at x=3: ")
(display (forall-positive 3)) (newline)
(display "forall x>0, instantiate at x=5: ")
(display (forall-positive 5))
Universal generalization (∀I)
To prove ∀x P(x), take an arbitrary element c (with no special assumptions about it) and prove P(c). Since c was arbitrary, the proof works for everything.
Scheme
; Universal generalization: prove for arbitrary c, conclude forall; The restriction: c must be truly arbitrary (no assumptions about it); Prove: forall x. (x + 0 = x); Take arbitrary c. c + 0 = c by arithmetic. Done.
(define (plus-zero-identity c) (= (+ c 0) c))
; Test with several values (standing in for "arbitrary")
(display "(c + 0 = c) for c=0: ") (display (plus-zero-identity 0)) (newline)
(display "(c + 0 = c) for c=7: ") (display (plus-zero-identity 7)) (newline)
(display "(c + 0 = c) for c=-3: ") (display (plus-zero-identity -3)) (newline)
(display "Since c was arbitrary: forall x. x + 0 = x")
Existential instantiation (∃E)
From ∃x P(x), introduce a new name c and assume P(c). The name must be fresh: not used elsewhere. You cannot pick which element it is.
Scheme
; Existential instantiation: name the witness; "There exists an even prime" -> call it c, c is even and prime
(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 (even? n) (= 0 (modulo n 2)))
; Find a witness: exists x. even?(x) and prime?(x)
(define domain (list 2345678910))
(define witness #f)
(for-each
(lambda (x)
(if (and (even? x) (prime? x) (not witness))
(set! witness x)))
domain)
(display "Witness for 'exists even prime': ")
(display witness) (newline)
(display "Is it even? ") (display (even? witness)) (newline)
(display "Is it prime? ") (display (prime? witness))
Python
# Existential instantiationdef is_prime(n):
if n < 2: returnFalsereturnall(n % d != 0for d inrange(2, int(n**0.5) + 1))
domain = range(2, 20)
witness = next(x for x in domain if x % 2 == 0and is_prime(x))
print(f"Witness for 'exists even prime': {witness}")
print(f"Even? {witness % 2 == 0}, Prime? {is_prime(witness)}")
Existential generalization (∃I)
From P(c) for some specific c, conclude ∃x P(x). If a particular thing has a property, then something has that property.
Scheme
; Existential generalization: from P(c), derive exists x. P(x); We know 2 is even and prime
(define (even? n) (= 0 (modulo n 2)))
(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)))))))
(display "2 is even: ") (display (even? 2)) (newline)
(display "2 is prime: ") (display (prime? 2)) (newline)
(display "Therefore: exists x. even(x) and prime(x)")
Quantifier negation
¬∀x P(x) ≡ ∃x ¬P(x). "Not everything is P" means "something is not P." ¬∃x P(x) ≡ ∀x ¬P(x). "Nothing is P" means "everything is not P."
Scheme
; Quantifier negation equivalences
(define domain (list 12345))
(define (even? n) (= 0 (modulo n 2)))
(define (forall pred d)
(cond ((null? d) #t) ((not (pred (car d))) #f) (else (forall pred (cdr d)))))
(define (exists pred d)
(cond ((null? d) #f) ((pred (car d)) #t) (else (exists pred (cdr d)))))
; not (forall x. even(x)) should equal exists x. not even(x)
(display "not forall even: ")
(display (not (forall even? domain))) (newline)
(display "exists not-even: ")
(display (exists (lambda (x) (not (even? x))) domain)) (newline)
; not (exists x. > 10) should equal forall x. not (> 10)
(display "not exists >10: ")
(display (not (exists (lambda (x) (> x 10)) domain))) (newline)
(display "forall <=10: ")
(display (forall (lambda (x) (<= x 10)) domain))