```Date: Mar 15, 2013 6:13 PM
Author: Graham Cooper
Subject: Re: I Bet \$25 to your \$1 (PayPal) That You Can’t P<br>	rove Naive Set Theory Inconsistent

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/QSo P/Q means there is an ALGORITHM M thatenumerates (constructs 1 element at a time)SET P based on PREDICATE Q ?e.g.Q = "ADD(A,B,C)"P = { C |  A(A)A(B) ADD(A,B,C) }M = " ADD(s(A), B,, s(C)) <- ADD(A,B,C)..... "...So... EXISTENCE is via POSSIBLE ALGORITHM?like Skolem Functions replace E(X)......I pointed out a flaw in using predicates to specify sets in CBL acouple 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.>> 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?> - 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> Paradox)> 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-BI 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 aNEW RULE on it's own, then it's not formal.What is the TRANSITIVE CLOSURE OF CBL?Enumerate the 1st 1000 theorems of CBL?Herc--www.BLoCKPROLOG.com
```