Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 14, 11:20 pm, William Hale <h...@xxxxxxxxxx> wrote:
In article
<9df49f3b-9476-475f-97c8-ffc2c184f...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>, Charlie-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:

==========================
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? 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. 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. It is not a big
interest because nothing new is generated. In other branches of
Computer Science, we generate new, significant theorems that aren't so
obvious, e.g. those of Godel, Rosser, Turing and Smullyan.

But I can see that much of ZF's theorems can be easily proven in CBL,
and I can give as an example the generating of the ZF Pairing Axiom:

SE(x,y) means y is an element of set x. P(x)/Q(a,b) means set P can
be characterized in base (2 place relation) Q, which by definition of
the "/" operator means that there is an M which characterizes P(x)
meaning that P(x)<=>Q(M,x). So M is the set that contains the
elements of P.

The Pairing Axiom is wff EQ(I,x)vEQ(J,x): For any two values I and J
there is a set that contains every value that is equal to I or equal
to J. This means that EQ(I,x)vEQ(J,x)/SE (we declare SE as the
default base) which is saying that wff EQ(I,x)vEQ(J,x) defines a set.
We can prove that using simple general useful axioms:

EQ(I,x) For every thing, there is a set that contains only it.
UNION: P(x) , Q(x) => P(x) v Q(x) The union of two sets is a set.
SUB: P(I) => P(J) [The rule is trying to say that we can replace any
input variable by any other input.]

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

So the answer is that CBL does Set Theory the same way that it
axiomatizes any branch of Computer Science: via Axioms and Rules of
Inference. I have never bothered/tried to generate lots of Theorems
from Set Theory, because they generally are not enlightening, as they
are statements already known.

(Please don't make the mistake of confusing ZF with Set Theory. ZF is
one possible set of axioms for some sort of Set Theory. Set Theory
includes the syntax and semantics of wffs. You can use the syntax and
semantics of wffs to define sets or to even use the Set Theory wffs as
the set of expressions in a diffrerent system. But the ZF axioms
aren't used to prove anything outside of simple, fairly obvious,
statements about sets. (Refutations welcome.)

But, as I say, we can represent most of e.g. ZF's axioms. Continuing
the above discussion, we have:

1. Extensionality: Is the use of DEF inCBL.

ZF: If the elements of A are all the elements of B, then A=B.
CBL: If all the elements of A are all the elements of B, then we can
substitute A for B.
P , Q means all the elements of P are all the elements of Q.

2. Pairing: Is a theorem EQ(I,x)vEQ(J,x)/SE as explained above.
3. Separation: P/SE , Q/TW => P^Q/SE If P is expressible and Q is a
set, then P^Q is a set.
4. Sum Set: P(x) => (eA)P(A)^SE(A,x)/SE
5. Power Set: (aA)~SE(x,A) v SE(I,A)/SE
6. Infinity: TRUE / SE
7. Replacement: P/SE , Q/TW => P(x)^Q(x,y)/SE => (eA)P(A)^Q(A,x)/SE
8. Empty Set: ~TRUE / SE
9. Foundation: -~SE / SE
10. Choice: M # P / SE + -P,~TRUE => SE(M,aoc(M))

Keep it brief; I can ask you to expand on it further later.
From that former post that I mentioned above, I suspect that you will
give the axioms, terms, etc that form the basis of CBL Set Theory.

Yes, above.

Request 2: I object to the wording "axioms (formal definitions)" above.
For me, "axiom" does not mean "formal definition." I think the standard
terminology is that "functions are primitive" something.

What does ' "functions are primitive" refer to?

I forget what that "something" is.

Axioms (and Rules) are part of an Axiomatic System, which is a
formalization of the subject matter being referred to. CBL axioms are
statements given as being true, as in any use of the notion of an
axiom.

Request 3: If you can, include Pairing that you mentioned above, unless
it will take pages to get to that point (if so, we can come to pairing
later after request 1 is done).

See above.

C-B
.

Relevant Pages