Logic is the grammar of proof. Propositions are sentences that are true or false. Connectives combine them. Quantifiers range over domains. Logical equivalence lets you rewrite statements without changing their truth, which is the entire engine of formal proof.
Propositions and connectives
A proposition is a statement that is either true or false. The five connectives: negation (not), conjunction (and), disjunction (or), implication (if-then), biconditional (if and only if). Every compound proposition is built from these.
Scheme
; Propositional connectives as functions
(define (neg p) (not p))
(define (conj p q) (and p q))
(define (disj p q) (or p q))
(define (impl p q) (or (not p) q))
(define (bicon p q) (and (impl p q) (impl q p)))
; Truth table for implication
(display "P Q P->Q") (newline)
(for-each
(lambda (row)
(let ((p (car row)) (q (cadr row)))
(display p) (display " ")
(display q) (display " ")
(display (impl p q)) (newline)))
(list (list #t#t) (list #t#f) (list #f#t) (list #f#f)))
Python
# Connectives
impl = lambda p, q: (not p) or q
bicon = lambda p, q: impl(p, q) and impl(q, p)
print("P Q P->Q")
for p in [True, False]:
for q in [True, False]:
print(f"{p!s:5} {q!s:5} {impl(p, q)}")
Logical equivalences
Two propositions are logically equivalent if they have the same truth value in every row of their truth table. De Morgan's laws, double negation, contrapositive, and distribution are the workhorses. These are the rewrite rules of formal reasoning.
# Verify logical equivalences
impl = lambda p, q: (not p) or q
vals = [True, False]
dm = all(
(not (p and q)) == ((not p) or (not q))
and (not (p or q)) == ((not p) and (not q))
for p in vals for q in vals
)
print(f"De Morgan's laws hold? {dm}")
contra = all(
impl(p, q) == impl(not q, not p)
for p in vals for q in vals
)
print(f"Contrapositive holds? {contra}")
Predicate logic and quantifiers
A predicate is a proposition with a variable: P(x). The universal quantifier "for all x, P(x)" asserts P holds everywhere. The existential quantifier "there exists x such that P(x)" asserts at least one witness. Negating a universal gives an existential, and vice versa.
Scheme
; Predicates over a finite domain
(define domain (list 12345678910))
; P(x): x is even
(define (even? x) (= 0 (modulo x 2)))
; For-all: every element satisfies P
(define (for-all pred lst)
(cond ((null? lst) #t)
((not (pred (car lst))) #f)
(else (for-all pred (cdr lst)))))
; Exists: at least one element satisfies P
(define (exists pred lst)
(cond ((null? lst) #f)
((pred (car lst)) #t)
(else (exists pred (cdr lst)))))
(display "All even? ") (display (for-all even? domain)) (newline)
(display "Some even? ") (display (exists even? domain)) (newline)
; Negation: not(for-all P) = exists(not P)
(display "not(all even) = exists(odd)? ")
(display (equal? (not (for-all even? domain))
(exists (lambda (x) (not (even? x))) domain)))
Python
domain = list(range(1, 11))
print(f"All even? {all(x % 2 == 0 for x in domain)}")
print(f"Some even? {any(x % 2 == 0 for x in domain)}")
print(f"not(all even) == exists(odd)? "f"{(not all(x % 2 == 0 for x in domain)) == any(x % 2 != 0 for x in domain)}")
Proof methods
Direct proof: assume P, derive Q. Contrapositive: assume not-Q, derive not-P. Contradiction: assume P and not-Q, derive a contradiction. Each is valid because the underlying logical equivalences guarantee it. The choice of method is a matter of convenience, not truth.
Scheme
; Example: "if n^2 is even, then n is even"; Contrapositive proof: "if n is odd, then n^2 is odd"; n odd means n = 2k+1 for some k.; n^2 = (2k+1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1, which is odd.; Verify computationally:
(define (even? x) (= 0 (modulo x 2)))
(display "Checking n=1..100: if n^2 even then n even") (newline)
(define (check n)
(if (= n 101) #t
(if (even? (* n n))
(if (even? n)
(check (+ n 1))
#f)
(check (+ n 1)))))
(display "All pass? ")
(display (check 1)) (newline)
; Proof by contradiction example:; sqrt(2) is irrational. Assume a/b in lowest terms,; then 2b^2 = a^2. So a is even. But then b must be; even too, contradicting lowest terms.; (We can't prove this computationally, only state it.)
(display "sqrt(2) irrational: proved by contradiction")
Python
# Verify: if n^2 is even then n is even
check = all(
(n % 2 == 0) if (n * n) % 2 == 0elseTruefor n inrange(1, 101)
)
print(f"All pass (1..100)? {check}")
Notation reference
Math
Scheme
Python
Meaning
P ∧ Q
(and p q)
p and q
Conjunction
P ∨ Q
(or p q)
p or q
Disjunction
P → Q
(impl p q)
impl(p, q)
Implication
∀x P(x)
(for-all pred lst)
all(pred(x) ...)
Universal quantifier
∃x P(x)
(exists pred lst)
any(pred(x) ...)
Existential quantifier
Neighbors
Other chapter pages
Milewski Ch.23 โ topoi have internal logic: subobject classifiers generalize truth values
Levin Ch.2 โ induction is the proof method that matches recurrence relations
Levin's logic chapter covers proof techniques that are inherently human activities. Programs can verify instances but cannot produce proofs. The Scheme implementations model propositions as booleans and quantifiers as folds over finite domains. Real logic quantifies over infinite domains, which requires axioms, not loops. The implication connective is the one that surprises newcomers: "false implies anything" is vacuously true.
Propositional calculus