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