Craig DeLancey · A Concise Introduction to Logic, Ch. 6 · CC BY-SA 4.0
Predicate logic extends propositional logic with predicates (properties of objects), quantifiers (∀ "for all", ∃ "there exists"), and variables. It can express statements about individuals in a domain that propositional logic cannot.
Predicates
A predicate is a property or relation applied to objects. P(x) means "x has property P." R(x, y) means "x stands in relation R to y." Unlike propositions, predicates have open slots that variables fill.
Scheme
; Predicates are functions that return true or false
(define (even? n) (= 0 (modulo n 2)))
(define (greater? x y) (> x y))
; Predicate applied to specific objects
(display "even?(4) = ") (display (even? 4)) (newline)
(display "even?(7) = ") (display (even? 7)) (newline)
(display "greater?(5, 3) = ") (display (greater? 53)) (newline)
(display "greater?(2, 8) = ") (display (greater? 28))
Quantifiers
∀x P(x) means "for every x in the domain, P(x) is true." ∃x P(x) means "there is at least one x in the domain where P(x) is true."
Scheme
; Quantifiers over a finite domain
(define domain (list 246810))
; forall: every element satisfies the predicate
(define (forall pred domain)
(cond
((null? domain) #t)
((not (pred (car domain))) #f)
(else (forall pred (cdr domain)))))
; exists: at least one element satisfies the predicate
(define (exists pred domain)
(cond
((null? domain) #f)
((pred (car domain)) #t)
(else (exists pred (cdr domain)))))
(define (even? n) (= 0 (modulo n 2)))
(define (less-than-5? n) (< n 5))
(display "forall even? in (2 4 6 8 10): ")
(display (forall even? domain)) (newline)
(display "exists less-than-5? in (2 4 6 8 10): ")
(display (exists less-than-5? domain)) (newline)
(display "forall less-than-5? in (2 4 6 8 10): ")
(display (forall less-than-5? domain))
Python
# Quantifiers over a finite domain
domain = [2, 4, 6, 8, 10]
print(f"forall even in domain: {all(x % 2 == 0 for x in domain)}")
print(f"exists < 5 in domain: {any(x < 5 for x in domain)}")
print(f"forall < 5 in domain: {all(x < 5 for x in domain)}")
Bound and free variables
A variable is bound when it falls under a quantifier. A variable is free when it does not. ∀x P(x) has x bound. P(x) ∧ Q(y) has both x and y free. A sentence (closed formula) has no free variables.
Scheme
; Checking for free variables in a formula; Representation: (forall x (P x)) or (and (P x) (Q y))
(define (free-vars formula bound)
(cond
((symbol? formula)
(if (member formula bound) (list) (list formula)))
((or (equal? (car formula) (quote forall))
(equal? (car formula) (quote exists)))
; Quantifier binds a variable
(free-vars (caddr formula) (cons (cadr formula) bound)))
((member (car formula) (list (quote and) (quote or) (quote implies)))
(append (free-vars (cadr formula) bound)
(free-vars (caddr formula) bound)))
(else; Predicate application like (P x)
(let loop ((args (cdr formula)) (result (list)))
(if (null? args) result
(loop (cdr args)
(append result (free-vars (car args) bound))))))))
; forall x. P(x) -- x is bound, no free vars
(display "Free vars in (forall x (P x)): ")
(display (free-vars (list (quote forall) (quote x) (list (quote P) (quote x))) (list))) (newline)
; P(x) and Q(y) -- x and y are free
(display "Free vars in (and (P x) (Q y)): ")
(display (free-vars (list (quote and) (list (quote P) (quote x)) (list (quote Q) (quote y))) (list)))
Translating English to logic
"All dogs bark" becomes ∀x(Dog(x) → Barks(x)). Note: it uses implication, not conjunction. "Some cats purr" becomes ∃x(Cat(x) ∧ Purrs(x)). Note: it uses conjunction, not implication.
Scheme
; Translation examples; Domain: all animals
(define animals (list "dog1""dog2""cat1""cat2""fish1"))
(define (dog? x) (or (equal? x "dog1") (equal? x "dog2")))
(define (cat? x) (or (equal? x "cat1") (equal? x "cat2")))
(define (barks? x) (or (equal? x "dog1") (equal? x "dog2")))
(define (purrs? x) (equal? x "cat1"))
(define (forall pred domain)
(cond ((null? domain) #t)
((not (pred (car domain))) #f)
(else (forall pred (cdr domain)))))
(define (exists pred domain)
(cond ((null? domain) #f)
((pred (car domain)) #t)
(else (exists pred (cdr domain)))))
; "All dogs bark" = forall x. Dog(x) -> Barks(x)
(define (impl p q) (or (not p) q))
(display "All dogs bark: ")
(display (forall (lambda (x) (impl (dog? x) (barks? x))) animals)) (newline)
; "Some cats purr" = exists x. Cat(x) and Purrs(x)
(display "Some cats purr: ")
(display (exists (lambda (x) (and (cat? x) (purrs? x))) animals))