Re: Godel proved maths inconsistent not incompleteness theorem

On Sat, 03 May 2008 17:21:43 -0500, William Hale <hale@xxxxxxxxxx> said:
In article
<dda4ff27-1c83-42df-9fe2-190767f65a4a@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,
Charlie-Boo <shymathguy@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.
...
... your algorithm doesn't show that, for each line of the proof,
the line is an axiom or the line follows from some previous lines of
the proof by the rules of inference of the system.

Huh, you're right. It's not even a proof verifier for valid proofs.
It's just a list-of-theorems verifier: If you've actually got a list of
theorems, it will tell you (eventually!); if you've got a non-theorem on
your list, it never halts. Nice.

.

Relevant Pages

  • Re: Congruence based factoring algorithm
    ... algorithm will run faster with as small a p as possible; ...    report that T is prime ... Can you prove an upper bound on the numbers for which the effect can ... so it's equivalent to a brute force technique as a k that works gives ...
    (comp.theory)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... | equals that line. ... For each line in the purported proof ... | That's what an algorithm looks like. ... theorem generator a check that each theorem generated must equal the ...
    (sci.logic)
  • Re: Searching substrings in records.
    ...     for each text field in the record ... but I just can't tell the difference between the algorithm ... you introduced above and the brute force approach I described on the ... every record and perform a substring search on any of them. ...
    (comp.programming)
  • Re: Lotto 7/45
    ...   if) ... Therefore there should be an algorithm that 3 times of random ... I want an algorithm by which a 27 bit random integer suffice to make a ...
    (comp.programming)
  • Re: Minimal enclosing Triangle
    ...       is much larger than what your application uses. ... I'm pretty sure the algorithm I mentioned is only a couple of factors ... essential to understand the pseudocode. ... if not, vertex C is twice the height of a-1, but on side B ...
    (comp.graphics.algorithms)
Quantcast