#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; Matt Kaufmann
;; Ramsey Theorem (infinite version) events supporting ``An Extension
;; of the Boyer-Moore Theorem Prover to Support First-Order
;; Quantification,'' to appear in JAR (1992?).  The DEFN-SK events
;; have been replaced by DCLs and ADD-AXIOMs, as shown.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Ramsey Theorem Events List
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Start with the initial nqthm theory.

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

#| The original DEFN-SK event here was processed as follows:
>(defn-sk extensible (s)
  ;; s is a list of pairs (i . c), and extensible means that there
  ;; are infinitely many a for which prehom-seq-1(a,s) holds.
  (forall above
          (exists next
                  (and (lessp above next)
                       (prehom-seq-1 next s)))))

Adding the Skolem axiom:
      (AND (IMPLIES (AND (LESSP (ABOVE S) NEXT)
                         (PREHOM-SEQ-1 NEXT S))
                    (EXTENSIBLE S))
           (IMPLIES (NOT (AND (LESSP ABOVE (NEXT ABOVE S))
                              (PREHOM-SEQ-1 (NEXT ABOVE S) S)))
                    (NOT (EXTENSIBLE S)))).

     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (EXTENSIBLE S))
          (FALSEP (EXTENSIBLE S)))
is a theorem.

[ 0.3 0.0 0.0 ]
EXTENSIBLE
>
|#

Event: Introduce the function symbol above of one argument.

Event: Introduce the function symbol next of 2 arguments.

Event: Introduce the function symbol extensible of one argument.

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

→ (¬ extensible (s)))

Axiom: extensible-boolean truep (extensible (s)) ∨ falsep (extensible (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.
#| The original DEFN-SK event here was processed as follows:
>(defn-sk good-color-p (c)
  ;; says that arbitrarily large elements of ramsey-seq agree with c
  (forall big
          (exists good-c-index
                  (and (lessp big good-c-index)
                       (equal c (cdr (car (ramsey-seq good-c-index))))))))

Adding the Skolem axiom:
      (AND
          (IMPLIES (AND (LESSP (BIG C) GOOD-C-INDEX)
                        (EQUAL C
                               (CDAR (RAMSEY-SEQ GOOD-C-INDEX))))
                   (GOOD-COLOR-P C))
          (IMPLIES (NOT (AND (LESSP BIG (GOOD-C-INDEX BIG C))
                             (EQUAL C
                                    (CDAR (RAMSEY-SEQ (GOOD-C-INDEX BIG C))))))
                   (NOT (GOOD-COLOR-P C)))).

     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (GOOD-COLOR-P C))
          (FALSEP (GOOD-COLOR-P C)))
is a theorem.

[ 0.2 0.0 0.0 ]
GOOD-COLOR-P
>
|#

Event: Introduce the function symbol big of one argument.

Event: Introduce the function symbol good-c-index of 2 arguments.

Event: Introduce the function symbol good-color-p of one argument.

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

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

Axiom: good-color-p-boolean truep (good-color-p (c)) ∨ falsep (good-color-p (c))

;; 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, 3, 4 above-all, 4 above-all-aux, 3, 4 above-all-aux-monotone, 4

big, 6, 7 bound, 1, 2, 4, 7

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

extensible, 3–5, 8 extensible-boolean, 3 extensible-cons, 4 extensible-intro, 3 extensible-necc, 3 extensible-next-property, 5 extensible-nlistp, 5 extensible-suff, 3

good-c-index, 6–8, 10 good-c-index-non-zero, 10 good-c-index-numberp, 8 good-c-index-wit, 7 good-c-index-wit-positive, 7 good-color-p, 6, 7 good-color-p-boolean, 6 good-color-p-intro, 6 good-color-p-necc, 7 good-color-p-suff, 7

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

p, 2, 4, 9, 10 p-intro, 2 p-num, 1, 2, 10 p-num-intro, 1 p-num-is-p, 10 plus-comm, 9 plus-difference-elim, 10 prehom-seq, 2, 5, 9, 10 prehom-seq-1, 2–5, 9 prehom-seq-1-next-element, 4 prehom-seq-1-next-element-cons, 4 prehom-seq-1-restn, 9 prehom-seq-ramsey, 9 prehom-seq-restn, 9 prehom-seq-restn-commuted, 10

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