Re: [Hol-info] Proof related to REAL_BIGNUM

[John H. <Joh...@cl...>]

Hi Osman,

| I am trying to prove the following theorem in HOL
| 
| |- ?(n:num). !(r:real). r < & n

In fact this is false. If there were such a number n, then in
particular we would have &n < &n, which is impossible. Here's a
proof of the negation (in HOL Light):

 MESON[REAL_LT_REFL] `~(?(n:num). !(r:real). r < & n)`;;

| It is somewhat related to the REAL_BIGNUM theorem found in the realTheory:
| 
| |- !r. ?n. r < &n

Right, this is known as the Archimedean property of the reals. The fact
that one is true and the other false just shows how critical the nesting
order of quantifiers can be.

Were you just trying to prove the above claim out of curiosity, or
was it meant as a lemma on the way to something else? If the latter,
perhaps someone can help you with what you really want to prove.

John.