;; The infinite Ramsey Theorem for exponent 2.

Event: Start with the initial nqthm theory.

;; We introduce the partition p on pairs via a CONSTRAIN event which
;; asserts that p is a symmetric function with range {1, ...,
;; (bound)}.  Actually, we do this by (roughly speaking) introducing a
;; function p-num on numbers and then extending it to a function p on
;; everything.

Conservative Axiom: p-num-intro ((x ∈ N) ∧ (y ∈ N)) → ((0 < p-num (x, y))

∧ (bound ≮ p-num (x, y))

∧ (p-num (x, y) = p-num (y, x)))

Simultaneously, we introduce the new function symbols p-num and bound. Event: Disable p-num-intro.

Definition: p (x, y) = p-num (fix (x), fix (y))

Theorem: p-intro (0 < p (x, y)) ∧ (bound ≮ p (x, y)) ∧ (p (x, y) = p (y, x))

Event: Disable p.

Definition: prehom-seq-1 (a, x) = if listp (x)

then (p (caar (x), a) = cdar (x)) ∧ prehom-seq-1 (a, cdr (x))

else t endif

Definition: prehom-seq (x) = if listp (x)

then if listp (cdr (x))

then (car (cadr (x)) < car (car (x))) ∧ prehom-seq-1 (caar (x), cdr (x)) ∧ prehom-seq (cdr (x))

else t endif else t endif Definition: extensible (s) ↔ ∀ above ∃ next ((above < next) ∧ prehom-seq-1 (next, s))

;; The following two lemmas are for the benefit of the proof-checker
;; macro-command SK*.

Theorem: extensible-suff ((above (s) < next) ∧ prehom-seq-1 (next, s)) → extensible (s)

Theorem: extensible-necc (¬ ((above < next (above, s)) ∧ prehom-seq-1 (next (above, s), s))) → (¬ extensible (s))

Definition: above-all-aux (a, s, n) = if n ≃ 0 then 0

else above (cons (cons (a, n), s)) + above-all-aux (a, s, n − 1) endif

Definition: above-all (a, s) = above-all-aux (a, s, bound)

Theorem: lessp-above-all-aux (0 < n) → (above-all-aux (a, s, n) ≮ above (cons (cons (a, n), s)))

Theorem: above-all-aux-monotone (bound ≮ n) → (above-all-aux (a, s, bound) ≮ above-all-aux (a, s, n))

Theorem: lessp-above-all-bound ((0 < n) ∧ (bound ≮ n)) → (above-all (a, s) ≮ above (cons (cons (a, n), s)))

Definition: next-element (a, s) = next (above-all (a, s), s)

Definition: next-color (a, s) = p (a, next-element (a, s))

Theorem: numberp-p p (x, y) ∈ N

Theorem: next-color-bound (0 < next-color (a, s)) ∧ (bound ≮ next-color (a, s))

Event: Disable above-all.

;; first of two goals for extensible-cons

Theorem: lessp-next-element extensible (s) → (above (cons (cons (a, next-color (a, s)), s)) < next-element (a, s))

Theorem: prehom-seq-1-next-element extensible (s) → prehom-seq-1 (next-element (a, s), s)

Event: Disable next-element.

;; second of two goals for extensible-cons

Theorem: prehom-seq-1-next-element-cons extensible (s) → prehom-seq-1 (next-element (a, s), cons (cons (a, next-color (a, s)), s))

Event: Disable next-color.

Theorem: extensible-cons extensible (s) → extensible (cons (cons (a, next-color (a, s)), s))

Definition: next-pair (s) = cons (next (caar (s), s), next-color (next (caar (s), s), s))

Theorem: next-pair-extends extensible (s) → extensible (cons (next-pair (s), s))

Definition: ramsey-seq-p (s) = (extensible (s) ∧ prehom-seq (s))

Theorem: extensible-next-property extensible (s) → ((a < next (a, s)) ∧ prehom-seq-1 (next (a, s), s))

Theorem: ramsey-seq-p-extends ramsey-seq-p (s) → ramsey-seq-p (cons (next-pair (s), s))

Theorem: extensible-nlistp (¬ listp (s)) → extensible (s)

Theorem: ramsey-seq-p-nlistp (s ≃ nil) → ramsey-seq-p (s)

Event: Disable ramsey-seq-p.

Event: Disable next-pair.

Definition: ramsey-seq (n) = if n ≃ 0 then nil

else cons (next-pair (ramsey-seq (n − 1)), ramsey-seq (n − 1)) endif

Theorem: ramsey-seq-has-ramsey-seq-p ramsey-seq-p (ramsey-seq (n))

;; Now we want to cut down this prehomogenous sequence to one that's
;; homogeneous.  First let's define the flag.

