Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 15, 2:10 pm, William Hale <h...@xxxxxxxxxx> wrote:
In article
<ddbba146-65a3-4ab8-af3f-a762e1910...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,

You are erroneously equating two things that are at different levels
of abstaction.  Recursion Theory is a specific system (which I
axiomatized) but "Set Theory" is a collection of systems (ZF, NBG,
etc.)  There's no such thing as "axiomatized Set Theory".  We can
axiomatize ZF or NBG etc.  I gave the CBL formalization of axioms for
ZF.

I am utterly confused. I don't know where to begin.

I think that Set Theory is a bad branch of Computer Science to use to
learn CBL. It is not well defined and you have to either pick one of
the axiomatizations (e.g. ZF) or make up your own. You axiomatize a
set of theorems. But the theorems of "Set Theory" are not well-
defined, and we need either a detailed informal description of those
theorems or a set of axioms that defines those theorems.

I guess this is all because Set Theory is so abstract. That is, (1)
the theorems are unclear, (2) those who have tried to clarify what the
theorems are with axioms disagree and so there are (at least) a dozen
axiomatizations to choose from.

I have answered the easier questions below, but this is a bad starting
point, I now realize (believe.) I can illustrate CBL with another
branch of CS, or get back to writing it up in detail.

Maybe it's time to put something on my empty home page and people can
help make it intelligible with the functionality of a web site to help
us.

I do thank you so much for taking the time and you have shown me a
lot.

"We can prove that using simple general useful axioms: EQ(I,x)  For
every thing, there is a set that contains only it. . . ."

I am utterly confused. I don't know where to begin.

So you have this axiom: EQ(I, x).

How does this relate to ZFC?

It is a CBL axiom that will help us prove some of the theorems proven
in ZFC. So it is a step in axiomatizing ZFC. (If ZFC is formal, then
the job is easier. For example, we can just prove the axioms of ZFC
and make sure CBL has the Rules of Inference that ZFC has to create
theorems.)

Do I still have the axioms that ZFC give as axioms when stated as a CBL
statement? That is, are the statement in CBL of the axioms in ZFC still
axioms within CBL? Since EQ(I,x) is not an axiom of ZFC, are you adding
that to the list of axioms for the formalization of ZFC in CBL?

Yes, EQ(I,x) is an axiom in the formalization (axiomatization) of ZFC
(whether ZFC is already formal or axiomatic - the job is still to
produce its theorems.) It says that for every thing there is a set
that contains just it.

From below, it appears that you are proving the statement in CBL of the
pairing axiom in ZFC. Why do you need to prove it? Isn't it already an
axiom?

It is an axiom in ZFC. In CBL I prefer to have more primitive axioms
than ZFC. But, as I said, we could just express the ZF axioms in CBL
instead of trying to improve them. The whole point is to produce the
same theorems as ZFC but using the formal wffs and rules of CBL.

Oh heavens no.  With all due respect, your understanding is not
accurate.  When we formalize a system, we produce the same theorems
and proofs, only we in effect give an algorithm to enumerate them,
rather than describing something informally.  So you have the same
system, although formally defined.

I think you are using "formalize" in a different meaning than I have.

Formalize means to give expressions that exactly define what a system
does. Axiomatize is a special case, meaning to show axioms and rules
of inference that produce true stratements regarding a particular
subject.

I think it would be hard to develop an axiomatization that only
generates known theorems.

I am utterly confused. I don't know where to begin.

You said you didn't want any new theorems.

So you developed CBL to generate new theorems, but it cannot generate
known theorems?

Not that it can't but that it's not very interesting or educational to
prove statements that are already known using proofs that are no
simpler or better than what already exists.

I am willing to generate the proof by hand of one or two
known theorems if only I understood how to use CBL. I am not asking
whether the program you wrote to do CBL generation of proofs can/does
generate proofs of known statements. Or, are you saying that I cannot do
proofs by hand in CBL but must use the CBL proof generating program?

There is no CBL proof generating program operational right now. I
hope and expect to be able to produce such a program with the help of
volunteers (6-8 have volunteered over the last few years) using a web
site (my name) to organize this and related activities.

You can certainly prove theorems by hand using CBL. That's what I do
and there is no way that I could have created those theorems without
CBL.

It would have to interface with a database
of existing theorems and be updated realtime!

I am utterly confused. I don't know where to begin.

I was joking about how I would avoid those known theorems that you
said that you didn't want to generate.

Is CBL a proof system? I don't need a database of existing theorems to
start to give proofs of statements. Give me the axioms and syntax and
rules, I will do my own private proofing of statements.

Unless you tell me that you don't want to generate new theorems.

Or, are you saying that you need the collection of theorems already so
that CBL can do something with them?

I personally need to know the theorems that I am trying to generate.
That is step one in axiomatizing.

