Re: Godel proved maths inconsistent not incompleteness theorem

On Tue, 18 Mar 2008 17:32:19 +0000 (UTC), Chris Menzel
<cmenzel@xxxxxxxxxxxxxxxxxxxx> wrote:

On Tue, 18 Mar 2008 05:43:50 -0500, David C Ullrich
<dullrich@xxxxxxxxxxx> said:
On Mon, 17 Mar 2008 18:28:27 +0000 (UTC), Chris Menzel
<cmenzel@xxxxxxxxxxxxxxxxxxxx> wrote:

On Mon, 17 Mar 2008 09:58:29 -0700 (PDT), MoeBlee
<jazzmobe@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. 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.

There's that too.

Which is amusing, given the way he goes on about how actual
proofs by others don't contain proofs that they actually prove
what they intend to prove...

David C. Ullrich
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... because he has no clue what a formal theory *is*. ... Of course he could prove us wrong by writing that CBL proof ... listing of a computer program, and its output, that generates 27 ... appreciating the actual mathematics he's groping toward. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... ...the ZF axioms aren't used to prove anything outside of simple, ... And still unable to see that CBL is just Magickal Thinking. ... because he has no clue what a formal theory *is*. ... appreciating the actual mathematics he's groping toward. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... because he has no clue what a formal theory *is*. ... Of course he could prove us wrong by writing that CBL proof ... that your proof generator doesn't need a proof checker. ... David C. Ullrich- Hide quoted text - ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... And still unable to see that CBL is just Magickal Thinking. ... simply because he has no clue what a formal theory *is*. ... A proof checker for CBL would be a good start, ... it has to be built upon a recognizable theory of recursive ...
    (sci.logic)
Loading