Definition: good-color-p (c) ↔ ∀ big ∃ good-c-index ((big < good-c-index)

∧ (c = cdr (car (ramsey-seq (good-c-index)))))

;; The following two lemmas are for the benefit of the proof-checker
;; macro-command SK*.

Theorem: good-color-p-suff ((big (c) < good-c-index) ∧ (c = cdar (ramsey-seq (good-c-index)))) → good-color-p (c)

Theorem: good-color-p-necc (¬ ((big < good-c-index (big, c))

∧ (c = cdar (ramsey-seq (good-c-index (big, c)))))) → (¬ good-color-p (c))

Definition: good-c-index-wit (bound) = if bound ≃ 0 then 1

else big (bound) + good-c-index-wit (bound − 1) endif

Theorem: good-c-index-wit-positive 0 < good-c-index-wit (bound)

Theorem: lessp-big-good-c-index ((0 < c) ∧ (bound ≮ c)) → ((big (c) < good-c-index-wit (bound)) = t)

Event: Disable good-c-index-wit.

Definition: color = cdar (ramsey-seq (good-c-index-wit (bound)))

Theorem: ramsey-seq-has-colors-in-bounds (0 < n) → ((0 < cdar (ramsey-seq (n))) ∧ (bound ≮ cdar (ramsey-seq (n))))

Theorem: color-in-bounds (0 < color) ∧ (bound ≮ color)

Theorem: color-is-good good-color-p (color)

Event: Disable color.

Event: Disable *1*color.

Definition: ramsey-index (n) = if n ≃ 0 then good-c-index (0, color)

else good-c-index (ramsey-index (n − 1), color) endif

Theorem: color-properties (big < good-c-index (big, color)) ∧ (cdr (car (ramsey-seq (good-c-index (big, color)))) = color)

Theorem: ramsey-index-increasing (i < j ) → (ramsey-index (i) < ramsey-index (j ))

Definition: ramsey (n) = car (car (ramsey-seq (ramsey-index (n))))

#| Next goal:
(prove-lemma ramsey-increasing (rewrite)
  (implies (lessp i j)
   (lessp (ramsey i) (ramsey j))))
|#

Theorem: good-c-index-numberp good-c-index (big, color) ∈ N

Theorem: ramsey-index-numberp ramsey-index (n) ∈ N

Theorem: car-next-pair car (next-pair (s)) = next (caar (s), s)

Theorem: ramsey-seq-extensible extensible (ramsey-seq (n))

Theorem: next-not-zerop extensible (s) → ((next (a, s) ∈ N) ∧ (next (a, s) ≠ 0))

Theorem: ramsey-seq-increasing (i < j ) → ((caar (ramsey-seq (i)) < caar (ramsey-seq (j ))) = t)

Theorem: ramsey-index-increasing-rewrite (i < j ) → ((ramsey-index (i) < ramsey-index (j )) = t)

Event: Disable ramsey-index-increasing.

Theorem: ramsey-increasing (i < j ) → (ramsey (i) < ramsey (j ))

;; Now we want to show that ramsey is homogeneous for (color):
#|
(prove-lemma ramsey-homogeneous (rewrite)
  (implies (lessp i j)
   (iff (p (ramsey i) (ramsey j))
(color))))
|#

Definition: restn (n, l) = if listp (l)

then if n ≃ 0 then l

else restn (n − 1, cdr (l)) endif else l endif

;; We've already proved (ramsey-seq-p (ramseq-seq i)).  So, in order
;; to prove the key lemma ramsey-seq-prehom below, we'll use this
;; together with an appropriate fact about restn and prehom seqs.

Theorem: ramsey-seq-restn-length restn (n, ramsey-seq (n)) = nil

Theorem: prehom-seq-ramsey prehom-seq (ramsey-seq (n))

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

else 0 endif Theorem: prehom-seq-1-restn (prehom-seq-1 (a, s) ∧ (x < length (s))) → (p (caar (restn (x, s)), a) = cdar (restn (x, s)))

Theorem: prehom-seq-restn (prehom-seq (s) ∧ (0 < x) ∧ (x < length (s))) → (p (caar (restn (x, s)), caar (s)) = cdar (restn (x, s)))

Theorem: ramsey-seq-plus restn (x, ramsey-seq (x + y)) = ramsey-seq (y)

Theorem: plus-comm (x + y) = (y + x)

Theorem: ramsey-seq-plus-commuted restn (x, ramsey-seq (y + x)) = ramsey-seq (y)

Theorem: length-ramsey-seq length (ramsey-seq (n)) = fix (n)

;; The lemmas from here to RAMSEY-SEQ-PREHOM were to eliminate the
;; proof-checker hints from that lemma.

Theorem: plus-difference-elim ((j ∈ N) ∧ (j ≮ i)) → ((i + (j − i)) = j )