(Of course, there are
people who claim they have such a database, that is if you choose to
accept statements of a Mathematical nature but without the necessary
proof.)

I am utterly confused. I don't know where to begin.

There are web sites with projects to list all Mathematical facts known
to man.

Are you saying that when I accept a statement of Mathematical nature as
an axiom without any proof, then that is wrong and that the stated axiom
without proof so be provided with the necessary proof?

No, axioms are axioms. I just need to produce the same theorems as
the system being axiomatized (as close as possible, anyway.)

Yes, although it is not a relation.  Did you know that?  Why is it
not?

I already said I am not assuming anything at this point. I am asking
what CBL assumes or takes for granted at this point.

Not much, really. You have to supply the axioms and rules, and that
depends on the branch of CS that you are in.

What is "SE(x,y)" ?

The relationship that holds iff y is an element of set x.

Let me take another approach. I don't know how to "speak" in CBL and you
won't tell me what the syntax, rules, axioms are.

I've done that at least 2 or 3 times in this thread and perhaps
another that was referenced or was active at the same time.

So I will say some
things as a child would when trying to learn to speak and have the
parent correct him.

For examples:

I say: "SB(x,y) means set y is a subset of set x."

I say: "CT(x,y) means set y contains element x."

I say SE(y,x).

I say" "HF(x,y) means field y is Hibert class field of field x".

I have no idea whether those are acceptable statements in CBL. Those
three statements make the same sense as your statement "SE(x,y) means y
is an element of set x". Can I make such statements in CBL as these
three statements that I gave. I have no idea.

We are defining relations as if we were Mathematicians.

Define "less than" and I will use your fav format.

I am utterly confused. I don't know where to begin.

If I could see how you define a relation then I will follow that
format.

I am not asking you to define x and y.

Anyway, without going in to the gory details, let's start with:

Definition. "a less than b" means "(Ec)(b = a + c and not (b = a))"

Definition: SE(x,y) means y is an element of set x.

If that were the case, then Mathematics would be in quite the
quagmire!

When I work in ZFC, I don't take "y is an element of set x" to mean
anything (except informally).

You use infix notation y e x and I use relational notation SE(x,y).

The meaning in ZFC of "y is an element of
set x" is obtained from the axioms.

And the fact that "y e x" or "SE(x,y)" stands for "y is an element of
set x" is obtained from our definitions.

But, I think this is one of your
points: current Mathematics is in quite a quagmire because they take
this point of view, rather than actually showing what they prove
corresponds to what they think they are proving.

Actually, I was responding to your comment that we can't refer to "is
an element" until we've set up axioms for it. But you can put it all
together in any order you want, and all that counts is when you 're
finished.

You are starting to sound like those idiots who waste time fighting
over syntax - and when I say, "Whatever syntax you want is fine." they
argue with that!  (Not that you're an idiot necessarily.)

You don't see that I am utterly confused? Part of the confusion is that
you and I are using the same words in different meaning (which you want
to dismiss as fighting over syntax). I am willing to try to learn your
syntax, but I am not picking it up.

What different meanings?

I am not even sure what CBL is trying to do.

Generate theorems of theoretical Computer Science (which is more or
less Metamathematics.)

I thought CBL was a
replacement for ZFC like NGB is a replacement for ZFC.

You can use whatever system you want. You can certainly set up axioms
that talk about set membership in CBL, as I did for ZF.

You seem to say
that I am wrong to view it this way. Ok, so I made some progress and
won't view CBL as a replacement fro ZFC.

"The development of mathematics towards greater exactness has, as is
well-known, lead
to formalization of large areas of it such that you can carry out
proofs by following a few
mechanical rules." - Kurt Godel, 1931

But, since I am interested in
proofs of statements, I don't know how to do that in CBL or whether I
should even be trying to work out proofs of statements in CBL.

See my examle proof of Pairing.

My current understanding is that CBL proves statements about what can be
proved in ZFC (say, for example). So, for example, CBL does not prove
that the union of two sets is commutative; rather, CBL proves that there
is some statement phi in ZFC such that phi cannot be proved and ~phi
cannot be proved.

No. CBL proves its own theorems without reference to other systems.

I gave the CBL representation of ZF.  Is there something else you
want?  Do you want me to develop a new system of Mathematics (rather
than formalizing an existing one)?

I am utterly confused. I don't know where to begin.

I don't want you to do anything except explain what CBL is.

It is an extension to Mathematical Logic that allows us to prove a lot
more with shorter proofs that are also formal.

I thought the set theory in CBL (number 5 item) was a replacement for
ZFC. Now I see that you are not doing that.

CBL formalizes existing systems.  See above.

I am utterly confused. I don't know where to begin.

You formalize formal systems?

An axiomatization is a formalization, of a system that may be formally
or informally given.

C-B
.

Relevant Pages
Loading