Re: Godel proved maths inconsistent not incompleteness theorem

On Sat, 3 May 2008 19:50:10 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> said:
On May 3, 6:21 pm, William Hale <h...@xxxxxxxxxx> wrote:
In article
<dda4ff27-1c83-42df-9fe2-190767f65...@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,

Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On May 3, 11:43 am, "Jesse F. Hughes" <je...@xxxxxxxxxxxxx> wrote:
Charlie-Boo <shymath...@xxxxxxxxx> writes:
No. I never said that's how a proof checker works.

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.

Here's the quote in context:

,----
| > I'd love to see them.  Where can we download them?  But you *do*
| > realize, don't you, that all we're talking about here is proof checking?
| > And you do understand there is a huge difference between proof checking
| > and theorem proving, right?
|
| 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.
|
| So you think hard things are easy and easy things are hard.
|
| That's what an algorithm looks like.  So now you should be able to
| give the complete spec and code.
`----

Sure looks like you're describing how a proof checker works.  If not,
what point were you trying to make when you described such a
***-stupid algorithm?

Refuting his last 9 words with a ***-stupid algorithm.  (Does that
mean he's ***-stupid?)

But, the given algorithm is not correct to check that a proof is valid.

Your algorithm shows that each line of the proof is correct.

No, they are not provable using only the lines above it. I am
extending the proof generated by one step each time and seeing if the
next step is among the possible next steps in a proof that has the
lines so far as its first steps.

It's rather trivial and shows the difference between generating and
verifying proofs is trivial, not "huge".

But your algorithm does *not* verify *proofs*; it doesn't have a thing
to do with proofs. All it does is tell you that a list of theorems is a
list of theorems.

It's just enumerating vs. semi-deciding it. The relationships between
them are simple and well-known. It seems that some (perhaps many)
people don't even see that simple fact.

No, everyone's clear on that elementary fact. You, however, still have
no clue what a proof checker is.

.

Quantcast