Theorem: restn-difference-ramsey-seq ((0 < i) ∧ (i < j )) → (restn (j − i, ramsey-seq (j )) = ramsey-seq (i))

Theorem: prehom-seq-restn-commuted (prehom-seq (s) ∧ (0 < x) ∧ (x < length (s))) → (p (caar (s), caar (restn (x, s))) = cdar (restn (x, s)))

Theorem: ramsey-seq-prehom-lemma ((0 < i) ∧ (i < j )) → (p (caar (restn (j − i, ramsey-seq (j ))), caar (ramsey-seq (j )))

= cdar (restn (j − i, ramsey-seq (j ))))

Theorem: ramsey-seq-prehom ((0 < i) ∧ (i < j )) → (p (caar (ramsey-seq (i)), caar (ramsey-seq (j ))) = cdar (ramsey-seq (i)))

Theorem: cdar-ramseq-seq-ramsey-index cdar (ramsey-seq (ramsey-index (n))) = color Theorem: lessp-good-c-index (big < good-c-index (big, color)) = t

Event: Disable color-properties.

Theorem: good-c-index-non-zero (0 < good-c-index (big, color)) = t

Theorem: ramsey-index-positive 0 < ramsey-index (n)

Theorem: ramsey-seq-hom-lessp (i < j ) → (p (ramsey (i), ramsey (j )) = color)

Theorem: p-num-is-p ((x ∈ N) ∧ (y ∈ N)) → (p-num (x, y) = p (x, y))

Theorem: numberp-ramsey caar (ramsey-seq (ramsey-index (n))) ∈ N

Theorem: ramsey-seq-hom ((i ∈ N) ∧ (j ∈ N) ∧ (i ≠ j )) → (p-num (ramsey (i), ramsey (j )) = color)

;; The above, together with what was already proved, i.e.
;; (prove-lemma ramsey-increasing (rewrite)
;;  (implies (lessp i j)
;;      (lessp (ramsey i) (ramsey j))))
;; and the fact that p-num was arbitrary (and there are no add-axioms)
;; finishes the job.

Index

above, 2, 3 above-all, 2 above-all-aux, 2 above-all-aux-monotone, 2

big, 4 bound, 1, 2, 4, 5

car-next-pair, 5 cdar-ramseq-seq-ramsey-index, 7 color, 4, 5, 7, 8 color-in-bounds, 5 color-is-good, 5 color-properties, 5

exists, 2, 4 extensible, 2, 3, 5, 6 extensible-cons, 3 extensible-necc, 2 extensible-next-property, 3 extensible-nlistp, 3 extensible-suff, 2

forall, 2, 4

good-c-index, 4, 5, 8 good-c-index-non-zero, 8 good-c-index-numberp, 5 good-c-index-wit, 4 good-c-index-wit-positive, 4 good-color-p, 4, 5 good-color-p-necc, 4 good-color-p-suff, 4

length, 6, 7 length-ramsey-seq, 7 lessp-above-all-aux, 2 lessp-above-all-bound, 2 lessp-big-good-c-index, 4 lessp-good-c-index, 8 lessp-next-element, 3 next, 2, 3, 5, 6 next-color, 2, 3 next-color-bound, 2 next-element, 2, 3 next-not-zerop, 6 next-pair, 3–5 next-pair-extends, 3 numberp-p, 2 numberp-ramsey, 8

p, 1, 2, 7, 8 p-intro, 1 p-num, 1, 8 p-num-intro, 1 p-num-is-p, 8 plus-comm, 7 plus-difference-elim, 7 prehom-seq, 1, 3, 6, 7 prehom-seq-1, 1–3, 7 prehom-seq-1-next-element, 3 prehom-seq-1-next-element-cons, 3 prehom-seq-1-restn, 7 prehom-seq-ramsey, 6 prehom-seq-restn, 7 prehom-seq-restn-commuted, 7

ramsey, 5, 6, 8 ramsey-increasing, 6 ramsey-index, 5–8 ramsey-index-increasing, 5 ramsey-index-increasing-rewrite, 6 ramsey-index-numberp, 5 ramsey-index-positive, 8 ramsey-seq, 4–8 ramsey-seq-extensible, 5 ramsey-seq-has-colors-in-bounds, 5 ramsey-seq-has-ramsey-seq-p, 4 ramsey-seq-hom, 8 ramsey-seq-hom-lessp, 8 ramsey-seq-increasing, 6 ramsey-seq-p, 3, 4 ramsey-seq-p-extends, 3 ramsey-seq-p-nlistp, 3 ramsey-seq-plus, 7 ramsey-seq-plus-commuted, 7 ramsey-seq-prehom, 7 ramsey-seq-prehom-lemma, 7 ramsey-seq-restn-length, 6 restn, 6, 7 restn-difference-ramsey-seq, 7