Re: Major inconsistencies in Table 10.7 with unbounded intervals
On 2015-02-14 13:09:53 +0000, John Pryce wrote:
> If people agree that Vincent's suggestion solves the problem, I
> suggest to add to the paragraph "The “set” and “bound” columns in
> Table 10.7..." (p39/14) a sentence saying the sets are compactified
> in the relevant cases. Vincent, will you provide the text?
I suggest:
To interpret the "set" column, the intervals must be compactified,
i.e. the bounds are added to the intervals (this matters only for
-inf and +inf).
> However is there another solution? Suppose we change the set
> definition of "starts" from
> exists_a forall_b a\le b (aa has a lower bound for bb)
> exists_b forall_a b\le a (bb has a lower bound for aa)
> exists_b forall_a a<b (bb has a strict upper bound for aa)
>
> by switching the quantifiers of the first two phrases, to
> forall_b exists_a a\le b (bb has NO strict lower bound for aa)
> forall_a exists_b b\le a (aa has NO strict lower bound for bb)
> exists_b forall_a a<b (bb has a strict upper bound for aa)
>
> and similarly for the other three offenders. Does that work?
Yes, this seems to work. This is probably better.
> Maybe some help from a theorem-prover package would be useful. Nathalie?
This would be useful to make sure that everything is correct.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)