# Re: Constraints and Functional Dependencies

Date: 24 Feb 2007 08:09:28 -0800

Message-ID: <1172333368.439634.100140_at_t69g2000cwt.googlegroups.com>

On Feb 24, 6:18 am, paul c <toledobythe..._at_oohay.ac> wrote:

*> Marshall wrote:
*

> > ...

*> > In a data management context, there is some value to restricting
**> > what we can quantify over as being only attributes of declared
**> > relations (whether variables or constants.) So, we can't express
**> > the "no-upper-bound" property of the natural numbers; they aren't
**> > a database table so we can't quantify over them.
**> > ...
**>
**> Thanks for a theory topic at last. Minor question - is it not rather
**> that we can express it, but agree not to because we can't always compute it?
*

In response to that, I proposed some specific restrictions on range variables that actually do make it impossible to express. But it's true that expressing it using standard quantifiers is no problem.

not exists n in N: forall m in N: n > m

I believe there are software systems that can work with expressions of this form. I don't know whether they could automatically find a proof of this specific formula, but I suspect they could if you prodded them enough. They could certainly verify a supplied proof.

> eg., if n is not infinite, just has a finite number of values, wouldn't

*> R(n) OR NOT R(n) enumerate all possible values of n?
*

Marshall Received on Sat Feb 24 2007 - 17:09:28 CET