Re: Godel proved maths inconsistent not incompleteness theorem

On Sat, 3 May 2008 08:22:41 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> wrote:

On May 1, 7:56 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Wed, 30 Apr 2008 01:54:34 -0700 (PDT), Charlie-Boo

<shymath...@xxxxxxxxx> wrote:
On Apr 28, 12:39 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx>
wrote:
[...]

Yeah.  For each line of the purported proof you have to run the
theorem prover for one step and see if any of the theorems proven
equals that line.

1. For each line in the purported proof
 a. Run one step of the theorem prover
2. For each theorem generated, compare it to the theorem at that line.
3. If equal, then go to the next line (1)
  a. If no more lines, the proof is valid.
4. If no more theorems to generate, the proof is not valid.

My god this is simply incredible. After people have posted
trivial proof=of-concept examples and pointed you to
industrial strength examples elsewhere you still think
that _this_ is how a proof checker works?

No. I never said that's how a proof checker works.

Huh? This was in the middle of a discussion of proof
checkers. You said "For each line of the purported proof
you have to...". Not even "you could...", but "you
have to".

Nice try. Unfortunately for your credibility in all this
people can see what you actually wrote.

As long as you're commenting on people's comments
on your awesomely stupid post, someone should
point something out that I guess nobody thought
of a few days ago: Not only is your outline above
incredibly stupid, it also simply won't work. The
problem being that there are (in certain circumstances)
infinitely many possible nest steps for a theorem
prover, so if the next step never verifies that the
next line is ok we have an infinite loop.

Giggle.

One last time: If you think something is stupid etc. first consider
the possibility that you are simply misinterpreting what is being
said. Follow the discussion closely.

I guess it's now clear why you think that various previous
descriptions of how such a thing would work were incomplete:
they didn't mention any of the nonsense above. The reason
is that the nonsense above is the worst possible method
to write a proof checker - the sketches you were given
_were_ complete, you just thought otherwise because
you had this incredibly awful plan in mind.

This reminds me of something James Harris did once:
He was showing us an algorithm to calculuate pi(n),
the number of primes <= n. At one point he needs
to test whether x is prime. He does that by noting
that x is prime if and only if pi(x) > pi(x-1) and
so he calls his pi routine recursively to check
primality.
[...]

David C. Ullrich
.

Relevant Pages