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


On Mar 15, 6:13 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > 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 ?
If you can enumerate Q then you can enumerate P, yes. If Q is known to contain only r.e. sets then P/Q means that P is r.e. Q could be expressible sets or sets at any level >E1 in the Kleene Arithmetic Hierarchy and thus not r.e. The point is that you define relationships and show what is and what is not an example of one. Computer Science is all about what is and what is not in certain relationships. What is? Theory of Computation positive (UTM) results, Recursion Theory, Program Synthesis enumerate what is. What is not? Theory of Computation negative results (HT), Incompleteness in Logic and Paradoxes enumerate what is not.
> 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)..... " >
More like,
M = {(0,2,2,1,0),(3,2,4,5,4),(2,3,22,13,2)} P = EQ(I,J)* Q = YES
Turing Machine {(0, . . . , 2)} decides if 2 numbers are equal or not. The EQ(I,J) means it halts yes iff input I = input J and the * means it also halts.
> So... EXISTENCE is via POSSIBLE ALGORITHM?
M is/defines/represents/isin1to1with a program that accepts just the elements of P. Or M is a set that contains just the values defined by P. Or wff M expresses set P.
So that P is r.e. or a set or expressible.
> 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.
And didn?t I reply that X*2+5<11 is (eA)MUL(x,?2?,A) ^ (eB) ADD(A,?5?,B) ^ LT(B,?11?) ?
I could also show the PHP program produced by proving M # (eA)MUL(x,?2?,A) ^ (eB)ADD(A,?5?,B) ^ LT(B,?11?) / PHP which outputs the value(s) of X that solve the equation. Axioms are,
?echo $i*$j ;? # MUL(I,J,x)*/PHP ?echo $i+$j ;? # ADD(I,J,x)*/PHP ?echo $i<$j ; ?#LT(I,J)*/PHP ?for ($a=0;$a<$i;++$a) echo $a ;? # LT(x,I)* /PHP
It is in fact an interesting problem to try to do more mathematical algorithms such as solving equations in CBL. But then again, I am trying very hard to formulate Recursion Theory as equation solving.
> > 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?
M is an individual variable as I indicated in the definitions of variables.
A relationship is any way we (or a program) can think of to decide which tuples of n components of anything are to be included in that relationship. P is a relationship that we wish to characterize and Q characterizes a relationship my removing the first component of each tuple of Q and when it is equal to a certain value M include the remaining components as a tuple in the relationship.
The relationships that characterize some of our favorite relationships include,
1. Turing Machines characterize the r.e. sets where (M,N) is included iff Turing Machine M accepts input N.
2. Theoremproving characterizes the representable sets where (M,N) is included if wff M with N substituted for its free variable is provable.
3. Axioms of set theory characterize our sets where (M,N) is included iff M is a set and N is an element of M.
If YES(x,y) iff Turing Machine x accepts input y, then P/YES means P is r.e. If SE(x,y) iff set x contains element y, then P/SE means P expresses a set.
When we say that a formula F expresses an object O (e.g. set or concept) we are implicitly saying that (a) each proposition in F is an O, and (b) the logical rules applied to those propositions in O yield objects in O.
Define TW(M,N) as wff M with N substituted for its free variable is true. (Assume all symbols in M are literals so there is no ?interpretation?.) Then when we say that P is a formula, we are saying that P/TW. Because, P is formula M iff P(x) = = TW(M,x) so that M # P/TW.
Then if we say ?Consider formula x ~e x.? we are saying in CBL that ~SE / TW.
And if we say that all formulas define a set, we are saying that TW / SE.
And guess what we can do with that? Apply Rules of Inference.
Did you know that P/Q ^ Q/R => P/R? Very useful.
> > >  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?
1/2 of Smullyan's approximately 200 theorems in his 4 texts prior to Set Theory. I know because I made sure of that.
> Enumerate the 1st 1000 theorems of CBL?
I did list several 1 and 2 line theorems. Let me be more explicit:
1. The first way to generate a theorem is to substitute in an axiom. 1.1 The first axiom is  ~P / P Axiom of Diagonalization with variable P. 1.1.1. The first constants that can be substituted for P are PR, TW, DIS, YES, SE , . . .
These yield the following theorems:
T1.  ~PR / PR : The set of unprovable sentences is not representable. (Godel 1931) T2.  ~TW / TW : Falsehood is not expressible. (Lemma to Tarski?s Theorem.) T3.  ~DIS / DIS : Unrefutability is not contrarepresentable. (New or obscure) T4.  ~YES / YES : The set of Turing Machines that do not halt yes on themselves is not r.e. T5.  ~SE / SE : There is no set of sets that do not contain themselves (Russell?s Paradox.) . . . T99.  ~(PRvTW) / (PRvTW) : The sentences that are not true or provable can't be characterized by ... ??? ... We're getting into some strange territory here!!
CB
HEY EVERYBODY WHERE'S MY $1 EACH?
> Herc > www.BLoCKPROLOG.com Hide quoted text  > >  Show quoted text 

