Re: Godel proved maths inconsistent not incompleteness theorem

On Mon, 24 Mar 2008 10:29:44 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> wrote:

On Mar 18, 6:43 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Mon, 17 Mar 2008 18:28:27 +0000 (UTC), Chris Menzel





<cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Mon, 17 Mar 2008 09:58:29 -0700 (PDT), MoeBlee <jazzm...@xxxxxxxxxxx>
said:
On Mar 16, 8:01 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Sat, 15 Mar 2008 01:25:35 -0700 (PDT), Charlie-Boo
<shymath...@xxxxxxxxx> said:

...
...the ZF axioms aren't used to prove anything outside of simple,
fairly obvious, statements about sets.

Ignorant codswallop. I gave you three examples (of thousands):

1. Every singular limit ordinal k with cofinality < card(k) lacks the
Souslin property.

2. The Stone Representation theorem (every Boolean Algebra is isomorphic
to a field of sets)

3. Every normal function on the ordinals has arbitrarily large fixed
points.

(Refutations welcome.)

Where "welcome" = "ignored".

Wow, Charlie-Boo is STILL making that challenge and IGNORING replies.

And still unable to see that CBL is just Magickal Thinking.  E.g., in
CBL, "P(I)" just *means* "P is recursive", where "recursive" appears to
be an undefined primitive; "YES(x,y)" just *means* "Turing Machine x
halts yes on input y", but one looks in vain for the definition of a
Turing Machine and what it is for one to halt on a given input.  Simply
*declaring* those expressions to mean the complex concepts that he
intends them to mean is his idea of an adequate formal theory, simply
because he has no clue what a formal theory *is*.  

So it would appear.

Of course he could prove us wrong by writing that CBL proof
checker - that would prove that CBL is in fact "formal" in the
required sense.

So all of the authors who haven't done that are bullshitters, huh?

No, just you.

I don't see the point to any of your comments below. You explain
that your proof generator doesn't need a proof checker. I never
said it did. A proof checker would prove that in fact CBL _is_
a "formal" system. It would answer various people's complaints
about vagueness.

And if CBL actually _is_ sufficiently well-defined to be an actual
formal system then a proof checker would be trivial to write.

Axiomatic Theorem Proving doesn't involve doing a syntax check against
purported proofs. (BS authors will claim they "verified" a particular
proof, unable to BS their way to saying they "generated" it - a
pointless exercise.)

If you don't believe me, read

http://selfref.googlegroups.com/web/A%20Simple%20Generator%20of%20Incompleteness%20Theorems.pdf?gda=6wgFpmIAAAD6Y2To0LQBjcOuo8Q63uZ_lQA4SGAGq6yCh-5864Yyx2G1qiJ7UbTIup-M2XPURDQzSDmKMzn3Sg8-2GbVvdi117y3W4zJ8GbL7WWaTD9l9Ko2dOZBEuzU2DVNzz0QUbvKHSFV3pq93kT4KvIWNWYO&hl=en

That is an article that I published a few years ago which includes a
listing of a computer program, and its output, that generates 27
theorems from the Theory of Computation with no input from the user.
I include a check-sum function that allows you to check for typing
errors when entering the program into your computer.

See, no need for a proof checker.

(Not that CB cares, but the point is that the axioms and rules
need to be clearly defined, and clearly defined _only_ in terms
of the _syntax_, with no reference to what anything "means",
so that one can determine whether a proof is correct by just
looking at the syntactic structure of the lines in the proof,
_without_ knowing what anything "means".

Which of course is exactly why writing a proof-checker
would be compelling evidence that we're all wrong about
CBL, because the computer _doesn't_ know what anything
means.)

But instead of
educating himself -- he certainly seems smart enough to learn the
material -- he appears to be stuck in the illusion that his work is
simply too innovative and original to be accepted by a mathematical
community that is blinded by its ossified traditions.  Pity that.  I
mean, I'd really *like* the guy to have the pleasures of learning and
appreciating the actual mathematics he's groping toward.  I guess that's
why I keep responding in off moments.

David C. Ullrich- Hide quoted text -

- Show quoted text -

David C. Ullrich
.

Quantcast