
Re: I Bet $25 to your $1 (PayPal) That You Can’t P rove Naive Set Theory Inconsistent
Posted:
Mar 15, 2013 6:13 PM


On Mar 13, 4:09 am, CharlieBoo <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 Selfrepresentation: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 1line 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. > > 2line 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 higherlevel 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 > FregeRussell 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 selfoutputting program, and about 12 lines to prove > various double recursion theorems. > > CB
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

