Re: SUO: IFF example?
On Fri, May 02, 2003 at 02:00:27PM -0700, Adam Pease wrote:
> >I believe that SUMO and OpenCyc are in fact not logically consistent
> >overall, but there may be portions that are consistent, or can be
> >made so with small modifications.
>
> Do you mean that they are not mutually consistent, or that they are
> not internally consistent? I suspect the former is true, to some
> degree,
Truths about consistency don't really come in degrees, Adam. Your
theory is consistent or it isn't.
> we have done proofs for consistency within specified time boundaries.
What is consistency within a specified time boundary? Would this be the
idea: a set A of sentences is consistent within a boundary of 50 if no
proof under 50 steps contains both a formula and its negation. Is that
right? If so, how would one go about proving such a thing?
> We found and removed inconsistencies found in up to 50-step proofs.
I do not understand this result at all. If you find an inconsistency in
a proof, there's no "removing" it. You just stop asserting its
premises (and you hopefully find which premises are false).
> We can run for days now without finding anything, so we have some
> degree of confidence that SUMO is internally consistent.
I think that is a wholly unwarranted conclusion -- at most it seems to
provide some justification for the (still perhaps significant)
conclusion that many useful subsets of SUMO are consistent.
-chris