; Matt Kaufmann, ICSCA, Univ. of Texas, Austin, TX 78712
; 1/26/87
; Here is a mechanically-checked proof of the finite version
; of Ramsey's Theorem for exponent 2.  This proof was shown
; to me (with ordinary mathematical notation rather than in
; the Boyer-Moore logic) by Jim Schmerl, who claims that it's
; not a new proof.
; Theorem (RAMSEY-THM-2):
; (IMPLIES (LEQ (RAMSEY P Q)
;               (LENGTH DOMAIN))
;          (AND
;            (SUBSETP (HOM-SET PAIRS DOMAIN P Q)
;                     DOMAIN)
;            (OR
;              (AND (HOMOGENEOUS (HOM-SET PAIRS DOMAIN P Q)
;                                PAIRS
;                                1)
;                   (LEQ P (LENGTH (HOM-SET PAIRS DOMAIN P Q))))
;              (AND (HOMOGENEOUS (HOM-SET PAIRS DOMAIN P Q)
;                                PAIRS
;                                2)
;                   (LEQ Q (LENGTH (HOM-SET PAIRS DOMAIN P Q)))))))
; Here, HOM-SET can be thought of as a Skolem function which picks
; out the desired homogeneous subset of the given DOMAIN, i.e.
; homogeneous with respect to the relation PAIRS (presented as a
; list of ordered pairs).  Notice that if DOMAIN has no repetitions
; (which is a harmless assumption for the statement of Ramsey's
; Theorem), then LENGTH is just cardinality.  The function LEQ is
; just "less than or equal", at least on the natural numbers.
; (HOMOGENEOUS S PAIRS 1) is true, i.e. equals T, if the list
; S is homogeous with respect to PAIRS in the positive sense,
; i.e., in that each pair from S is related by PAIRS (i.e. either
; the pair or its reverse belongs to PAIRS).  Similary,
; (HOMOGENEOUS S PAIRS 2) is true if no pair from S belongs to
; PAIRS (in the same sense).  RAMSEY is a function which returns
; an integer which (according to the theorem above) is "large
; enough".  However, at the end of this note we prove that
; (RAMSEY P Q) = (CHOOSE (PLUS P Q) P), where (CHOOSE M N) is
; the binomial coefficient (defined though with integer division).

; The description above completes the discussion of the theorem,
; but to read on it helps to realize that we don't define HOM-SET
; until near the end of this note.  Instead, we define a function
; WIT which returns a pair, so that HOM-SET merely returns the CAR
; of this pair.  The CDR of the value of WIT is the "color", which
; is 1 or 2 (as is proved in a lemma below).  It's really best to
; think of WIT as a Skolem function, though in fact it is defined
; to make the theorem true.

Event: Start with the initial nqthm theory.

Definition: ramsey (p, q) = if p ≃ 0 then 1

elseif q ≃ 0 then 1

else ramsey (p − 1, q) + ramsey (p, q − 1) endif

;this is a hint to get the
;definition accepted

Definition: related (i, j , pairs) = ((cons (i, j ) ∈ pairs) ∨ (cons (j , i) ∈ pairs))

Definition: partition (n, rest, pairs) = if listp (rest)

then if related (n, car (rest), pairs)

then cons (cons (car (rest), car (partition (n, cdr (rest), pairs))), cdr (partition (n, cdr (rest), pairs)))

else cons (car (partition (n, cdr (rest), pairs)),

cons (car (rest), cdr (partition (n, cdr (rest), pairs)))) endif

else cons (nil, nil) endif

Definition: length (lst) = if listp (lst) then 1 + length (cdr (lst))

else 0 endif

Definition: wit (pairs, domain, p, q) = if p ≃ 0 then cons (nil, 1)

elseif q ≃ 0 then cons (nil, 2)

elseif length (car (partition (car (domain), cdr (domain), pairs)))

