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