Re: FOL/HOL: is there a middle ground?
Date: 18 Jul 2004 21:31:03 -0700
Message-ID: <3638acfd.0407182031.584a46fa_at_posting.google.com>
"Marshall Spight" <mspight_at_dnai.com> wrote in message news:<q9AKc.114259$IQ4.31025_at_attbi_s02>...
> There are clear incompleteness problems associated with allowing
> the definition of set A to references the definition of set A. What
> are some of the other problems with using HOL as a basis for
> a relational algebra?
To put it succinctly:
(a) the relational model fundamentally depends upon the notion of
equality, but
(b) deciding whether two relations are equivalent is undecidable
in general.
Note that trying to answer (b) by just using name equivalence
doesn't work:
> Is there a middle ground, above FOL but
if p(X) <=> X mod 2 = 0
and q(X) <=> 2 in {Y | Y is a factor of X}
then p and q are certainly equivalent. But deciding this sort
of thing in general would mean solving the halting problem.
> below fully-recursive definitions, that is more expressing
> than FOL but still consistent?
Welllll, you could restrict yourself to purely finite relations, but that puts a serious crimp in the utility of the idea.
> What are the various pitfalls one runs into with recursively
> defined relations? Can we enumerate the "holes" and plug
> them all with restrictions on our fractal order logic?
'Fraid not. You can't even begin such a task.
Can you explain why you would want this level of expressive power?
- Ralph