[Bug 1612] what is the quantification of unbound variables?

From: <bugzilla@wiggum.w3.org>
Date: Mon, 25 Jul 2005 20:47:49 +0000

Cc:
Message-Id: <E1Dx9rZ-0004CL-QQ@wiggum.w3.org>
```
http://www.w3.org/Bugs/Public/show_bug.cgi?id=1612

Regarding this thread, I think that my suggestion that inferences
are patterns representing all possible substitutions for the
variables would handle my concern, and simultaneously convey
the correct part of additional comment #1.

Regarding the
use of "1 <= i <= n", I think the proposal in additional
comment #3, to write this on a separate line to avoid the
appearance of a quantifier, is a good one and should be
accepted.  I am personally indifferent whether it is expressed
as 1 <= i <= n or i in {1, ..., n}, since, as a mathematician,
I regard "for all i in {1, ..., n}" as just a much a
quantifier as "for all i, 1 <= i <= n".  The important thing is
to get the judgment on its own line.

It would also help if section 2 somewhere explicitly considered
this notation.  Using my convention that every inference is a
pattern,  the inference

dynEnv |- Expri => false
1 <= i <= 2
------------------------
dynEnv |- Expr1 and Expr2 => false

is a pattern for inferences such as

dynEnv |- (\$a = \$b) => false
1 <= 1 <= 2
------------------------------------------
dynEnv |- (\$a = \$b) and (\$c = \$d) => false

and

dynEnv |- (\$c = \$d) => false
1 <= 2 <= 2
------------------------------------------
dynEnv |- (\$a = \$b) and (\$c = \$d) => false

Regarding the proposal that ellipses be used instead of universal
quantification in inferences, I find this acceptable with two
provisos:

a) document it.  Jim relayed to me that someone thought this
was already well understood, but what does it cost you to
write a paragraph about a convention?

b) you must examine every premise with universal quantification
and decide whether the vanishing case is permitted (ie,
the upper bound is 0 and there are no cases at all), or
alternatively the minimum for the upper bound is 1.  See
my comment #1737 about the inference in 8.1.10 "Union type of
derived types".  After much inferencing on my own part, I concluded
that the ellipsis 1 ... n is permitted to vanish (n = 0)
whereas the ellipsis 1 ... m is not permitted to vanish
(m > 0).  So it seems that there is something to explain