Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Topic: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Replies: 20   Last Post: Mar 19, 2013 1:32 PM

 Messages: [ Previous | Next ]
 Charlie-Boo Posts: 1,618 Registered: 2/27/06
Re: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Posted: Mar 19, 2013 1:27 PM

On Mar 15, 6:13 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> On Mar 13, 4:09 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>

> > > So what is the difference between MetaMath's and Dan's axioms
> > > and rules of inference, and between your axioms and rules
> > > of inference? Do they smell differently?

>
> > > Bye
>
> > Mine are written in CBL.
>
> > The user interface is: for any two relationships P(...) and Q(...), we
> > define
> > M # P / Q as (all A)Q(M,A,A,...,A) == P(A,A,...,A) and define
> > P/Q as (exists M) M # P/Q

>
> So P/Q means there is an ALGORITHM M that
> enumerates (constructs 1 element at a time)
> SET P based on PREDICATE Q ?

If you can enumerate Q then you can enumerate P, yes. If Q is known
to contain only r.e. sets then P/Q means that P is r.e. Q could be
expressible sets or sets at any level >E1 in the Kleene Arithmetic
Hierarchy and thus not r.e. The point is that you define
relationships and show what is and what is not an example of one.
Computer Science is all about what is and what is not in certain
relationships. What is? Theory of Computation positive (UTM)
results, Recursion Theory, Program Synthesis enumerate what is. What
is not? Theory of Computation negative results (HT), Incompleteness
in Logic and Paradoxes enumerate what is not.

> e.g.
>
>
> P = { C |  A(A)A(B) ADD(A,B,C) }
>
>

More like,

M = {(0,2,2,1,0),(3,2,4,5,4),(2,3,22,13,2)}
P = EQ(I,J)*
Q = YES

Turing Machine {(0, . . . , 2)} decides if 2 numbers are equal or
not. The EQ(I,J) means it halts yes iff input I = input J and the *
means it also halts.

> So... EXISTENCE is via POSSIBLE ALGORITHM?

M is/defines/represents/is-in-1-to-1-with a program that accepts just
the elements of P.
Or M is a set that contains just the values defined by P.
Or wff M expresses set P.

So that P is r.e. or a set or expressible.

> like Skolem Functions replace E(X)..
>
> ....
>
> I pointed out a flaw in using predicates to specify sets in CBL a
> couple months ago.
>
> You can't write:
>    What numbers times 2 add 5 are less than 11?
>
> because you run into the same problem most logic notation has,
> referencing particular arguments.

And didn?t I reply that X*2+5<11 is (eA)MUL(x,?2?,A) ^ (eB)

I could also show the PHP program produced by proving M #
(eA)MUL(x,?2?,A) ^ (eB)ADD(A,?5?,B) ^ LT(B,?11?) / PHP which outputs
the value(s) of X that solve the equation. Axioms are,

?echo \$i*\$j ;? # MUL(I,J,x)*/PHP
?echo \$i<\$j ; ?#LT(I,J)*/PHP
?for (\$a=0;\$a<\$i;++\$a) echo \$a ;? # LT(x,I)* /PHP

It is in fact an interesting problem to try to do more mathematical
algorithms such as solving equations in CBL. But then again, I am
trying very hard to formulate Recursion Theory as equation solving.

> > If P / Q we say P is characterizable in Q, the base.  If M # P / Q we
> > say that M solves or characterizes P in Q.

>
> > Depending on Q, P / Q means that P is recursively enumerable,
> > expressible, a set, a class, a concept, definable in English etc. and

>
> > M # P / Q means
>
> ********************* M **********************
>

> > M is a computer program in programming language Q that
> > enumerates set P,
> > M is a wff that represents set P in logic Q,
> > M is a
> > wff that expresses set P in logic Q,
> > M is a concept and P is its
> > extension,
> > M is a sentence in natural language Q which expresses set P
> > (the set of noun phrases that when substituted for the pronouns in M
> > forms a true sentence) etc.

>
> ************************************
>
> You shouldn't use multiple definitions.
>
> What is M?

M is an individual variable as I indicated in the definitions of
variables.

A relationship is any way we (or a program) can think of to decide
which tuples of n components of anything are to be included in that
relationship. P is a relationship that we wish to characterize and Q
characterizes a relationship my removing the first component of each
tuple of Q and when it is equal to a certain value M include the
remaining components as a tuple in the relationship.

The relationships that characterize some of our favorite relationships
include,

1. Turing Machines characterize the r.e. sets where (M,N) is included
iff Turing Machine M accepts input N.

2. Theorem-proving characterizes the representable sets where (M,N) is
included if wff M with N substituted for its free variable is
provable.

3. Axioms of set theory characterize our sets where (M,N) is included
iff M is a set and N is an element of M.

If YES(x,y) iff Turing Machine x accepts input y, then P/YES means P
is r.e. If SE(x,y) iff set x contains element y, then P/SE means P
expresses a set.

