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/Q

So P/Q means there is an ALGORITHM M that

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

>

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

Enumerate the 1st 1000 theorems of CBL?

Herc

--

www.BLoCKPROLOG.com