< ramsey (p − 1, q) then if cdr (wit (pairs,

cdr (partition (car (domain), cdr (domain), pairs)), p, q − 1))

       = 1

then wit (pairs, cdr (partition (car (domain), cdr (domain), pairs)), p, q − 1) else cons (cons (car (domain),

car (wit (pairs,

cdr (partition (car (domain), cdr (domain), pairs)),

p,

q − 1))),

2) endif

elseif cdr (wit (pairs, car (partition (car (domain), cdr (domain), pairs)), p − 1, q))

     = 2

then wit (pairs, car (partition (car (domain), cdr (domain), pairs)), p − 1, q) else cons (cons (car (domain),

car (wit (pairs,

car (partition (car (domain), cdr (domain), pairs)),

p − 1, q))),

1) endif

Definition: homogeneous1 (n, domain, pairs, flg) = if listp (domain)

then if flg = 1 then related (n, car (domain), pairs)

else ¬ related (n, car (domain), pairs) endif ∧ homogeneous1 (n, cdr (domain), pairs, flg)

else t endif

Definition: homogeneous (domain, pairs, flg) = if listp (domain) then homogeneous1 (car (domain), cdr (domain), pairs, flg) ∧ homogeneous (cdr (domain), pairs, flg)

else t endif

Theorem: length-of-partitions length (cons (n, domain)) = (1 + (length (car (partition (n, domain, pairs)))

+ length (cdr (partition (n, domain, pairs)))))

Theorem: lessp-length-ramsey-2 (listp (domain) ∧ (i ≄ 0) ∧ (j ≄ 0) ∧ ((i + j ) ≤ length (domain)) ∧ (length (car (partition (car (domain), cdr (domain), pairs))) < i)) → ((length (cdr (partition (car (domain), cdr (domain), pairs))) < j ) = f)

Theorem: ramsey-not-zerop ramsey (p, q) ≄ 0

Event: Disable lessp-length-ramsey-2.

Theorem: lessp-length-ramsey ((p ≄ 0) ∧ (q ≄ 0) ∧ (ramsey (p, q) ≤ length (domain)) ∧ (length (car (partition (car (domain), cdr (domain), pairs)))

< ramsey (p − 1, q))) → ((length (cdr (partition (car (domain), cdr (domain), pairs)))

< ramsey (p, q − 1))

= f)

Theorem: wit-flag (cdr (wit (pairs, domain, p, q)) ≠ 1) → (cdr (wit (pairs, domain, p, q)) = 2)

Theorem: homogeneous1-partition-cdr homogeneous1 (a, cdr (partition (a, domain, pairs)), pairs, 2)

Theorem: homogeneous1-partition-car homogeneous1 (a, car (partition (a, domain, pairs)), pairs, 1)

Definition: subsetp (x, y) = if x ≃ nil then t

elseif car (x) ∈ y then subsetp (cdr (x), y)

else f endif Theorem: subsetp-preserves-homogeneous1 (subsetp (l, m) ∧ homogeneous1 (a, m, pairs, flg)) → homogeneous1 (a, l, pairs, flg)

; The following lemmas, till further notice, are simply
; lemmas about sets, some of which may be needed below.

Theorem: member-cons (a ∈ l) → (a ∈ cons (x, l))

Theorem: subsetp-cons subsetp (l, m) → subsetp (l, cons (a, m))

Theorem: subsetp-reflexivity subsetp (x, x)

Theorem: cdr-subsetp subsetp (cdr (x), x)

Theorem: member-subsetp ((x ∈ y) ∧ subsetp (y, z)) → (x ∈ z)

Theorem: subsetp-is-transitive (subsetp (x, y) ∧ subsetp (y, z)) → subsetp (x, z)

; end of silly subset lemmas

Theorem: partition-subsetp subsetp (car (partition (a, dom, pairs)), dom) ∧ subsetp (cdr (partition (a, dom, pairs)), dom)

Theorem: ramsey-not-zero ramsey (p, q) ≠ 0

