Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 18, 1:32 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Tue, 18 Mar 2008 05:43:50 -0500, David C  Ullrich
<dullr...@xxxxxxxxxxx> said:





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.

(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.)

A proof checker for CBL would be a good start, but it would not address
CBL's biggest problem, viz., that it has no significant mathematical
content.

Can you find a flaw in any of the proofs (the intuitive, "actual"
proofs) that I have posted that are generated by CBL? (I will provide
links to some of them if you'd like.)

So you think I wrote them by hand (despite my showing the formal
representations and their formal proofs)? Ok, 3 possibilities:

1. Show that the proofs are published anywhere.
2. CBL is a fantastic theorem prover.
3. C-B is a fantastic theorem prover.

The BS authors claim to have generated or verified (a pointless
exercise that doesn't show any mathematical significance to the
formalism) well-known theorems, but don't even give a formal
representation of the theorem.

Who has ever shown NEW proofs (supposedly generated)?

Who has shown MY proofs?

Who has shown proofs as short?

Peter Smith claims his book has my proofs, but see my reply - his
statements are not so. His proofs are an order of magintude longer
and more complex than mine.

 Even if CB manages to make his system rigorous enough that CBL
proofs are all formally valid, but his theorems still would't have
anything like the content he purports.  You can't just *intend* that,
e.g.,"P(I)" expresses that P is recursive (what *is* that "I" doing
there?); it has to be built upon a recognizable theory of recursive
functions.  You can't just *intend* "TW" to refer to the set of true
sentences of arithmetic.  It needs to be built at least upon a
(presumably arithmetized) theory of syntax.  That sort of
infrastructure, painstakingly developed in legitimate theories of
computatibility, are entirely lacking in CBL.  So any CBL theorem
involving the likes of "P(I)" and "TW", even if clearly formally valid,
is entirely lacking in genuine content.

Why the *** is a valid proof of a mathematical theorem lacking in
content?

See Turing 1937.

C-B
.