Re: SUO: IFF example?
On Sat, May 03, 2003 at 11:14:30PM -0700, Adam Pease wrote:
> >> 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?
>
> Automated proof is a search, so one can simply terminate the search
> after a certain amount of time, if results haven't already been
> returned.
I think I misread your original assertion. I *thought* you were saying
that you had some sort of (meta)proof that proofs under 50 steps have
some sort of consistency property, e.g., as noted, that no such proof
contains a statement and its negation. But all you seem to be making is
the much more modest claim that you have a procedure for terminating
proofs after, say, 50 steps if an inconsistency hasn't been found and a
desired conclusion hasn't been reached.
> >> 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).
>
> Yes, that's what I meant by removing the inconsistency. When we've
> discovered an inconsistency, that has alerted us to an axiom that was
> incorrect, so we change the axiom and that removes the inconsistency.
> Since such a change could introduce a new inconsistency, it's
> necessary then to rerun the consistency check.
Ok, that makes sense.
-chris