When we say that a formula F expresses an object O (e.g. set or
concept) we are implicitly saying that (a) each proposition in F is an
O, and (b) the logical rules applied to those propositions in O yield
objects in O.

Define TW(M,N) as wff M with N substituted for its free variable is
true. (Assume all symbols in M are literals so there is no
?interpretation?.) Then when we say that P is a formula, we are
saying that P/TW. Because, P is formula M iff P(x) = = TW(M,x) so
that M # P/TW.

Then if we say ?Consider formula x ~e x.? we are saying in CBL that
~SE / TW.

And if we say that all formulas define a set, we are saying that TW /
SE.

And guess what we can do with that? Apply Rules of Inference.

Did you know that P/Q ^ Q/R => P/R? Very useful.

>
> > - E means expression E is false.
>
> > P , Q means P and Q are the same relationship.
>
> > If we are talking about a single formal logic, then PR = the provable
> > sentences, TW = the true sentences and DIS = the refutable sentences.
> > If we are talking about a particular natural language then TS = the
> > true sentences in that natural language.  Also SE(a,b) iff b e a.

>
> > Axioms
>
> > A1. - ~P / P   Axiom of Diagonalization: A base cannot characterize
> > the negation of itself.

>
> > A2. SELF / SELF  Axiom of Self-representation:There is a relationship
> > SELF that characterizes itself

>
> > A3. P / NOTX => ~P / NOTX  Axiom of Negatability: There is a
> > relationship NOTX that characterizes the negation of all relationships
> > that it characterizes.

>
> > Rules of Inference
>
> > R1.  Double Negative: P / Q , ~P / ~Q
>
> > R2.  Transitivity: P/Q , Q/R => P/R
>
> > Theorems with 1-line proofs:
>
> > 1. The set of Turing Machines that don't halt yes on themselves is not
> > recursively enumerable.
> > 2. There is no set of sets that do not contain themselves.  (Russell's
> > 3. There is no truth value to "This is false."  (Liar Paradox)
> > 4. Falsehood is not expressible.

>
> > 2-line proofs:
>
> > 1. Tarski: Truth is not expressible.
>
> > 3 or 4 line proofs:
>
> > 1. Gödel 1931
> > 2. Rosser 1936
> > 3. Smullyan Dual Form Theorem

>
> > although a higher-level theorem which proves all of the above 3 is
> > provable in a few lines.

>
> > CBL can represent and manipulate axioms of various set theories, the
> > Frege-Russell debate, Hilbert's Program's conditions for a perfect
> > logic and how Gödel, Rosser and Smullyan each prove it impossible.
> > That is, CBL proves Hilbert impossible, and individual incompleteness
> > theorems that each can be used as a lemma to prove Hilbert impossible.

>
> > It takes about 8 lines to prove the fixed point theorem, recursion
> > theorem and self-outputting program, and about 12 lines to prove
> > various double recursion theorems.

>
> > C-B
>
> I don't see how...  this is the last time I repeat myself.
>
> If MICROSOFT EXCEL can't use CBL Rules for the COMPUTER to formulate a
> NEW RULE on it's own, then it's not formal.
>
> What is the TRANSITIVE CLOSURE OF CBL?

1/2 of Smullyan's approximately 200 theorems in his 4 texts prior to
Set Theory. I know because I made sure of that.

> Enumerate the 1st 1000 theorems of CBL?

I did list several 1 and 2 line theorems. Let me be more explicit:

1. The first way to generate a theorem is to substitute in an axiom.
1.1 The first axiom is - ~P / P Axiom of Diagonalization with variable
P.
1.1.1. The first constants that can be substituted for P are PR, TW,
DIS, YES, SE , . . .

These yield the following theorems:

T1. - ~PR / PR : The set of unprovable sentences is not
representable. (Godel 1931)
T2. - ~TW / TW : Falsehood is not expressible. (Lemma to Tarski?s
Theorem.)
T3. - ~DIS / DIS : Unrefutability is not contrarepresentable. (New or
obscure)
T4. - ~YES / YES : The set of Turing Machines that do not halt yes on
themselves is not r.e.
T5. - ~SE / SE : There is no set of sets that do not contain
. . .
T99. - ~(PRvTW) / (PRvTW) : The sentences that are not true or
provable can't be characterized by ... ??? ... We're getting into
some strange territory here!!

C-B

HEY EVERYBODY WHERE'S MY \$1 EACH?

> Herc
> --www.BLoCKPROLOG.com- Hide quoted text -
>
> - Show quoted text -

Date Subject Author
3/13/13 Graham Cooper
3/13/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/15/13 Charlie-Boo
3/19/13 Graham Cooper
3/19/13 Charlie-Boo
3/19/13 Charlie-Boo
3/15/13 Graham Cooper
3/15/13 Charlie-Boo
3/15/13 Graham Cooper
3/19/13 Charlie-Boo