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>,





 Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On Mar 15, 10:55 am, William Hale <h...@xxxxxxxxxx> wrote:
In article
<fe25bfeb-8804-4891-8374-e3dbefaa6...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,

 Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On Mar 14, 11:20 pm, William Hale <h...@xxxxxxxxxx> wrote:
In article
<9df49f3b-9476-475f-97c8-ffc2c184f...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>, Cha
rlie
-Boo <shymath...@xxxxxxxxx> wrote:

[cut]

And if my description is in fact poorly written, tell me what wording
is unclear.  I will glady - eagerly - try to make it more
intelligible.

I find it hard to understand CBL because you usually give all the
things
that CBL can do. Such a presentation forces me to try to see how all
that fits together and raises questions for me that concern this
inter-relation between all these things. But, I would prefer to
concentrate on just one of the things that CBL can do and work from
there.

I would like to chose "Set Theory" of the many things that CBL does.
I think it would help to present CBL with regards to "Set Theory" only.

I quote from a former post of yours:

Former?  I haven't disavowed it.

==========================
5. Set Theory
We can state most of the standard axioms of Set Theory pretty easily.
Many are theorems from more primitive axioms than those given in
print.  For example, Pairing is theorem EQ(I,x)vEQ(J,x) from axioms
EQ(I,x) for every thing there is a set that contains just it, and P,Q
=> PvQ the union of two sets is a set.  Comprehension is P/SE , Q/TW
=> P^Q/SE.
When you formalize these axioms in CBL you notice that they refer to
other mathematical objects like functions and wffs, without giving
axioms (formal definitions) for them.  And remember that not being
exact about what a wff consists of is what gets us in trouble with the
Russell Paradox.
==========================

Request 1: What is the starting explanation of how CBL does "Set
Theory"?

You mean how do I generate theorems of set theory?

No. I am not interested how CBL generate theorems of set theory. I want
to generate theorems of set theory by hand, using the axioms and rules
of CBL for set theory.

That's the same thing.

I can but don't
bother to, really.  I mention Program Synthesis, Theory of Computaton,
Recursion Theory and Incompleteness in Logic (Proof Theory) as 4
systems that I have axiomatized.

But, the quote of yours that I gave above says that "5. Set Theory" is
one of the things formalized by CBL.

Read the first sentence: "We can state most of the standard axioms of
Set Theory pretty easily."  You have to indicate which system.  I
referred to "the standard axioms" as if that constitutes a single
system.

I am confused. You say that you can
state at least one axiom of the standard axioms of Set Theory and that
it is a theorem in CBL. Doesn't this mean that it is derived from the
CBL axioms for Set Theory and that the derivation uses the rules of CBL
for deriving theorems? I am asking you what are those axioms and rules
that CBL use to derive theorems in the CBL axiomatization of Set Theory.

I just gave all of that.  I don't have a separate axiomatization that
is different from ZF or anything else.  That would entail developing a
new system of Mathematics, rather than the formalization of an
existing one.  That has no real relevance.

Are you saying that you have axiomatized Program Synthesis, Theory of
Computaton, Recursion Theory and Incompleteness in Logic (Proof Theory),
but that you have not axiomatized Set Theory?

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.

Try this: CBL is an axiomatic system. It's theorems are about
Metamathematics instead of Mathematics.

The rest is just looking at the Axioms, Rules of Inference and
Theorems, and comparing the proofs to that published. You will find
the published proof typically 2-10 times as long (and never shorter.)

C-B

First we have to show the system that is to be axiomatized, then we
can talk about axiomatizing it.

To formalize Program Synthesis et. al. is to formalize an existing
system.  "Set Theory" is not an existing (well-defined) system.  It is
intuitive and there are dozens of alternate systems, each with its own
set of axioms.

I could also think of new systems (more alternatives to ZF), but then
I would be making up a brand new system, and formalizing that, rather
than just formalizing an existing system.  I've thought of doing that,
but developing a new system of Mathematics has nothing to do with
axiomatizing an existing one, which is what CBL does.

If so, then I will have to
reread your post where I got that "5. Set Theory" segment from. I really
thought that number 5 was on the same footing as number 1 through 4. Do
you see how I might have gotten confused?

Yes, by not realizing that "Set Theory" is actually a collection of
multiple distinct systems and we axiomatize individual systems.

You wrote above (which is the main topic being discussed in this
subthread):

===============
And if my description is in fact poorly written, tell me what wording
is unclear.  I will glady - eagerly - try to make it more intelligible.
===============

As I say, I took item 5 to be on the same footing as items 1 to 4. Is my
reading comprehension so bad that I did not understand what you wrote?

Is it clear when you direct your attention to the first sentence, as I
suggested above?

Or, does your description need to be made more intelligible?

When people talk about the ZF
axioms, I sometimes mention (as above) that most of these axioms are
easy to represent, and as in the case just mentioned, I sometimes show
how some of the ZF "axioms" are CBL theorems.

I am confused again. How can you show a statement of ZF is a theorem of
CBL without having axioms and rules that are being applied?

No axioms or rules??  What do you think this means:

"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?

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?

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?







and

"Thm. Pairing Axiom  EQ(I,x)vEQ(J,x)  There is a set that contains
every value that is equal to I or equal to J.
1. EQ(I,x)  Axiom: For every thing there is a set that contains only
it.
2. EQ(J,x)  SUB 1  For every second thing there is a set that contains
only it.
3. EQ(I,x)vEQ(J,x)  There is a set that contains all values equal to a
given thing I or a second thing J.
    qed"

It is not a big interest because nothing new is generated.

But, if I am going to embrace CBL, then I will replace ZFC Set Theory
with CBL Set Theory,

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.



Now, if you maintain that ZF is formal, then fine.  (There is a
problem, though, in that there are many different syntaxes and even
semantics used to represent the axioms!)  Then CBL would be an
"alternate formalization"

so I will need to reestablish the old statements
that I know about Set Theory and have their proofs done in CBL Set
Theory. I am not interested at this point of time of generating new
statements.

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.

So you developed CBL to generate new theorems, but it cannot generate
known theorems? 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?

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.

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.

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

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

Are you saying that when I accept a statement of Mathematical nature ...

read more »- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -

.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... I find it hard to understand CBL because you usually give all the things ... I think it would help to present CBL with regards to "Set Theory" only. ... We can state most of the standard axioms of Set Theory pretty easily. ... You mean how do I generate theorems of set theory? ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... concentrate on just one of the things that CBL can do and work from ... I think it would help to present CBL with regards to "Set Theory" only. ... We can state most of the standard axioms of Set Theory pretty easily. ... I am not interested how CBL generate theorems of set theory. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ...  How does this tethering happen in real mathematics? ... any evidence that CBL is tethered in the same way to computation at ... with axioms written in CBL, as I have done and described for PA. ... From that point onward, PR refers to the set of theorems, ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... you are using them in a standard way in CBL. ... assertion that the set of theorems is ... Any system where PR being the set of theorems satisfies the axioms. ... theorems or truths of any given system besides your say so. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... learn CBL. ... But the theorems of "Set Theory" are not well- ... theorems or a set of axioms that defines those theorems. ... How does this relate to ZFC? ...
    (sci.logic)
Quantcast