Theorem: witness-subsetp (ramsey (p, q) ≤ length (domain)) → subsetp (car (wit (pairs, domain, p, q)), domain)

; Here are the commands to generate proofs of four of
; the six induction steps in the theorem.

Theorem: ramsey-thm-2-goals-1-2-3-5 t Theorem: all-but-goal-4 t

Theorem: ramsey-thm-2-except-length (ramsey (p, q) ≤ length (domain)) → homogeneous (car (wit (pairs, domain, p, q)),

pairs,

cdr (wit (pairs, domain, p, q)))

Theorem: ramsey-thm-2-length (ramsey (p, q) ≤ length (domain)) → ((length (car (wit (pairs, domain, p, q)))

< if cdr (wit (pairs, domain, p, q)) = 1 then p

else q endif) = f)

; Finally, the main theorem's proof is concluded:

Definition: hom-set (pairs, domain, p, q) = car (wit (pairs, domain, p, q))

Theorem: ramsey-thm-2 (ramsey (p, q) ≤ length (domain)) → (subsetp (hom-set (pairs, domain, p, q), domain)

∧ ((homogeneous (hom-set (pairs, domain, p, q), pairs, 1) ∧ (p ≤ length (hom-set (pairs, domain, p, q)))) ∨ (homogeneous (hom-set (pairs, domain, p, q), pairs, 2) ∧ (q ≤ length (hom-set (pairs, domain, p, q))))))

;;; The following were aded 4/22/88 to show that in fact, under the
;;; hypotheses of the theorem above, the HOM-SET has no duplicates
;;; (and hence LENGTH really does measure cardinality, though I don't
;;; formalize or prove this parenthetical remark).

Definition: setp (x) = if listp (x) then (car (x) ∉ cdr (x)) ∧ setp (cdr (x))

else t endif

Theorem: set-partition setp (x) → (setp (car (partition (a, x, pairs))) ∧ setp (cdr (partition (a, x, pairs))))

Theorem: member-partition (a ∉ x) → ((a ∉ car (partition (b, x, pairs)))

∧ (a ∉ cdr (partition (b, x, pairs))))

Theorem: member-cons-expand (a ∈ cons (b, y)) = if a = b then t

else a ∈ y endif

Theorem: setp-cons-expand setp (cons (b, y)) = if b ∈ y then f

else setp (y) endif

Theorem: member-hom-set-implies-member-domain ((length (domain) ≮ ramsey (p, q)) ∧ (a ∉ domain)) → (a ∉ car (wit (pairs, domain, p, q)))

Theorem: setp-hom-set ((length (domain) ≮ ramsey (p, q)) ∧ setp (domain)) → setp (hom-set (pairs, domain, p, q))

Index

all-but-goal-4, 6

cdr-subsetp, 5

hom-set, 6, 7 homogeneous, 3, 4, 6 homogeneous1, 3–5 homogeneous1-partition-car, 4 homogeneous1-partition-cdr, 4

length, 2, 4–7 length-of-partitions, 4 lessp-length-ramsey, 4 lessp-length-ramsey-2, 4

member-cons, 5 member-cons-expand, 7 member-hom-set-implies-member-d

omain, 7 member-partition, 7 member-subsetp, 5

partition, 2–7 partition-subsetp, 5

ramsey, 2–7 ramsey-not-zero, 5 ramsey-not-zerop, 4 ramsey-thm-2, 6 ramsey-thm-2-except-length, 6 ramsey-thm-2-goals-1-2-3-5, 5 ramsey-thm-2-length, 6 related, 2, 3

set-partition, 6 setp, 6, 7 setp-cons-expand, 7 setp-hom-set, 7 subsetp, 4–6 subsetp-cons, 5 subsetp-is-transitive, 5 subsetp-preserves-homogeneous1, 5 subsetp-reflexivity, 5

wit, 2–7 wit-flag, 4 witness-subsetp, 5