Search the archives, you idiot! Or shut up!

On Jul 20, 7:54 pm, "Jesse F. Hughes" <je...@xxxxxxxxxxxxx> wrote:

<snip more *** from Jesse's bad memory = Jesse's ass>

You keep saying you searched your "memory" and "evidence".

And from _that_ basis, you feel good about yourself? You're a fucking
joke.

Look Jesse, you are clearly just too dumb to search the archives.

Your Google search was lame and cursory.

Your memory is faulty.

Do your homework BEFORE you open your mouth, you ***!

I CAN SEARCH THE ARCHIVES to back up what I said. Obviously, my
ability to search the archives is better than yours. And clearly my
memory is better than yours.

Why won't I *prove* what I said? Because YOU ARE THE IDIOT who took
the position of knowing the "truth" of Quinn's postings, YET you can't
find a single posting of Quinn related to Quinn's asinine "closed
list" statement.

Quinn Tyler Jackson used a lame "closed list" argument to bull***
this newsgroup regarding James Harris.

Anyone who denies Quinn said it is a complete imbecile.

C'mon Jesse, find ONE SINGLE POSTING of Quinn's regarding his "closed
list" statement.

You CAN'T? You ARE UNABLE TO? (snicker)

Oh look! Here's a totally arbitrary and intentionally irrelevant post
I found. Where? From my memory? From my imagination? From a well
of lies? No, you dumb *** Jesse F. Hughes, it's FROM THE ARCHIVES.

Do you deny that these are your words (for a totally irrelevant
topic)?


Subject: Yes, proof checkers exist!

Jesse F. Hughes wrote on January 1, 2001, 2:44 AM

<bran...@xxxxxxxxxxxxx> writes:
There seems to be some confusion about the differences between a
proof checker and a theorem decider. From what I can gather from the
posts, we are taking a "proof checker" to be a program that simply
verifies the *syntactics* of a set of symbols, whereas a theorem
decider verifies the *semantics* of a set of symbols.
I don't have any idea about verifying the "semantics" of a set of
symbols in the way you indicate. I think you've introduced a
distinction that doesn't match my distinction. I also think that I
added to the confusion with a post in which I didn't define my terms.
So here they are:
A proof checker would, when given a purported proof, verify that the
proof is valid. This is a trivial task (assuming, of course, that
our
set of axioms is decidable, but this is perfectly reasonable).
A theorem decider would, when given a formula, determine whether the
formula is a theorem (of, say, ZFC). This puppies don't exist, for
well known reasons
(Obviously, I've sketched the definitions above very informally, but
I
hope they suffice. I will elaborate if necessary.)
Assuming that I've got the definition correct, we can still use the
Halting Problem here. One of the implications of the Halting Problem
is that *no* program of sufficient complexity can be proven correct
*semantically*, that is to say, we can never be sure that a program
does what it is supposed to do.
That does not look like an implication of the halting problem as I
understand it. What is "sufficient complexity" of a program? Does
this implication yield difficulties for current work in program
verification?
--
"The extra care that's needed for such expressions has been turned
into
a statement that they can't be used at all in factorizations because
the position is that I haven't proven that once I am no longer using
polynomials that factorizations are still non unique." -J. S. Harris

.