Godel proved maths inconsistent not incompleteness theorem
elsiemelsi
even prove the incompleteness theorem. The incompleteness theorem is just
an attempt to hide from what he did prove-which is math is inconsistent he
could not accept that so he set up the incompleteness theorem
http://gamahucherpress.yellowgum.com/books/philosophy/GODEL5.pdf
[quote]Godel proved that mathematics was inconsistent
From Nagel -"Gödel" Routeldeg & Kegan, 1978, p 85-86
***Gödel also showed that G is demonstrable if and only if it’s formal
negation ~G is demonstrable.*** However if a formula and its own negation
are both formally demonstrable the mathematical ***calculus is not
consistent*** (this is where he adopts the watered down version noted by
bunch) accordingly if (just assumed to make math’s consistent) the
calculus is consistent neither G nor ~G is formally derivable from the
axioms of mathematics. Therefore if mathematics is consistent G is a
formally undecidable formula Gödel then proved that though G is not
formally demonstrable it nevertheless is a true mathematical formula
From Bunch
"Mathematical fallacies and paradoxes” Dover 1982" p .151
Gödel proved
~P(x,y) & Q)g,y)
***in other words ~P(x,y) & Q)g,y) is a mathematical version of the liar
paradox.*** It is a statement X that says X is not provable. ***Therefore
if X is provable it is not provable a contradiction. ***If on the other
hand X is not provable then its situation is more complicated. If X says
it is not provable and it really is not provable then X is true but not
provable ***Rather than accept a self-contradiction mathematicians settle
for the second choice***
[/quote]
[quote]Thus Godel by using invalid axioms and impredicative definitions
only succeeded in getting the inevitable paradox that his axioms and
impredicative definitions ordained him to get. In other words he could
have only ended in paradox for this is what his axioms and impredicative
definitions determined him to get. Thus his proof is a complete failure
as his proof. that mathematics is inconsistent was the only result
that he could have logically arrived at since this result is what his
axioms and impredicative definitions logically would lead him to; because
these axioms and impredicative definitions lead to or end in paradox
themselves. All he succeeded in getting was a paradoxical result..
Godel by using those axioms and impredicative definitions he could only
have arrived at a paradoxical result [/quote]
--
Message posted using http://www.talkaboutscience.com/group/sci.logic/
More information at http://www.talkaboutscience.com/faq.html
Charlie-Boo
> Godel ends up proving maths is inconsistent by useing maths. Godels did not
> even prove the incompleteness theorem.
Ok, I'll do it then:
The set of provable statements is r.e. but the set of true statements
is not (otherwise the halting problem would be solved by looking for
"X halts." and "X doesn't halt."), so if the system is sound then
there is a wff true and not provable, and also since it is sound then
it can't be refuted either!
How 'zat?
C-B
Charlie-Boo
> On Feb 17, 10:51 pm, "elsiemelsi" <cyprin...@nosam.yahoo.com> wrote:
>
> > Godel ends up proving maths is inconsistent by useing maths. Godels did not
> > even prove the incompleteness theorem.
>
> Ok, I'll do it then:
>
> The set of provable statements is r.e. but the set of true statements
> is not (otherwise the halting problem would be solved by looking for
> "X halts." and "X doesn't halt."), so if the system is sound then
> there is a wff true and not provable, and also since it is sound then
> it can't be refuted either!
>
> How 'zat?
>
> C-B
BTW What Godel actually proved was that there is a recursive function
that creates a wff that is true and unprovable (a constructive proof
of existance), but he stated it as being the weaker theorem: only that
such a wff exists. This weaker theorem can thus be proved in a much
simpler manner than in which Godel proved the unspoken stronger
theorem.
Thus we have ultra-short proofs for not only Godel's results but also
Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
Godel. (In all fairness, Godel had just invented [primitive]
recursive functions and it is reasonable that he didn't think of a
proof as a recursive function that is proven to produce the object
which exists.)
(This is something I discovered only recently, actually.)
(Now people are enticed to try both "It's stupid." and "Everybody
knows that." at the same time!)
C-B
Peter_Smith
> Thus we have ultra-short proofs for not only Godel's results but also
> Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> Godel.
I'm not sure you should be talking about a "mistake" here.
After all it is interesting, important (and given the intellectual
context of the time, crucial to Gödel) that (a) an undecidable
decidable sentence can be effectively constructed, and (b) that the
proof of its undecidability depends only on syntactically specifiable
conditions (i.e. doesn't appeal to the notion of truth).
But of course, you are absolutely right contra our dear friend
elsiemelsi that there are (lots of) short and pretty incompleteness
proofs that don't in any way depend on the assumptions that elsiemelsi
(wrongly) thinks are involved in Gödel's proof. And the one you
mention is about the shortest even if we start from first principles.
One of my other favourites is the proof that Kleene's normal form
theorem entails incompleteness.
Aatu Koskensilta
> (In all fairness, Godel had just invented [primitive] recursive
> functions and it is reasonable that he didn't think of a proof as a
> recursive function that is proven to produce the object which
> exists.)
Godel was well aware that his proof was constructive.
> (This is something I discovered only recently,
> actually.)
The constructive nature of Godel's proof or his presumed ignorance of
it?
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Charlie-Boo
wrote:
> On 2008-03-03, in sci.logic, Charlie-Boo wrote:
>
> > (In all fairness, Godel had just invented [primitive] recursive
> > functions and it is reasonable that he didn't think of a proof as a
> > recursive function that is proven to produce the object which
> > exists.)
>
> Godel was well aware that his proof was constructive.
But the statement of the result is the weaker theorem, which can be
proved much simpler. In general, those (e.g. Chaitin - a total idiot)
who say that it is complex and difficult to prove "Godel's Theorem"
are wrong, as that theorem is stated as one which has a much simpler
proof than the constructive proof given by Godel and cited.
(Refutations welcome.)
(Most of the similar results can likewise be simplified.)
(Even the constructive proof is simple if you accept the fact that
proving a system universal is not something easily generalized (nor is
it constructive to try to do so) and so should remain axiomatic for
each system, while proven using general proof methods. Beyond proving
that Logic and Turing Machines are universal, the rest of the Godel/
Turing/Rosser et. al. proofs are very simple, allowing such short
constructive proofs as well, given these axioms.)
(Of course professors don't like to talk about Occam's Razor, as it is
one of the few widely-read criteria for what is WRONG with what is
being published routinely.)
> > (This is something I discovered only recently,
> > actually.)
>
> The constructive nature of Godel's proof or his presumed ignorance of
> it?
How to exploit the mistatements of the various incompleteness
theorems.
C-B
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
Charlie-Boo
> On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > Thus we have ultra-short proofs for not only Godel's results but also
> > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > Godel.
>
> I'm not sure you should be talking about a "mistake" here.
>
> After all it is interesting, important (and given the intellectual
> context of the time, crucial to Gödel) that (a) an undecidable
> decidable sentence can be effectively constructed, and (b) that the
> proof of its undecidability depends only on syntactically specifiable
> conditions (i.e. doesn't appeal to the notion of truth).
>
> But of course, you are absolutely right contra our dear friend
> elsiemelsi that there are (lots of) short and pretty incompleteness
> proofs
Lots? Ok, how about showing a couple of those short and pretty
proofs? In particular, where has my proof above appeared?
It is not Mathematics to make unfounded claims. It is not even
honest.
C-B
Peter_Smith
> On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
>
>
>
> > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > Thus we have ultra-short proofs for not only Godel's results but also
> > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > > Godel.
>
> > I'm not sure you should be talking about a "mistake" here.
>
> > After all it is interesting, important (and given the intellectual
> > context of the time, crucial to Gödel) that (a) an undecidable
> > decidable sentence can be effectively constructed, and (b) that the
> > proof of its undecidability depends only on syntactically specifiable
> > conditions (i.e. doesn't appeal to the notion of truth).
>
> > But of course, you are absolutely right contra our dear friend
> > elsiemelsi that there are (lots of) short and pretty incompleteness
> > proofs
>
> Lots? Ok, how about showing a couple of those short and pretty
> proofs? In particular, where has my proof above appeared?
>
> It is not Mathematics to make unfounded claims. It is not even
> honest.
>
> C-B
Brevity depends on what you take for granted, but various short proofs
abound, e.g. in my book secs 5.3/5.4, 6.2/6.3, 33.6 to mention three
proofs distinct from Gödel's ... and the proof you sketch via the
unsolvability of the halting problem is also there too in two
versions.
Chris Menzel
> On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
> > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
> > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > >Godel.
>
> > I'm not sure you should be talking about a "mistake" here.
>
> > After all it is interesting, important (and given the intellectual
> > context of the time, crucial to Gödel) that (a) an undecidable
> > decidable sentence can be effectively constructed, and (b) that the
> > proof of its undecidability depends only on syntactically specifiable
> > conditions (i.e. doesn't appeal to the notion of truth).
>
> > But of course, you are absolutely right contra our dear friend
> > elsiemelsi that there are (lots of) short and prettyincompleteness
> > proofs
>
> Lots? Ok, how about showing a couple of those short and pretty
> proofs? In particular, where has my proof above appeared?
*Your* proof? You're talking about the "proof" here, in your "system"
CBL? http://arxiv.org/html/cs.lo/0003071 . I don't think so. A
short discussion of a smattering of the problems that infect CBL from
the ground up can be found here: http://groups.google.com/group/sci.logic/msg/d0d34dcbffd7a744
. You haven't proved a thing beyond your own need to learn some basic
mathematical logic and computability theory.
Charlie-Boo
>
> > Thus we have ultra-short proofs for not only Godel's results but also
> > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > Godel.
>
> I'm not sure you should be talking about a "mistake" here.
>
> After all it is interesting, important (and given the intellectual
> context of the time, crucial to Gödel) that (a) an undecidable
> decidable sentence can be effectively constructed,
Where is that needed vs. a non-constructive proof? In any case, the
simplification is there. Occam Rocks!
(I assume you mean the Godel sentence.)
This post screen is all weird. I think Google is crashingh ./qa'
dflsdewfl ;wf,as cas '
a'dlas
das
d
Charlie-Boo
>
> > Thus we have ultra-short proofs for not only Godel's results but also
> > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > Godel.
>
> I'm not sure you should be talking about a "mistake" here.
Generations have restricted themselves to the unnecessary complexities
of the constructive proof.
> After all it is interesting, important (and given the intellectual
> context of the time, crucial to Gödel) that (a) an undecidable
> decidable sentence can be effectively constructed,
When must it be constructive? And can anyone deny the value of
minimizing the number of primitives? Occam rocks!
> and (b) that the
> proof of its undecidability depends only on syntactically specifiable
> conditions (i.e. doesn't appeal to the notion of truth).
You want to define "syntactically specifiable conditions"? What are
the conditions? How are they syntactically specified? What isn't or
can't be?
> But of course, you are absolutely right contra our dear friend
> elsiemelsi that there are (lots of) short and pretty incompleteness
> proofs that don't in any way depend on the assumptions that elsiemelsi
> (wrongly) thinks are involved in Gödel's proof.
I thought it was neat - crank call, clowns silent or honking horns as
usual, purported crank instead throws out another bone. LOL
(BMAPMOTB breaking my arm patting myself on the back)
> And the one you
> mention is about the shortest even if we start from first principles.
I've posted plenty of shorter alternatives to get -PR,TW. The
unprovable sentences are expressible but not representable, e.g. (I
posted a list once.)
The set of proofs generated by CBL is infinite. You create variations
by altering the node of the tree below the root FALSE or replacing
rules used to derive a node.
> One of my other favourites is the proof that Kleene's normal form
> theorem entails incompleteness.
You mean favorite short proof? How's that one go? (Tiny so no
excuses.)
C-B
Charlie-Boo
> On Mar 9, 12:53 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
>
> > > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > Thus we have ultra-short proofs for not only Godel's results but also
> > > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > > > Godel.
>
> > > I'm not sure you should be talking about a "mistake" here.
>
> > > After all it is interesting, important (and given the intellectual
> > > context of the time, crucial to Gödel) that (a) an undecidable
> > > decidable sentence can be effectively constructed, and (b) that the
> > > proof of its undecidability depends only on syntactically specifiable
> > > conditions (i.e. doesn't appeal to the notion of truth).
>
> > > But of course, you are absolutely right contra our dear friend
> > > elsiemelsi that there are (lots of) short and pretty incompleteness
> > > proofs
>
> > Lots? Ok, how about showing a couple of those short and pretty
> > proofs? In particular, where has my proof above appeared?
>
> > It is not Mathematics to make unfounded claims. It is not even
> > honest.
>
> > C-B
>
> Brevity depends on what you take for granted,
I'm not so sure that what you're trying to say is true. Do you want
to give a simple example - a pair of proofs that differ only by what
is "taken for granted"?
> but various short proofs
> abound, e.g. in my book secs 5.3/5.4, 6.2/6.3, 33.6 to mention three
> proofs distinct from Gödel's ... and the proof you sketch via the
> unsolvability of the halting problem is also there too in two
> versions.
You have not given these (lots of) proofs that you say are so short
and easy to give. I gave mine.
But thanks for the reference - you will get your royalty. I have
posted at least 5-10 proofs of various forms of incompleteness
generated by CBL. I would be surprised if none of them were published
elsewhere. Why? Think. That would mean that I didn't represent what
was published! But I would also be surprised if all of them were
(nontrivial set) - e.g. nobody knew or challenged my shortest Rosser
1936. Your book sounds delicious (your previous ads weren't as good,
I guess) and I am always hungry for short/high level proofs. That is
where everyone should be headed. And also the use of programs in the
proof - agreed? (TF didn't.)
I will do your job and see what you have there. And maybe even the
job of showing it here.
C-B
- Hide quoted text -
>
> - Show quoted text -
Charlie-Boo
> Godel ends up proving maths is inconsistent by useing maths. Godels did not
> even prove the incompleteness theorem. The incompleteness theorem is just
> an attempt to hide from what he did prove-which is math is inconsistent he
> could not accept that so he set up the incompleteness theorem
>
> http://gamahucherpress.yellowgum.com/books/philosophy/GODEL5.pdf
> [quote]Godel proved that mathematics was inconsistent
>
> From Nagel -"Gödel" Routeldeg & Kegan, 1978, p 85-86
>
> ***Gödel also showed that G is demonstrable if and only if it's formal
> negation ~G is demonstrable.*** However if a formula and its own negation
> are both formally demonstrable the mathematical ***calculus is not
> consistent*** (this is where he adopts the watered down version noted by
> bunch) accordingly if (just assumed to make math's consistent) the
> calculus is consistent neither G nor ~G is formally derivable from the
> axioms of mathematics. Therefore if mathematics is consistent G is a
> formally undecidable formula Gödel then proved that though G is not
> formally demonstrable it nevertheless is a true mathematical formula
The mistake isn't in Godel, it is in Bunch. Rosser showed (for his G)
|-G <=> |-~G while Godel proved that G <=> ~|-G.
Actually, there's also a mistake or two by both Godel and Bunch here:
1. Godel didn't prove that G is true using metamathematical means, as
stated by Godel and Bunch. He proved that if the system is sound then
G is true.
2. The wff that expresses "If the system is sound then G is provable"
is provable. Godel himself used a variation of this in his proof of
the second theorem, leaving the odd taste of his saying that we can't
formally prove G but we can formally prove that if the system is
consistent then G is true (thus we cannot prove the system
consistent.) Hopefully this will clear up the confusion. (Just spell
my name right.)
> From Bunch
> "Mathematical fallacies and paradoxes" Dover 1982" p .151
Including his own! Is there a book of all fallacies made in books of
fallacies (false negatives)? No, by the CBP (C-B Paradox) it is self-
referentially excluded. See http://groups.google.com/group/selfref?hl=en
C-B
> Gödel proved
>
> ~P(x,y) & Q)g,y)
> ***in other words ~P(x,y) & Q)g,y) is a mathematical version of the liar
> paradox.*** It is a statement X that says X is not provable. ***Therefore
> if X is provable it is not provable a contradiction. ***If on the other
> hand X is not provable then its situation is more complicated. If X says
> it is not provable and it really is not provable then X is true but not
> provable ***Rather than accept a self-contradiction mathematicians settle
> for the second choice***
> [/quote]
>
> [quote]Thus Godel by using invalid axioms and impredicative definitions
> only succeeded in getting the inevitable paradox that his axioms and
> impredicative definitions ordained him to get. In other words he could
> have only ended in paradox for this is what his axioms and impredicative
> definitions determined him to get. Thus his proof is a complete failure
> as his proof. that mathematics is inconsistent was the only result
> that he could have logically arrived at since this result is what his
> axioms and impredicative definitions logically would lead him to; because
> these axioms and impredicative definitions lead to or end in paradox
> themselves. All he succeeded in getting was a paradoxical result..
> Godel by using those axioms and impredicative definitions he could only
> have arrived at a paradoxical result [/quote]
>
> --
Aatu Koskensilta
> 2. The wff that expresses "If the system is sound then G is provable"
> is provable.
The soundness of the system is not expressible in the system, though
weaker correctness properties, such as omega-consistency or
1-consistency are.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Charlie-Boo
> On Mar 9, 7:53 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
> > > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
> > > > Thus we have ultra-short proofs fornotonlyGodel'sresults but also
> > > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > > >Godel.
>
> > > I'm not sure you should be talking about a "mistake" here.
>
> > > After all it is interesting, important (and given the intellectual
> > > context of the time, crucial to Gödel) that (a) an undecidable
> > > decidable sentence can be effectively constructed, and (b) that the
> > > proof of its undecidability depends only on syntactically specifiable
> > > conditions (i.e. doesn't appeal to the notion of truth).
>
> > > But of course, you are absolutely right contra our dear friend
> > > elsiemelsi that there are (lots of) short and prettyincompleteness
> > > proofs
>
> > Lots? Ok, how about showing a couple of those short and pretty
> > proofs? In particular, where has my proof above appeared?
>
> *Your* proof? You're talking about the "proof" here, in your "system"
The proof ("above") in the previous post is self-contained.
As far as my year 2000 article goes, I just now explained in that
thread that it is just program synthesis and Turing Theory of
Computation, not Godel/Rosser incompleteness in logic, and there is
some miscommunication occurring in your concerns, partially caused by
how I formalized program synthesis in 2000, which is improved now by
including the program in the expression. Instead of PRIME(x) for list
the prime numbers, I now have the form M # PRIME(x) to mean that some
particular program M lists the prime numbers.
The development of CBL (it's really fascinating, if you'll muster the
effort to follow it):
1. Program Synthesis: 1 year 9 months to develop the 8 Rules of
Inference described in ARXIV 2000.
P(I) P is decided
P(x) P is listed
P means no x in P( . . . ) like P(I)
(additional I are optional)
Rules of Inference:
SUB: P(I) => P(". . .") NOT: P(I) => ~P(I) The complement of a
recursive set is recursive.
AND: P , Q => P^Q IF: P , Q(x) => P^Q(x)
OR: P , Q => PvQ QUIT: P(x,y) => (eA)P(x.A)
DO: P(x) , Q(I) => P(x) ^ Q(x) UNION: P(x) , Q(x) => P(x) v Q(x)
These have morphed over time. We are tempted to have P(x) , Q(x) =>
P(x) ^ Q(x) but that is only a theorem when we have axiom EQ(I,J). We
also have P(I) => P(x) but that is only when TRUE(x) (try proving that
all recursive sets are r.e. without referring to the universal set as
being r.e.). So the original 8 rules are universally true while
axioms in programming EQ(I,J) and TRUE(x) let us add theorems like
P(x) , Q(x) => P(x) ^ Q(x).
2. DataBase Query Processing: Represent a file as a set of programs.
3. Theory of Computation: Same Rules!
Add 3 Axioms! -~YES(x,x) , YIT(I,J,K)* , TRUE(x) (Diagonalization
within YES, Kleene T predicate, Peano)
Minsky and Rogers: "Turing has no practical value."
CBL: "Turing is one tiny step from Program Synthesis, the most
practical branch of CS (BCS)."
4. Recursion Theory: Expand to:
P is a function f(I,J, . . .)
M # P Program M solves spec P.
M # P(I) M decides set P.
M # P(x) M enumerates set P.
yes(I) The set of inputs accepted/outputs enumerated by program
number I,
sii(I,J) The result of substituting literal J for the first of the
one input into program I.
Axioms:
1. I # yes(I)
Programs are deterministic - defined by functions. The result of
running program (input) I is to enumerate/accept set yes(I)
2. wr(I) # I
For every input I there is a program that outputs only that value,
given by function wr.
3. wr(I)
wr is recursive.
4. M # f(I) => s11(M,N) # f(N)
Definition of substituion. If M outputs f(I) then s11(M,N)
substitutes N for I and outputs f(N).
5. s11(I,J)
Substitution is recursive.
Rules: Substitution and Modus Ponens.
Theorems: There is a self-outputting program. Fixed Point.
Resursion. Double Recursion. Solutions to Smullyan et. al. recursion
equations puzzles.
4.1 Revamp Program Synthesis. Use M # P(x) and follow the program
development within the wff not as a separate process that occurs
afterwards against the proof as described in ARXIV 2000. Realize that
"Program Synthesis" = |- M # P ! Anyhthing else is bogus.
5. Various other branches of Mathematics/Computer Science: Set Theory,
Proof Theory, Truth, Paradoxes (constant proof, variable system),
Foundations, Classic Logic etc. need 1 more thing: a variable (Q
below) for the base/domain. This is one of the main things missing
from the current state of the art.
M # P / Q
P = Q(M)
P(a) = Q(M,a)
M characterizes set P in base Q, i.e. P(a) = Q(M,a)
When Q is . . . then P is:
Q: Program I halts on input J. Recursively enumerable.
Q: Wff I is provable on input J (free variable substituted for).
Representable
Q: Wff I is true on input J. Expressible
Q: Set I contains element J. Well-founded set
Q: English sentence I with J substituted for its pronouns. (definable
in English)
etc.
Operator (function) # operates on 2 sets with different
cardinalities. This is MetaMathematics formalized.
6. Abstract UP to model Branches of Computer Science:
Program Synthesis PGSYN X # I / YES Input the spec, output the
program, the base (programming language) is YES = Turing Machines.
Program Analysis PGANA I # X / YES Input the program, output the
spec.
Program Debugging: PGDEB I # J / YES Input the program and spec and
determine if the program meets the spec.
Set Theory: SETH X / SE List the sets that can be
defined.or X # Y / SE List the sets and how to define them.
Theory of Computation: TOCP X / YES List the r.e. sets TOCN -X /
YES List the non-re sets (P,N=+.-)
[ At this point, substitution is at the highest and the lowest levels
of abstraction. Crucial theorems of Recursion Theory depend on the
fact that substitution is recursive i.e. s11(I,J) (in general sij for
all natural numbers ~(I>J)) and the various branches of Computer
Science and Mathematics are formally defined by expressions of the
form M # P / Q or P / Q (such an M exists) where we originally said P
which is short for P / YES which means there is an M such that M # P /
YES, where in fact:
M # P / Q Program M meets spec P in programming language Q
is actually an instance of substitution, the model for Computer
Science above.
P = s12(Q,M)
P = Q(M) ]
Incompleteness in Logic: INC This is really tricky. Where does it
all start? It all ends in diagonalization: Axiom -~P/P
( -~YES(x,xU) in TOC is a special case.)
Godel 1: PR/TW => ~PR/TW => -PR,TW Provability is expressible so
nonprovability is and so proof and truth differ.
Rosser: PR/PR => PR/DIS => -PR,~DIS Provability is representable so
contrarepresentable so proof and nonrefutability differ.
Turing: NO/YES (Theorem) + ~(YESvNO)/YES (Halting Problem) = (OR Rule)
NO v ~(YES v NO) / YES. CONS: YES^NO,~TRUE => ~YES/YES
Also note that CONS = PR^DIS,~TRUE = ~TRUE/PR is useful in showing
relationships among theorems.
(Godel-2 can be proven in at least 3 ultra short distinct ways.)
The axiom -~P/P states that no base can characterize its complement.
The proof uses this here as:
P/Q => -P,~Q If P is characterized in base Q, then P is not equal to
the complement of Q.
Nonprovability is expressible and provability is contrarepresentable
are Godel 1 and Rosser.
But where do we get PR/TW and PR/PR? These are the starting point of
Godel, Rosser and Turing.
PR/PR is universality in Logic PR (theorems). Turing uses
universality in YES (halting programs).
And why the concern that PR=>TW (sound) or PR => ~DIS (consistent) or
~PR => DIS (complete) etc.?
At this point everyone is lost and I receive no response to anything
at this level of abstfraction or above. But I know the final answer:
Hilbert!
7. Beyond (new 1/08)
SELF is any universal relation (base).
Example: Theorems (are representable) and halting programs (are
recursively enumerable)
NOTX is any complementable relation.base.
Examples: True Logic sentences, True English sentences, Sets
(The complement of an expressible relation (of a set) is expressible
(is a set).)
SELF / SELF Theoremdom (halting programs) is representable (r.e.)
(Rosser and Turing)
SELF / NOTX Theoremdom is expressible. (Godel-1)
- NOTX / SELF Truth is not recursively enumerable.
- NOTX / NOTX (Theorem) Truth is not expressible (Tarski.)
SELF/SELF is not actually saying that theoremdom is representable! It
is saying that by definition, SELF / SELF as SELF is defined to be any
universal relation. So the process of determining that Logic and
Programs are universal does not exist within this system. We remove
99% of the proof - the big messy proof of universality in Godel 1931
and Turing 1937's papers, have no role at this level of abstraction.
This is only concerned with what we can do with any given SELF and
NOTX, not where they might be found.
Now note that no relation can be both SELF and NOTX. But get this:
ALL THE BASES USED IN MATHEMATICS ARE EITHER SELF OR NOTX ! ! !
Why ? ? ?
C-B
> short discussion of a smattering of the problems that infect CBL from
> the ground up can be found here:http://groups.google.com/group/sci.logic/msg/d0d34dcbffd7a744
How about the above?
> . You haven't proved a thing beyond your own need to learn some basic
> mathematical logic and computability theory.- Hide quoted text -
Charlie-Boo
>
>
>
>
>
> > On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
> > > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
> > > > Thus we have ultra-short proofs fornotonlyGodel'sresults but also
> > > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > > >Godel.
>
> > > I'm not sure you should be talking about a "mistake" here.
>
> > > After all it is interesting, important (and given the intellectual
> > > context of the time, crucial to Gödel) that (a) an undecidable
> > > decidable sentence can be effectively constructed, and (b) that the
> > > proof of its undecidability depends only on syntactically specifiable
> > > conditions (i.e. doesn't appeal to the notion of truth).
>
> > > But of course, you are absolutely right contra our dear friend
> > > elsiemelsi that there are (lots of) short and prettyincompleteness
> > > proofs
>
> > Lots? Ok, how about showing a couple of those short and pretty
> > proofs? In particular, where has my proof above appeared?
>
> *Your* proof? You're talking about the "proof" here, in your "system"
> short discussion of a smattering of the problems that infect CBL from
> the ground up can be found here:http://groups.google.com/group/sci.logic/msg/d0d34dcbffd7a744
> . You haven't proved a thing
You know, the proof is in the pudding. If it makes good pudding, then
you can only complain about how I made it (went outside the rules),
not what the ingredients are. So talking about how certain things are
handled in the system doesn't mean much if we show legitimate programs
being synthesized and valid proofs are displayed. You can only
complain about their source - show that I wrote them by hand and
slipped them in.
This is a common mistake and you may be guilty of that here. Can you
show my output to be incorrect or spurious?
C-B
> beyond your own need to learn some basic
Aatu Koskensilta
"Metaproof" of what? The implication "if T is omega-consistent, G is
true but undecidable in T" is provable in the usual T -- certainly in
the system P Godel considers.
But allow me to offer you a chance to flex the CBL muscle. Be a sport,
do provide for our inspection a proof of the theorem that Robinson
arithmetic does not prove the usual formalisation in the language of
arithmetic of "Robinson arithmetic is consistent", in the concise
style we've come to expect from CBL.
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > 2. The wff that expresses "If the system is sound then G is provable"
> > is provable.
>
> The soundness of the system is not expressible in the system,
Yes, it would seem that no nontrivial function of the true sentences
could be expressed. Can we show a function f such that if w1
expresses "Provable => True" then f(w1) expresses "x is true"?
So if assertion P is provable metamathematically and w expresses P,
then w is provable in the logic? I am assuming that Godel
metamathematically proved "If the logic is Sound (or w-consistent)
then G" rather than "G", which you skipped in your rebuke, so you
agree??
> though
> weaker correctness properties, such as omega-consistency or
> 1-consistency are.
And some stronger as well.
C-B
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
>
Aatu Koskensilta
> Yes, it would seem that no nontrivial function of the true sentences
> could be expressed. Can we show a function f such that if w1
> expresses "Provable => True" then f(w1) expresses "x is true"?
I'm afraid I can't make anything of this question. Perhaps you can
elaborate on what you have in mind?
> So if assertion P is provable metamathematically and w expresses P,
> then w is provable in the logic?
That depends on whether the principles used in the "metamathematical"
proof of P are included in the system under consideration.
> I am assuming that Godel metamathematically proved "If the logic is
> Sound (or w-consistent) then G" rather than "G", which you skipped
> in your rebuke, so you agree??
G follows from the observation that the system P under consideration
is sound and hence consistent. This proof of G is not formalisable in
P, but the proof of "if P is consistent then G" is, as is the proof of
"if P is consistent, G is not provable in P, and if P is
omega-consistent, not-G is not provable in P".
> And some stronger as well.
What correctness properties stronger than soundness do you have in
mind? On the face of it the notion makes no sense.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Charlie-Boo
>
> > Thus we have ultra-short proofs for not only Godel's results but also
> > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > Godel.
>
> I'm not sure you should be talking about a "mistake" here.
>
> After all it is interesting, important (and given the intellectual
> context of the time, crucial to Gödel) that (a) an undecidable
> decidable sentence can be effectively constructed, and (b) that the
> proof of its undecidability depends only on syntactically specifiable
> conditions (i.e. doesn't appeal to the notion of truth).
>
> But of course, you are absolutely right contra our dear friend
> elsiemelsi that there are (lots of) short and pretty incompleteness
> proofs that don't in any way depend on the assumptions that elsiemelsi
> the one you
> mention is about the shortest even if we start from first principles.
If you restrict the competition to a subset (those that "start from
first principles") of what would constitute a proof, then naturally my
rank on the brevity scale can only go up.
C-B
Charlie-Boo
>
>
>
>
>
> > On Mar 3, 6:32 am, Peter_Smith <ps...@cam.ac.uk> wrote:
> > > On Mar 3, 7:10 am, Charlie-Boo <shymath...@gmail.com> wrote:
> > > > Thus we have ultra-short proofs fornotonlyGodel'sresults but also
> > > > Rosser's 1936 extenstion (a misnomer) as he made the same mistake as
> > > >Godel.
>
> > > I'm not sure you should be talking about a "mistake" here.
>
> > > After all it is interesting, important (and given the intellectual
> > > context of the time, crucial to Gödel) that (a) an undecidable
> > > decidable sentence can be effectively constructed, and (b) that the
> > > proof of its undecidability depends only on syntactically specifiable
> > > conditions (i.e. doesn't appeal to the notion of truth).
>
> > > But of course, you are absolutely right contra our dear friend
> > > elsiemelsi that there are (lots of) short and prettyincompleteness
> > > proofs
>
> > Lots? Ok, how about showing a couple of those short and pretty
> > proofs? In particular, where has my proof above appeared?
>
> *Your* proof? You're talking about the "proof" here, in your "system"
> short discussion of a smattering of the problems that infect CBL from
> the ground up can be found here:http://groups.google.com/group/sci.logic/msg/d0d34dcbffd7a744
> . You haven't proved a thing beyond your own need to learn some basic
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > But where does the formalization of the metaproof fail??
>
> "Metaproof" of what? The implication "if T is omega-consistent, G is
> true but undecidable in T" is provable in the usual T -- certainly in
> the system P Godel considers.
A non-theorem according to the logic. Not sure where that comes from
- other thread?
I asked if every Metatheorem expressible in the loigic is provable in
the logic. Then I asked where an attempt to formalize its metaproof
within the logic fails, as in the case of a metatheorem involving
truth that you pointed out is not even expressible much less provable
in the logic.
> But allow me to offer you a chance to flex the CBL muscle.
Please do.
> Be a sport,
When have I not? (Unsubstantiated innuendo?)
> do provide for our inspection a proof of the theorem that Robinson
> arithmetic does not prove the usual formalisation in the language of
> arithmetic of "Robinson arithmetic is consistent", in the concise
> style we've come to expect from CBL.
I'll crank. It helps if you give me an on-line proof. (Unless you're
more intersted in my failing, contrary to your posture.)
So that's Godel-2 for Q? There are numerous ways to prove Godel-2 (I
am amazed at their absence from texts.)
I could use an intuitive (actual) proof, or at least some properties
of Q - the ones needed mayhaps? Or we have to wait awhile while it
cranks.
C-B
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
>
MoeBlee
> On Mar 10, 6:47 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> wrote:
> > Be a sport,
>
> When have I not? (Unsubstantiated innuendo?)
(1) No, he didn't insinuate that you're not a sport. (2) But the
answer to your question includes such instances as never getting back
to me as to the purpose of your question about set theory that I
answered in full (our very first discussion), and not recognizing the
examples given to you of theorems of mathematics proven by ZFC.
By the way, did you ever figure out how to prove in Z set theory that
if a set and its complement are recursively enumerable then the set is
recursive?
MoeBlee
Alan Smaill
got to be easy --
just feed it into CBL and turn the handle, AIUI.
> MoeBlee
--
Alan Smaill
Aatu Koskensilta
> I asked if every Metatheorem expressible in the loigic is provable in
> the logic.
What do you mean by "Metatheorem" here? A mathematical theorem about
the system of course need not in general be provable in the system
even when the theorem is expressible in the system.
> Then I asked where an attempt to formalize its metaproof within the
> logic fails, as in the case of a metatheorem involving truth that
> you pointed out is not even expressible much less provable in the
> logic.
I am at loss as to what "Metatheorems" and "metaproofs" you have in
mind. Theorems about the system that fail to be provable in it are
those that can't be proved without appeal to principles not contained
in the system.
> I'll crank. It helps if you give me an on-line proof.
You'll find a proof that Robinson arithmetic does not prove its
consistency in
/Godel's Second Incompleteness Theorem for Q/
A. Bezboruah and J. C. Shepherdson
The Journal of Symbolic Logic Vol. 41, No. 2 (Jun., 1976),
pp. 503-512
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > Yes, it would seem that no nontrivial function of the true sentences
> > could be expressed. Can we show a function f such that if w1
> > expresses "Provable => True" then f(w1) expresses "x is true"?
>
> I'm afraid I can't make anything of this question. Perhaps you can
> elaborate on what you have in mind?
To prove that "Provable => True" cannot be expressed, since "x is
true" cannot be expressed.
> > So if assertion P is provable metamathematically and w expresses P,
> > then w is provable in the logic?
>
> That depends on whether the principles used in the "metamathematical"
> proof of P are included in the system under consideration.
>
> > I am assuming that Godel metamathematically proved "If the logic is
> > Sound (or w-consistent) then G" rather than "G", which you skipped
> > in your rebuke, so you agree??
>
> G follows from the observation that the system P under consideration
> is sound and hence consistent. This proof of G is not formalisable in
> P, but the proof of "if P is consistent then G" is, as is the proof of
> "if P is consistent, G is not provable in P, and if P is
> omega-consistent, not-G is not provable in P".
>
> > And some stronger as well.
>
> What correctness properties stronger than soundness do you have in
> mind?
It depends on how you define correctness properties. There certainly
are stronger properties that are expressible, aren't there? But it
may be a task to argue that they are "correctness properties".
C-B
> On the face of it the notion makes no sense.
>
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
Aatu Koskensilta
> To prove that "Provable => True" cannot be expressed, since "x is
> true" cannot be expressed.
The statement "for all sentences P in the language of S, if P is
provable in S then P is true" is obviously not expressible in S since
"P is true" is not.
> It depends on how you define correctness properties. There certainly
> are stronger properties that are expressible, aren't there? But it
> may be a task to argue that they are "correctness properties".
There are stronger correctness properties than omega-consistency or
1-consistency, certainly, e.g. soundness for Pi-17 sentences. In this
context it suffices to understand by correctness property any property
of theories implied by soundness. For some reason, I took your
original comment to be about correctness properties stronger than
soundness -- on re-reading your post I find a perfectly sensible
reading is also possible.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Charlie-Boo
> On Mar 10, 12:11 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > On Mar 10, 6:47 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> > wrote:
> > > Be a sport,
>
> > When have I not? (Unsubstantiated innuendo?)
>
> (1) No, he didn't insinuate that you're not a sport.
Ok, in that case: You really should consider using your brain. You
would be amazed at the results (that other people get) if you applied
a little bit of intelligence to a probelm rather than flying off the
handle all the time and attacking people's character.
> (2) But the
> answer to your question includes such instances as never getting back
> to me as to the purpose of your question about set theory that I
> answered in full (our very first discussion),
Oh No!! : ( MoeBlee mon ami, my budski - plz copy or link.
It's called "discovery", where you smoke out each other instead of
fighting battles. Like playing a game of chess rather than waging a
war. Sometimes they stand up and get shot at just to see the size and
direction of the enemy's line of fire.
> and not recognizing the
> examples given to you of theorems of mathematics proven by ZFC.
Oh, like 1+1=2? I was thinking about that, actually. Since ADD/PR
(addition is representable), we could try to derive the statement of
things like associativity by expanding it and applying the rules as
normal: ADD/PR = ADD(x,y,z)/PR => (aABC)
(eDEF)ADD(A,B,D)^ADD(D,C,E)^ADD(B,C,F)^ADD(A,F,E) I normally apply
CBL to Metamathematical problems (especially unsolved ones) rather
than Mathematical ones. (It does explain a lot about Fermat's Last
Problem, though. Much shorter than Wiles'. Did he win any money for
that?)
I always admitted that PA can prove things about arithmetic and the
ZFC axioms can prove some things about SETS (but all the important
questions can't be - most have been shown to be unanswered by ZFC and
it's just showmanship for anyone to even talk about using ZFC for
anything.) So together you can prove dinky little nothings, only.
(The big joke is, first they take 2,000 years and formalze basically
nothing - just Logic that is already formal anyway. Then they
announce that they have solved all possible remaining problems of
axiomatizing with 8 or 10 dumb little rules about what's in a set. So
in reality they've done nothing but then they claim to solve
everything! Now how could they possibly say anything more contrary to
the truth? Or be any more foolish or dishonest as that? It's totally
back-asswards.)
Can you prove the Pythagorean theorem in ZFC? I don't ask where I ask
how, so references are just claims that if you go to that source you
will find something satisfactory - just more unproved assertions (that
they expect you to prove for them!)
> By the way, did you ever figure out how to prove in Z set theory that
> if a set and its complement are recursively enumerable then the set is
> recursive?
In Z? Was I supposed to do that? (What's Z? There's the integers
and sports cars.) It's probably easy in CBL..
C-B
If you want to know the real problem, I can easily explain that. (My
postings rate a star they are so good.)
> MoeBlee
Charlie-Boo
What's with the Z? You want it in CBL? It's probably trivial. I
think it's an axiom, in fact.
C-B
> > MoeBlee
>
> --
> Alan Smaill- Hide quoted text -
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > I asked if every Metatheorem expressible in the loigic is provable in
> > the logic.
>
> What do you mean by "Metatheorem" here?
A theorem proven using metamathematics - a system other than the Logic
being discussed.
> A mathematical theorem about
> the system of course need not in general be provable in the system
> even when the theorem is expressible in the system.
>
> > Then I asked where an attempt to formalize its metaproof within the
> > logic fails, as in the case of a metatheorem involving truth that
> > you pointed out is not even expressible much less provable in the
> > logic.
>
> I am at loss as to what "Metatheorems" and "metaproofs" you have in
> mind. Theorems about the system that fail to be provable in it are
> those that can't be proved without appeal to principles not contained
> in the system.
>
> > I'll crank. It helps if you give me an on-line proof.
>
> You'll find a proof that Robinson arithmetic does not prove its
> consistency in
>
> /Godel's Second Incompleteness Theorem for Q/
> A. Bezboruah and J. C. Shepherdson
> The Journal of Symbolic Logic Vol. 41, No. 2 (Jun., 1976),
> pp. 503-512
That's online?
C-B
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
>
Aatu Koskensilta
>> /Godel's Second Incompleteness Theorem for Q/
>> A. Bezboruah and J. C. Shepherdson
>> The Journal of Symbolic Logic Vol. 41, No. 2 (Jun., 1976),
>> pp. 503-512
>
> That's online?
It's available through JSTOR. I also took the liberty of sending you
an electronic copy in e-mail.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > To prove that "Provable => True" cannot be expressed, since "x is
> > true" cannot be expressed.
>
> The statement "for all sentences P in the language of S, if P is
> provable in S then P is true" is obviously not expressible in S since
> "P is true" is not.
How's that?
> > It depends on how you define correctness properties. There certainly
> > are stronger properties that are expressible, aren't there? But it
> > may be a task to argue that they are "correctness properties".
>
> There are stronger correctness properties than omega-consistency or
> 1-consistency, certainly,
Stronger expressible properties. My original interest was provable
properties expressible but not provable within PA.
> e.g. soundness for Pi-17 sentences. In this
> context it suffices to understand by correctness property any property
> of theories implied by soundness. For some reason, I took your
> original comment to be about correctness properties stronger than
> soundness -- on re-reading your post I find a perfectly sensible
> reading is also possible.
>
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
MoeBlee
> On Mar 10, 3:58 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On Mar 10, 12:11 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > On Mar 10, 6:47 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> > > wrote:
> > > > Be a sport,
>
> > > When have I not? (Unsubstantiated innuendo?)
>
> > (1) No, he didn't insinuate that you're not a sport.
>
> Ok, in that case: You really should consider using your brain. You
> would be amazed at the results (that other people get) if you applied
> a little bit of intelligence to a probelm rather than flying off the
> handle all the time and attacking people's character.
I don't "all the time" attack people's character. In a few certain
cases, I do comment on what I find to be the poor character of some
people in their role of posting.
> > (2) But the
> > answer to your question includes such instances as never getting back
> > to me as to the purpose of your question about set theory that I
> > answered in full (our very first discussion),
>
> Oh No!! : ( MoeBlee mon ami, my budski - plz copy or link.
I've asked you about it for about two years since and NOW you ask me
for a link. I've given you refs to it already; I'm not going to again
try to track down where it was. It was in a thread in which you asked
for a formulation of the language of set theory. I gave you such a
formulation, but you would never answer as to what was the point of
that.
> It's called "discovery", where you smoke out each other instead of
> fighting battles. Like playing a game of chess rather than waging a
> war. Sometimes they stand up and get shot at just to see the size and
> direction of the enemy's line of fire.
More evidence that you're a putz.
> > and not recognizing the
> > examples given to you of theorems of mathematics proven by ZFC.
>
> Oh, like 1+1=2?
That's one, but not one that I mentioned. I mentioned a theorem in
topology (I could have mentioned hundreds, but I cited one just at
will). I mentioned the Bolzano-Weierstrass theorem (I could have
mentioned hundreds in analysis, but I cited one just at will).
> Can you prove the Pythagorean theorem in ZFC?
I'm working on a formulation of basic geometry as defined to be a
structure in Z set theory. Several theorems about lines, planes,
angles, and triangles are easy to prove right away. As I progress with
the work, I don't expect that the Pythagorean theorem will be
difficult to prove in this formulation. I already mentioned that if I
had a place to post PDF files then I could display the work as it
progresses.
> > By the way, did you ever figure out how to prove in Z set theory that
> > if a set and its complement are recursively enumerable then the set is
> > recursive?
>
> In Z? (What's Z? There's the integers
> and sports cars.)
Z SET THEORY [all caps now added], as I said and as you just QUOTED
me.
> Was I supposed to do that?
You kept saying that you don't know how it could be done and asked me
about it. Then I gave you a ref to the Boolos book, which you have.
You haven't said what in that proof you don't think can be carried out
in Z set theory.
> It's probably easy in CBL..
Yeah, sure.
MoeBlee
herbzet
Charlie-Boo wrote:
> Peter_Smith wrote:
> > the one you
> > mention is about the shortest even if we start from first principles.
>
> If you restrict the competition to a subset (those that "start from
> first principles") of what would constitute a proof, then naturally my
> rank on the brevity scale can only go up.
That depends how the scale is calibrated. In absolute length the
rank of your proof would naturally increase.
Relative to other proofs from first principles, yours will still
rank at, or near, the bottom, according to PS.
--
hz
herbzet
MoeBlee wrote:
> Charlie-Boo wrote:
> > It's called "discovery", where you smoke out each other instead of
> > fighting battles. Like playing a game of chess rather than waging a
> > war. Sometimes they stand up and get shot at just to see the size and
> > direction of the enemy's line of fire.
>
> More evidence that you're a putz.
Masterful. So effortless.
Is there an emoticon for "I bow to you"?
--
hz
Charlie-Boo
check your spelling
> --
> hz
Aatu Koskensilta
> On Mar 10, 4:46 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> wrote:
>
>> The statement "for all sentences P in the language of S, if P is
>> provable in S then P is true" is obviously not expressible in S since
>> "P is true" is not.
>
> How's that?
It's a basic result in mathematical logic, due to Tarski.
> Stronger expressible properties. My original interest was provable
> properties expressible but not provable within PA.
It's not provable in PA that PA is sound for Pi-17 sentences, but it
is provable using ordinary mathematical principles, and in e.g. the
formal theory ACA.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
Alan Smaill
you *think* it's an axiom?
where can I find the list of all CBL axioms?
> C-B
>
>> > MoeBlee
>>
--
Alan Smaill
Charlie-Boo
wrote:
> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>
> > On Mar 10, 4:46 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> > wrote:
>
> >> The statement "for all sentences P in the language of S, if P is
> >> provable in S then P is true" is obviously not expressible in S since
> >> "P is true" is not.
>
> > How's that?
>
> It's a basic result in mathematical logic, due to Tarski.
If you mean Tarski as in the fact that the set of true sentences isn't
expressible, then of course, its takes 4 steps in CBL (TW = the set of
true sentences):
1. -~P/P Axiom Diagonalization
2. -~TW/TW Sub 1:P=TW The set of untrue sentences is not
expressible.
3. P/TW => ~P/TW NOTX:TW (Property of TW) If P is expressible then
~P is expressible.
4. -TW/TW 2,3 The set of true sentences is not expressible.
qed
I asked if all nontrivial functions of TW were not expressible and you
did not commit. If true, then the above would be answered. Lacking a
response to the question of the general theorem, I ask for a proof of
this special case.
Also, if P is provable metamathematically but not expressible in
system T, is it possible that T can prove P? And how sure are you of
your answer? I mean, how much would you bet on it (in Euros)?
C-B
> > Stronger expressible properties. My original interest was provable
> > properties expressible but not provable within PA.
>
> It's not provable in PA that PA is sound for Pi-17 sentences, but it
> is provable using ordinary mathematical principles, and in e.g. the
> formal theory ACA.
>
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
Charlie-Boo
Name 2 authors who agree on what the ZF axioms are (or for that
matter, the CBL axioms).
> where can I find the list of all CBL axioms?
Here:
1. Program Synthesis e.g. for PHP programs
"function mul($a,$b){ return $a*$b ; }" # MUL(I,J,x)*/PHP We can
multiply.
"function lt($a,$b){ return $a<$b ; }" # LT(I,J)*/PHP We can decide
less than.
"function count($a){ for ($x=0;$x!>$a;++$x) echo $x ; }" # ~LT(I,x)*/
PHP We can count to any given number.
suffices to synthesize a program to decide if one number is a factor
of another (see ARXIV 2000 paper)
2. Theory of Computation
1. TRUE(x) The Universal Set is r.e.
2. EQ(I,J) The equality relation is r.e.
3. YIT(I,J,K)* Halting yes at a given iteration is a recursive
relation.
4. LT(I,J)* Less than is recursive.
5. ~LT(I,x)* We can count to any given number and halt.
Sufficies to prove (with definitions) Turing's 1937 unsolvability of
the halting problem and variations e.g. everhalting, always halting,
selfhalting unsolvable, and also e.g. the set of programs that halt no
is r.e. (see ARXIV 2000 paper.)
Also useful for modeling religion e.g. "God made the heaven and the
earth and on the 7th day he rested." is axiom TRUE(x)* where TRUE =
the heaven and the earth, x = made, and * = rested, and the Prophets
are -~P/P the Diagonalization/Incompleteness Axiom (all incompleteness
comes from our inability to predict the future.) Many religious
documents parallel the generation of CBL theorems. You will find
references to truth, provability, even the Liar Paradox.
Much overlap with Incompleteness in Logic. The difference is that
Turing only uses one base, Turing Machines, while Logic uses at least
two bases, the provable sentences and the true sentences. So we are
tempted to simplify Turing - but Turing is just a special case of the
wordier system Incompleteness in Logic.
3. Recursion Theory
1. I # yes(I) There is a function that defines the set enumerated or
accepted by Turing Machine number I.
2. wr(I) # I For every number (program, program input, and program
output) there is a program that writes it.
3. wr(I) There is a recursive function that gives a program that
writes any given number.
4. M # f(I) => s11(M,N) # f(N) If program M outputs function f, then
program s11(M,N) outputs the value of f(N).
5. s11(I,J) Substitution is recursive.
6. M # f(I,I) => twice(M) # f(I,I) Instance of Substitution - if
there is a program that computes function f(I,J) then there is a
program that computes f(I,I).
7. twice(I) Function twice is recursive.
Suffices to prove there is a selfoutputting program, the fixed point
theorem, recursion theorem, double recursion theorem and others. Also
well suited to represent the liar paradox, Godel-1, and other uses of
self-reference.
The axiom I # yes(I) implies yes(I) which in the Theory of Computation
is YES(I,x) which says that the set of numbers on which any given
program halts yes is r.e. You can see the overlap of the axioms.
(See discussion of higher level below.)
4. Incompleteness in Logic
1. PR/TW Provability is expressible.
2. PR/PR Provability is representable.
3. PRIT/PR* Proof x proves sentence y is a recursive relation.
4. -~P/P Diagonalization axiom: no base can represent its complement
(e.g. the set of programs that does not halt is not r.e., there is no
Russell Set, we cannot express nontruth, etc.)
5. P/TW => ~P/TW Property of true sentences.
This suffices to prove Godel-1 based on soundness, Godel-1 based on w-
consistency, Godel-2, Rosser, Smullyan's Dual Form theorem and others.
Altogether at least 100 of the approximately 200 distinct theorems
that Smullyan gives in his 4 texts (ignoring results in his puzzle
books) are derivable in CBL. (I have uncovered errors in his texts
while doing that.)
5. Set Theory
We can state most of the standard axioms of Set Theory pretty easily.
Many are theorems from more primitive axioms than those given in
print. For example, Pairing is theorem EQ(I,x)vEQ(J,x) from axioms
EQ(I,x) for every thing there is a set that contains just it, and P,Q
=> PvQ the union of two sets is a set. Comprehension is P/SE , Q/TW
=> P^Q/SE.
When you formalize these axioms in CBL you notice that they refer to
other mathematical objects like functions and wffs, without giving
axioms (formal definitions) for them. And remember that not being
exact about what a wff consists of is what gets us in trouble with the
Russell Paradox.
Higher level:
The higher level of this is Computer Science. We can formalize each
branch with a CBL wff that gives the basic process that is occurring.
From this we should be able to create the axioms, but that question is
on the cutting edge of current research.
For example, Program Synthesis is x # I / YES: Input mathematical
object/process (e.g. function to calculate or set to enumerate or
decide) and output programs that solve it in Turing Machines. The
Theory of Computation is -x/YES and x/YES i.e. list the non-r.e. sets
(e.g. the nonhalting set) and list the r.e. sets (e.g. the halting
set) as well as -x*/YES list the non-recursive sets (e.g. the halting
set) and variations that suggest new branches of Computer Science e.g.
x # yes(I) / PR: How do we translate a computer program into a wff
that represents the same set?
C-B
Alan Smaill
For the first, Takeuti and Zaring.
For the second, how come *you* don't know?
>> where can I find the list of all CBL axioms?
>
> Here:
>
> 1. Program Synthesis e.g. for PHP programs
"e.g." doesn't cut it.
So, there is no complete list of CBL axioms; far from being a dinky
little system like ZF, it's not even properly defined to start with.
--
Alan Smaill
Charlie-Boo
I think they're brothers.
> For the second, how come *you* don't know?
>
> >> where can I find the list of all CBL axioms?
>
> > Here:
>
> > 1. Program Synthesis e.g. for PHP programs
>
> "e.g." doesn't cut it.
Please read the rest and comprehend. There are an infinite number of
programming languages. I show the axioms for one enough to synthesize
a useful program nobody else has ever synthesized, the test for being
a factor.
People who write about a Program Synthesis system without reference to
the programming language are already BSing you. The axioms depend on
the language.
(I synthesize two different programs, that use differemt algorithms,
something those who translate one programming language into another
cannnot do. I can also complement each request: list all factors or
list all nonfactors, something else inputting a program cannot do as
you can input a program to list all prgrams that halt but you cannot
input the complement.)
> So, there is no complete list of CBL axioms;
See above.
> far from being a dinky
> little system like ZF, it's not even properly defined to start with.
ZF does nothing useful. It's axioms are not even enough to decide any
useful question about sets. What it does do is to show silly little
statements about sets that we already know are true. What new fact -
or any fact the least bit subtle - has it shown?
The real intent was to say they fixed the Russell Paradox because it
is all formal, but what they have is no solution as it doesn't provide
the facilities needed in an axiomatization: to be able to decide
questions about Set Theory. (CBL decides numerous questions about all
sorts of branches of CS.)
What new facts has ZF shown us? Rememeber, that's ZF, the 8 or 10
axioms.
(The real source of the problem is that they are inconsistent about
what a wff can contain. "Can a wff contain a reference to something
that is not a set?" The Russell Paradox occurs because they are
inconsistent on this question. Pick an answer (yes or no) and there
is no Paradox if you keep that answer in mind. They never thought of
it because they didn't even know there was such a thing as a non-set.
In fact, some still say to this day that "Everything is a set."!! {x|
~(x e x)} is not.
This is common in "Paradoxes" e.g. Unexpected Exam/Hanging and God
Paradox are the same. "Can we expect more than once?" is not
addressed and is inconsistently implied and refuted by the logic
used. This is all shown clearly by CBL, which is why I am able to
post so many proofs of theorems of Godel/Rosser/Turing et. al. One
proof generated by CBL was called the shortest one for Godel-1 by an
author of a book on Godel's Theorems, and I immediately provided a
shorter one - so that must be unpublished so far (outside of Google
Groups.)
C-B
Charlie-Boo
> Charlie-Boo wrote:
> > Peter_Smith wrote:
> > > the one you
> > > mention is about the shortest even if we start from first principles.
>
> > If you restrict the competition to a subset (those that "start from
> > first principles") of what would constitute a proof, then naturally my
> > rank on the brevity scale can only go up.
>
> That depends how the scale is calibrated. In absolute length the
> rank of your proof would naturally increase.
So my rank - the number of others above me plus one - will improve if
anything.
> Relative to other proofs from first principles, yours will still
> rank
But the quextion was not the rank, but rather the change to the rank,
and the change is only to improve.
> at, or near, the bottom, according to PS.
Where? He said, "And the one you mention is about the shortest even
if we start from first principles.", the opposite.
C-B
> --
> hz
>
>
>
> > C-B
>
> > > One of my other favourites is the proof that Kleene's normal form
> > > theorem entails incompleteness.- Hide quoted text -
MoeBlee
> ZF does nothing useful.
At the very least it provides an axiomatization for a vast amount of
mathematics. If that is not useful to you personally, then so be it.
> It's axioms are not even enough to decide any
> useful question about sets.
It depends on what you mean by "useful". In any case, ZF does decide a
vast amount about sets and mathematics.
> What it does do is to show silly little
> statements about sets that we already know are true. What new fact -
> or any fact the least bit subtle - has it shown?
(1) Even if it served only to axiomatize results already known, it
would have value. (2) New set theoretic results are published all the
time. Whether known before or not, one fact is that in Z it's not the
case that for every set S we have the set of tuples (tuples taken as
iterations of ordered pairing) of members of S, but in ZF we do.
> The real intent was to say they fixed the Russell Paradox because it
> is all formal,
The real intent of what? Of ZF specifically? No, that was not the
intent of formulating ZF.
> but what they have is no solution as it doesn't provide
> the facilities needed in an axiomatization: to be able to decide
> questions about Set Theory. (CBL decides numerous questions about all
> sorts of branches of CS.)
It is an incomplete theory, as is any consistent recursively
axiomatized theory in which we can define all the primitive recursive
functions.
> What new facts has ZF shown us?
> Rememeber, that's ZF, the 8 or 10
> axioms.
All kinds of things are provable in ZF that are not provable in Z. I
just mentioned one earlier in this post.
> (The real source of the problem is that they are inconsistent about
> what a wff can contain.
There's no such inconsistency. The definition of a wff in the language
of ZF is precise.
> "Can a wff contain a reference to something
> that is not a set?"
That's not even a coherent question.
> The Russell Paradox occurs because they are
> inconsistent on this question.
You're showing your ignorance and confusion in bright colors now.
> Pick an answer (yes or no) and there
> is no Paradox if you keep that answer in mind. They never thought of
> it because they didn't even know there was such a thing as a non-set.
> In fact, some still say to this day that "Everything is a set."!! {x|
> ~(x e x)} is not.
You desparately need instruction in basic mathematical logic,
especially the subjects of improperly referring terms and variable
binding notation.
MoeBlee
Chris Menzel
<shyma...@gmail.com> said:
> On Mar 11, 7:40 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
> wrote:
>> On 2008-03-10, in sci.logic, Charlie-Boo wrote:
>>
>> > On Mar 10, 4:46 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
>> > wrote:
>>
>> >> The statement "for all sentences P in the language of S, if P is
>> >> provable in S then P is true" is obviously not expressible in S since
>> >> "P is true" is not.
>>
>> > How's that?
>>
>> It's a basic result in mathematical logic, due to Tarski.
>
> If you mean Tarski as in the fact that the set of true sentences isn't
> expressible, then of course, its takes 4 steps in CBL (TW = the set of
> true sentences):
>
> 1. -~P/P Axiom Diagonalization
> 2. -~TW/TW Sub 1:P=TW The set of untrue sentences is not
> expressible.
> 3. P/TW => ~P/TW NOTX:TW (Property of TW) If P is expressible then
> ~P is expressible.
> 4. -TW/TW 2,3 The set of true sentences is not expressible.
> qed
This strikes me as a good example of what seems to me to be the central
problem of CBL. Nothing seems to be fixing the meaning of your symbols
beyond your own intentions. What, for example, is the meaning of "true
sentence"? What makes it the case that "TW" denotes the set of true
sentences? And do you really mean the set of true sentences or their
Gödel numbers? If so, what numbering are you using? What fixes the
meaning of your symbol "-"? Is it axiomatized somewhere? What is a
property? And what does it mean for a property to be expressible? Do
you mean arithmetically expressible? How do we know? AFAICS, none of
these questions is answered in your papers, which, if true, means that,
e.g., the conclusion of your proof above only means what it does in your
head; it has no mathematical content.
Chris Menzel
<shyma...@gmail.com> said:
> ...
> ZF does nothing useful.
Well, usefulness is admittedly relative to one's purposes. If you have
no interest in sets, for example, ZF is of course not very useful to
you.
> The real intent was to say they fixed the Russell Paradox
Actually, no one ever said that. The original motivation was simply to
*avoid* RP by blocking the usual routes to its derivation. In addition,
the intent was to make clear and explicit all of the assumptions needed
to be able to do all of the desired mathematics. Mathematicians since
Euclid have thought this sort of thing was a pretty good idea. Don't
you agree? As research in ZF progressed, a clear picture of the
structure of the set theoretic universe began to emerge more clearly.
With this, ZF began to be viewed less pragmatically than it had
originally and more as the principles describing a particular
well-defined mathematical structure (or perhaps more accurately, a class
of them), just as the axioms of PA describe the natural number
structure. You should perhaps actually *learn* something about the
history of set theory rather than pulling myths out of your ass.
> because it is all formal, but what they have is no solution as it
> doesn't provide the facilities needed in an axiomatization: to be able
> to decide questions about Set Theory.
That's a bizarre claim (whatever it's supposed to mean). All that is
needed in an axiomatization are some axioms. Of course, there are lots
of adequacy conditions we might impose relative to the purpose of the
axiomatization. The original conditions on ZF were (i) to block the
usual derivations of the paradoxes and (ii) to preserve all of the
useful mathematics that set theory had enabled. By those criteria it
was a resounding success.
> (CBL decides numerous questions about all sorts of branches of CS.)
That is really doubtful. I doubt whether you have even formulated a
rigorous definition of what it is for CBL to decide a question.
> What new facts has ZF shown us?
Oh, I was under the impression you at least knew a little set theory.
My mistake. How about that every singular limit ordinal k with
cofinality < card(k) lacks the Souslin property? Or maybe the Stone
Representation theorem (every Boolean Algebra is isomorphic to a field
of sets)? The fact that every normal function on the ordinals has
arbitrarily large fixed points?
> Rememeber, that's ZF, the 8 or 10 axioms.
(First-order) ZF has infinitely many axioms. You don't know this?
> (The real source of the problem is that they are inconsistent about
> what a wff can contain.
Who are "they"?
> "Can a wff contain a reference to something that is not a set?"
In ZF, the answer to this is trivially "no".
> The Russell Paradox occurs because they are inconsistent on this
> question.
You really have absolutely no idea what you're talking about.
> Pick an answer (yes or no) and there is no Paradox if you keep that
> answer in mind. They never thought of it because they didn't even
> know there was such a thing as a non-set. In fact, some still say to
> this day that "Everything is a set."!!
And in the context of pure ZF, that is trivially true. It is of course
not true in other theories like VNBG or KPU.
> {x| ~(x e x)} is not.
Indeed. And in ZF you can't refer to it.
> This is common in "Paradoxes" e.g. Unexpected Exam/Hanging and God
> Paradox are the same. "Can we expect more than once?" is not
> addressed and is inconsistently implied and refuted by the logic used.
> This is all shown clearly by CBL, which is why I am able to post so
> many proofs of theorems of Godel/Rosser/Turing et. al. One proof
> generated by CBL was called the shortest one for Godel-1 by an author
> of a book on Godel's Theorems, and I immediately provided a shorter
> one - so that must be unpublished so far (outside of Google
> Groups.)
Name of the "author" and a reference to your historic proof might make
your claim a bit more credible.
Charlie-Boo
> On Mar 12, 10:06 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > ZF does nothing useful.
>
> At the very least it provides an axiomatization for a vast amount of
> mathematics. If that is not useful to you personally, then so be it.
The only thing ZF does is dinky little stuff we already knew about
sets. Peano's Axioms already existed for arithmetic. Nothing else
uses the ZF axioms. What proof actually uses the ZF axioms outside of
sets and arithmetic? For example, how would you prove the Pythagorean
Theorem using the ZF axioms? Answer: It doesn't do that - it only
does sets and arithmetic.
> > It's axioms are not even enough to decide any
> > useful question about sets.
>
> It depends on what you mean by "useful". In any case, ZF does decide a
> vast amount about sets and mathematics.
What does ZF decide that we didn't already know - and is trivial at
that?
> > What it does do is to show silly little
> > statements about sets that we already know are true. What new fact -
> > or any fact the least bit subtle - has it shown?
>
> (1) Even if it served only to axiomatize results already known, it
> would have value. (2) New set theoretic results are published all the
> time. Whether known before or not, one fact is that in Z it's not the
> case that for every set S we have the set of tuples (tuples taken as
> iterations of ordered pairing) of members of S, but in ZF we do.
>
> > The real intent was to say they fixed the Russell Paradox because it
> > is all formal,
>
> The real intent of what? Of ZF specifically? No, that was not the
> intent of formulating ZF.
Why then? The 1st reference I checked is Classic Set Theory,
Goldrei. Page 66: "The theory of sets had alraming and deep
problems. The axioms of set theory are designed to avoid these
problems."
> > but what they have is no solution as it doesn't provide
> > the facilities needed in an axiomatization: to be able to decide
> > questions about Set Theory. (CBL decides numerous questions about all
> > sorts of branches of CS.)
>
> It is an incomplete theory, as is any consistent recursively
> axiomatized theory in which we can define all the primitive recursive
> functions.
But rather than missing queer statements about whether "For All Proofs
If it proves this doesn't halt then do halt" halts or not (which is
what PA is missing), it is missing fundamental questions such as
deciding the Continuum Hypothesis, and we have to spend decades
figuring out it's impossible for ZF to do it - it's just too dinky.
That's the mathematical truth.
> > What new facts has ZF shown us?
> > Rememeber, that's ZF, the 8 or 10
> > axioms.
>
> All kinds of things are provable in ZF that are not provable in Z. I
> just mentioned one earlier in this post.
What has it proven that we didn't already know?
> > (The real source of the problem is that they are inconsistent about
> > what a wff can contain.
>
> There's no such inconsistency. The definition of a wff in the language
> of ZF is precise.
>
> > "Can a wff contain a reference to something
> > that is not a set?"
>
> That's not even a coherent question.
Wffs refer to relations (sets.) Can they refer to non-sets there?
Wffs contain operations on relations. Can those operations be done on
nonrelations?
The problem was they figured every wff defined a set based on the wff
being true when a value is substituted for a free variable. Then they
thought of {x|~(x e x)} and there was a wff that was not a set. So
they said, ok, a wff is not always a set.
But there are only aleph-1 wffs and aleph-2 sets of numbers alone, so
there are plent more sets than wffs and we can say that there is in
fact a set for every wff. It is counter-intuitive to say sets do not
include what all wffs define.
In any case, they set out to define what any set can define, when the
real problem was they needed to be exact about terms such as wff.
If you first decide if a wff can make a reference to something that is
not a set, then if yes, then naturally these wffs are not sets, and if
no, then the {x|~(x e x)} example is NOT a set and we still have each
wff defining a set. So we don't really need to worry about what's in
a set as we do in ZF. We just need to be careful about the formal
system - what is the real syntax of a wff? Can it contain references
to nonsets?
C-B
> > The Russell Paradox occurs because they are
> > inconsistent on this question.
>
> You're showing your ignorance and confusion in bright colors now.
>
> > Pick an answer (yes or no) and there
> > is no Paradox if you keep that answer in mind. They never thought of
> > it because they didn't even know there was such a thing as a non-set.
> > In fact, some still say to this day that "Everything is a set."!! {x|
> > ~(x e x)} is not.
>
> You desparately need instruction in basic mathematical logic,
No, CBL is a lot better.
Charlie-Boo
The same as in classical logic. You don't have to worry about
"interpretations" - you can think of it as always being the "standard
interpretation", or take the CBL approach: a wff contains references
to relations, and any use of variables (symbols) that are replaced by
relations is not needed, as it is just a way to define the same wffs
that consist of references to relations.
> And do you really mean the set of true sentences or their
> Gödel numbers?
You can think of the universal set as being the natural numbers or the
finite strings - any r.e. set. The Turing Machine can operate on a
string of 0 and 1 that represents the Godel number of a wff, or on a
string that spells out the wff as we are used to seeing it. But the
result is the same in terms of the theory.
> If so, what numbering are you using? What fixes the
> meaning of your symbol "-"?
-E means that expression E is not true. This allows me to use ~ for
negation withing parts of expressions.
- Is it axiomatized somewhere?
The only real use is in proofs where we prove w and also prove -w to
show an inconsistency, and to represent theorems e.g. -HALT(I,J)*
means the Halting Problem is unsolvable.
> What is a
> property? And what does it mean for a property to be expressible?
Wff M expresses set P if x is in P iff M with its free variables
replaced by x is a true sentence.
> Do you mean arithmetically expressible? How do we know?
It is common for authors to say that a system of logic includes sets
and give names to them e.g. T, P, R for true, provable and refutable
sentences, and then make statements about them that are true in the
common systems of logic. Smullyan actually redid his system between
his 1960's book and his three 1990's books, using a single set that
represented both True and Provable!
> AFAICS, none of
> these questions is answered in your papers, which, if true, means that,
> e.g., the conclusion of your proof above only means what it does in your
> head; it has no mathematical content.- Hide quoted text -
I leave out what is commonly defined and only refer to its common
name, and give details of what CBL adds to Mathematical Logic:
expressions of the form M # P / Q and P / Q that represent semantics
which is normally only defined for special cases of Q, for kludge
definitions of representable, expressible, r.e., well-founded, rather
than in terms of properties of bases in general.
- ~P / P Diagonalization Axiom
P(M) / P
M # P(M) / P
P / Q + Q / R => P / R Transitivity (Theorem)
These are the highest level axioms and theorems.
C-B
William Hale
<f48930d8-4dd7-4e84...@u72g2000hsf.googlegroups.com>,
Charlie-Boo <shyma...@gmail.com> wrote:
[cut]
> the CBL approach: a wff contains references
> to relations, and any use of variables (symbols) that are replaced by
> relations is not needed, as it is just a way to define the same wffs
> that consist of references to relations.
True. But this is what, for example, Dedekind opposed and which he
recommended set theory as a better approach.
For one example, consider how Euclid handled real numbers. See the link:
http://aleph0.clarku.edu/~djoyce/java/elements/bookV/defV5.html
Quote:
================================
Def. 5. Magnitudes are said to be in the same ratio, the first to the
second and the third to the fourth, when, if any equimultiples whatever
are taken of the first and third, and any equimultiples whatever of the
second and fourth, the former equimultiples alike exceed, are alike
equal to, or alike fall short of, the latter equimultiples respectively
taken in corresponding order.
================================
End quote.
Here, Euclid (really Eudoxus) uses this property or relation to handle
proofs for real numbers. It is prone to error and complicates proofs.
For example, see how Archimedes proves his theorems on the lever.
Dedekind used his Dedekind cuts to simplify proving things about real
numbers.
For another example, consider how Kummer defined ideal numbers:
Quote from "Theory of Algebraic Integers" translated by Stillwell, page
57:
================================
Kummer did not define ideal numbers themselves, but only the
divisibility of these numbers. If a number alpha has a certain property
A, to the effect that alpha satisfies one or more congruences, he says
that alpha is divisible by an ideal number corresponding to the property
A. While this introduction of new numbers is entirely legitimate, it is
nevertheless to be feared at first that the language which speaks of
ideal numbers being determined by their products, presumably in analogy
with the theory of rational numbers, may lead to hasty conclusions and
incomplete proofs.
================================
Dedekind used his theory of ideals (certain sets of numbers) to simplify
proving things about algebraic numbers.
Chris Menzel
<shyma...@gmail.com> said:
> ...
> Wffs refer to relations (sets.) Can they refer to non-sets there?
> Wffs contain operations on relations. Can those operations be done on
> nonrelations?
>
> The problem was they figured every wff defined a set based on the wff
> being true when a value is substituted for a free variable. Then they
> thought of {x|~(x e x)} and there was a wff that was not a set. So
> they said, ok, a wff is not always a set.
My god. What must it be like to be so profoundly muddle-headed? I
really do feel badly for you.
> But there are only aleph-1 wffs
Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
> and aleph-2 sets of numbers alone,
You probably mean aleph_1 -- though, so understood, your claim assumes
the continuum hypothesis. You might find it helpful to try to
understand why. Good luck!
> so there are plent more sets than wffs and we can say that there is in
> fact a set for every wff. It is counter-intuitive to say sets do not
> include what all wffs define.
>
> In any case, they set out to define what any set can define, when the
> real problem was they needed to be exact about terms such as wff.
>
> If you first decide if a wff can make a reference to something that is
> not a set, then if yes, then naturally these wffs are not sets, and if
> no, then the {x|~(x e x)} example is NOT a set and we still have each
> wff defining a set. So we don't really need to worry about what's in
> a set as we do in ZF. We just need to be careful about the formal
> system - what is the real syntax of a wff? Can it contain references
> to nonsets?
The depth of your confusion is truly great. In this light your profound
ignorance of the history and content of set theory is more
understandable. I will read your posts with more compassion in the
future.
Alan Smaill
> On Mar 12, 12:11 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 11, 1:07 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> >> Charlie-Boo <shymath...@gmail.com> writes:
...
>> >> > What's with the Z? You want it in CBL? It's probably trivial. I
>> >> > think it's an axiom, in fact.
>>
>> >> you *think* it's an axiom?
>>
>> > Name 2 authors who agree on what the ZF axioms are (or for that
>> > matter, the CBL axioms).
>>
>> For the first, Takeuti and Zaring.
>
> I think they're brothers.
sigh ...
>> For the second, how come *you* don't know?
>>
>> >> where can I find the list of all CBL axioms?
>>
>> > Here:
>>
>> > 1. Program Synthesis e.g. for PHP programs
>>
>> "e.g." doesn't cut it.
>
> Please read the rest and comprehend. There are an infinite number of
> programming languages. I show the axioms for one enough to synthesize
> a useful program nobody else has ever synthesized, the test for being
> a factor.
That's just it ... I ask for the list of *all* axioms, and
you reply with examples.
I can get a one line proof of Godel's theorem by taking it as an axiom --
hey, you think that's a plus, don't you?
You yourself don't even know what the axioms are in an area you claim
CBL is a world beater.
> People who write about a Program Synthesis system without reference to
> the programming language are already BSing you. The axioms depend on
> the language.
Of course they do;
but those devious academics nevertheless gove a *complete* axiomatisation
of the systems they are working in. CBL does not.
>> So, there is no complete list of CBL axioms;
>
> See above.
your acceptance of the fact noted.
>> far from being a dinky
>> little system like ZF, it's not even properly defined to start with.
>
> ZF does nothing useful. It's axioms are not even enough to decide any
> useful question about sets.
it *is* a dinky system though --
I have this on the authority of Charlie-Boo.
> C-B
>
>> --
--
Alan Smaill
Charlie-Boo
wrote:
> On Wed, 12 Mar 2008 19:55:01 -0700 (PDT), Charlie-Boo
> <shymath...@gmail.com> said:
>
> > ...
> > Wffs refer to relations (sets.) Can they refer to non-sets there?
> > Wffs contain operations on relations. Can those operations be done on
> > nonrelations?
>
> > The problem was they figured every wff defined a set based on the wff
> > being true when a value is substituted for a free variable. Then they
> > thought of {x|~(x e x)} and there was a wff that was not a set. So
> > they said, ok, a wff is not always a set.
>
> My god. What must it be like to be so profoundly muddle-headed? I
> really do feel badly for you.
>
> > But there are only aleph-1 wffs
>
> Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
>
> > and aleph-2 sets of numbers alone,
I give a cardinality of aleph-0 to finite sets, but whatever numbers
you want is fine with me - like whether Peano starts with 0 or 1.
> You probably mean aleph_1 -- though, so understood, your claim assumes
> the continuum hypothesis. You might find it helpful to try to
> understand why. Good luck!
>
> > so there are plent more sets than wffs and we can say that there is in
> > fact a set for every wff. It is counter-intuitive to say sets do not
> > include what all wffs define.
>
> > In any case, they set out to define what any set can define, when the
> > real problem was they needed to be exact about terms such as wff.
>
> > If you first decide if a wff can make a reference to something that is
> > not a set, then if yes, then naturally these wffs are not sets, and if
> > no, then the {x|~(x e x)} example is NOT a set and we still have each
> > wff defining a set. So we don't really need to worry about what's in
> > a set as we do in ZF. We just need to be careful about the formal
> > system - what is the real syntax of a wff? Can it contain references
> > to nonsets?
>
> The depth of your confusion is truly great. In this light your profound
> ignorance of the history and content of set theory is more
> understandable. I will read your posts with more compassion in the
> future.
You haven't answered the question either (the source of the problem
with the Russell Paradox.) A wff can reference relations (sets) e.g.
(all x)P(x) refers to relation P. May a wff contain a reference to
something instead of the relation and use a non-relation there? If
f(some relation) is a wff then is f(something not a relation)
necessarily a wff as well? When we see in a wff (all x) . . . must
the . . . be a reference to a relation e.g. P(x) above or can wffs
contain a non-relation for the . . . ?
The fact of the matter is, naive set theory is right, they were just
confused as to how to define wffs after it was discovered that there
were things that are not sets. You are not showing any better ability
to grapple with the question, even with a guide.
If (all x)_(x) is a wff for something in place of the _ could that
something be other than a relation?
C-B
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 12, 12:11 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > On Mar 11, 1:07 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> >> >> Charlie-Boo <shymath...@gmail.com> writes:
> ...
> >> >> > What's with the Z? You want it in CBL? It's probably trivial. I
> >> >> > think it's an axiom, in fact.
>
> >> >> you *think* it's an axiom?
>
> >> > Name 2 authors who agree on what the ZF axioms are (or for that
> >> > matter, the CBL axioms).
>
> >> For the first, Takeuti and Zaring.
>
> > I think they're brothers.
>
> sigh ...
phi ...
> >> For the second, how come *you* don't know?
>
> >> >> where can I find the list of all CBL axioms?
>
> >> > Here:
>
> >> > 1. Program Synthesis e.g. for PHP programs
>
> >> "e.g." doesn't cut it.
>
> > Please read the rest and comprehend. There are an infinite number of
> > programming languages. I show the axioms for one enough to synthesize
> > a useful program nobody else has ever synthesized, the test for being
> > a factor.
>
> That's just it ... I ask for the list of *all* axioms, and
> you reply with examples.
There are an infinite number of programming languages. For the ones
used as output to your Program Synthesis system, you give axioms for
the constructs in that language. Most languages are terribly
redundant - theoretically all they need is constants, if, addition,
loops. But there are bigger constructs such as multiplication and it
makes better programs if it can use that as well, so we need to
include enough to cover the domain we are in.
Three of the constructs in the PHP programming language are operators
< and * and control structure for (expr;expr;expr). These are
formalized by using references to wff LT(I,J)* and MUL(I,J,x)* and
~LT(I,x)* which mean that less than is recursive, multiplication is
recursive, and we can enumerate in a finite time the elements of {x|
~LT(I,x)} for any given value of I.
Published papers on Program Synthesis give no examples of the
synthesis of a real program. They don't even mention how the
particular programming language is handled. There are different
semantics structures in different languages. Some are procedural
(with GOTOs) and others are definitional (no GOTOs) with special
control structures e.g. go through all elements of a finite stored
set, or go through the elements of a set logically defined by
mathematical expressions.
Program Synthesis in CBL is real, so that you have:
1. Lots of examples.
2. Examples use real programs e.g. determine if one number is a factor
of another, or list the prime factors of a given number. These are
programs used all the time.
The BS articles talk about creating "a program of a given type".
That's just something made up by the authors of the paper. It's not
an existing program synthesis problem. How does that actually relate
to the problem of Program Synthesis - creating the set of recursive
functions? And how does that relate to the functions over numbers
that are really what occurs in programs, both mathematical and
theoretical? E.g. both PA and Turing Machines use the natural numbers
as the universal set - and CBL does as well.
3. Reference to the Programming Language. You will see where each
construct is defined in the Program Synthesis process. The syntax and
semantics of a Programming Language is arbitrary - we have to code in
there somewhere what is in the language in which the system must wrote
programs.
Some BSers go so far as to say, "We produce XYZ wffs and of course we
can easily translate them into computer programs." and never do. But
they are not even showing that they are in fact faithfully
representing the wffs and that they are in fact able to solve the
problem of creating computer programs from that.
They are saying, "It's theoretically possible, so why bother?" - but
the question isn't whether or not it is theoretically possible, but
rather who has succeeded at doing it. Without examples to prove that
it works, they cannot honestly make the claim that they did. If it
worked, they would have examples of it working.
> I can get a one line proof of Godel's theorem by taking it as an axiom --
> hey, you think that's a plus, don't you?
That is an interesting discussion in itself - where Axioms should lie
and what is reasonable. I have argued that the bulk of the Godel 1931
and Turing 1937 papers is showing the same property of Logic and
Turing Machines, and there is no reason to generalize (axiomatize) it,
since there is not a stream of systems to do, but rather a small
number of very different ones, each with an infinite number of wffs.
If we need a new system, we need a new axiomatization, as that is the
same question.
Someone should start a thread asking what is a reasonable
axiomatization in that regard.
> You yourself don't even know what the axioms are in an area you claim
> CBL is a world beater.
See above. I can't list all infinity (aleph-whatever) Programming
Languages.
> > People who write about a Program Synthesis system without reference to
> > the programming language are already BSing you. The axioms depend on
> > the language.
>
> Of course they do;
> but those devious academics nevertheless gove a *complete* axiomatisation
> of the systems they are working in.
As far as Program Synthesis goes, they don't give anything at all -
example programs, the formal program spec, how the program is
created. They show a bunch of their buzzwords and junk, and there is
no standard in use as to how they can be held accountable.
I have given axioms (and theorems) for results in Program Synthesis,
Theory of Computation, Recursion Theory, Incompleteness in Logic. The
axioms are given above. What are the axioms for these branches of
Computer Science that have been published? NONE $1 for each axiom.
(Once I get my site going, I will offer substantial money for
examples, to prove that there are none. The money will come from
advertisers, especially booksellers. Readers will scour the Internet
to assure the lowest prices are offered my readers. I don't want to
jump the gun on the awards right now. I should say, the Center for
Boolean Learning will be officially offering the awards. Some may go
quickly, such as the formalization of Propositional Calculus. Others
e.g. Recursion Theory, will likely stay unsolved for awhile, and
especially Program Synthesis, where they have made 0 progress - I know
the stages of understanding of that problem, and they haven't done
step 1, 2, . . . Like formalize the relationship between program and
spec, use the Theory of Computation model, prove that the program
meets the spec. These are the starting points, and they haven't done
any of that at all. Phase one is to establish the truth - the true
state of the art in formalizing Computer Science and Mathematics.
Phase 2 is how we can continue the development. That's where I have
something to say myself. All are welcome.)
> CBL does not.
>
> >> So, there is no complete list of CBL axioms;
>
> > See above.
>
> your acceptance of the fact noted.
>
> >> far from being a dinky
> >> little system like ZF, it's not even properly defined to start with.
>
> > ZF does nothing useful. It's axioms are not even enough to decide any
> > useful question about sets.
>
> it *is* a dinky system though --
> I have this on the authority of Charlie-Boo.
Anyone who takes the time to open their eyes.
C-B
> > C-B
>
> >> --
Jesse F. Hughes
> I give a cardinality of aleph-0 to finite sets, but whatever numbers
> you want is fine with me - like whether Peano starts with 0 or 1.
So all finite sets have the same cardinality, namely aleph-0?
--
Jesse F. Hughes
"Liberals have hijacked science for long enough. Now it's our turn."
-- From the cover of "The Politically Incorrect Guide to Science"
Charlie-Boo
> In article
> <f48930d8-4dd7-4e84-8faf-acd6aca99...@u72g2000hsf.googlegroups.com>, Charlie-Boo <shymath...@gmail.com> wrote:
>
> [cut]
>
> > the CBL approach: a wff contains references
> > to relations, and any use of variables (symbols) that are replaced by
> > relations is not needed, as it is just a way to define the same wffs
> > that consist of references to relations.
>
> True. But this is what, for example, Dedekind opposed and which he
> recommended set theory as a better approach.
When we are applying the meaning of truth to a wff, it is the same
rules whether that wff consists of variables and a map from variables
to relations, or references to the relations themselves. However, the
former must be translated into the latter.
So if we are to define the rules of truth, do we need to talk about
how to translate the expression with variables into one without?
After all, that has nothing to do with how we evaluate truth - truth
or falsity occurs only with the latter form, the expression where the
relation is given.
C-B
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
> > you want is fine with me - like whether Peano starts with 0 or 1.
>
> So all finite sets have the same cardinality, namely aleph-0?
On the infinity scale viz. finite.
It all has to do with loops in computer programs, you know - how many
loops it takes to process the finite subset of the world that man will
ever see.
C-B
Jesse F. Hughes
> On Mar 13, 2:53 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
>> > you want is fine with me - like whether Peano starts with 0 or 1.
>>
>> So all finite sets have the same cardinality, namely aleph-0?
>
> On the infinity scale viz. finite.
>
> It all has to do with loops in computer programs, you know - how many
> loops it takes to process the finite subset of the world that man will
> ever see.
I asked a yes/no question.
Maybe you're not so good with yes/no. I'll try true/false:
T/F Every finite set has the same cardinality.
--
Jesse F. Hughes
"What does soap kill? Germs or Germans?"
-- Quincy P. Hughes (age 3 1/2) asks for clarification
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 13, 2:53 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
> >> > you want is fine with me - like whether Peano starts with 0 or 1.
>
> >> So all finite sets have the same cardinality, namely aleph-0?
>
> > On the infinity scale viz. finite.
>
> > It all has to do with loops in computer programs, you know - how many
> > loops it takes to process the finite subset of the world that man will
> > ever see.
>
> I asked a yes/no question.
I gave an implicit yes.
> Maybe you're not so good with yes/no. I'll try true/false:
>
> T/F Every finite set has the same cardinality.
Are you saying that this is a request directly from Torkel/Franzen?
Did you know that he spent his last days of this level of abstraction
working in CBL? It's true. Look up his last posts.
In ZFC or CBL?
C-B
Is this a trick question?
Jesse F. Hughes
> On Mar 13, 3:43 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 13, 2:53 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> >> Charlie-Boo <shymath...@gmail.com> writes:
>> >> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
>> >> > you want is fine with me - like whether Peano starts with 0 or 1.
>>
>> >> So all finite sets have the same cardinality, namely aleph-0?
>>
>> > On the infinity scale viz. finite.
>>
>> > It all has to do with loops in computer programs, you know - how many
>> > loops it takes to process the finite subset of the world that man will
>> > ever see.
>>
>> I asked a yes/no question.
>
> I gave an implicit yes.
If you say so. Okay, so every finite set has the same cardinality.
Well, that *is* revolutionary.
>> Maybe you're not so good with yes/no. I'll try true/false:
>>
>> T/F Every finite set has the same cardinality.
>
> Are you saying that this is a request directly from Torkel/Franzen?
> Did you know that he spent his last days of this level of abstraction
> working in CBL? It's true. Look up his last posts.
>
> In ZFC or CBL?
I've never seen any hint that CBL has a definition of cardinality.
> Is this a trick question?
I wouldn't have thought so, no.
--
Jesse F. Hughes
"You do know that after the get done with [outlawing] cigarettes,
they're gonna come after guns, right?"
-- AM talk radio host Mike Gallagher
Chris Menzel
<shyma...@gmail.com> said:
> On Mar 12, 11:36 pm, Chris Menzel <cmen...@remove-this.tamu.edu>
> wrote:
>> On Wed, 12 Mar 2008 19:55:01 -0700 (PDT), Charlie-Boo
>> <shymath...@gmail.com> said:
>>
>> > ...
>> > Wffs refer to relations (sets.) Can they refer to non-sets there?
>> > Wffs contain operations on relations. Can those operations be done on
>> > nonrelations?
>>
>> > The problem was they figured every wff defined a set based on the wff
>> > being true when a value is substituted for a free variable. Then they
>> > thought of {x|~(x e x)} and there was a wff that was not a set. So
>> > they said, ok, a wff is not always a set.
>>
>> My god. What must it be like to be so profoundly muddle-headed? I
>> really do feel badly for you.
>>
>> > But there are only aleph-1 wffs
>>
>> Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
>>
>> > and aleph-2 sets of numbers alone,
>
> I give a cardinality of aleph-0 to finite sets,
So, in your mouth, "aleph-0" means "finite". Bizarre. It would make
just about as much sense to use, say, "seventeen" for that purpose.
"aleph-0" has a fixed and longstanding meaning in mathematics and it is
perverse, or clueless, in the extreme to decide to use it to mean
something entirely different.
> but whatever numbers you want is fine with me -
What numbers I want has nothing to do with it. The issue is your use of
"aleph-0" to mean something other than its universally accepted meaning
in modern mathematics.
>> > so there are plent more sets than wffs and we can say that there is in
>> > fact a set for every wff. It is counter-intuitive to say sets do not
>> > include what all wffs define.
>>
>> > In any case, they set out to define what any set can define, when the
>> > real problem was they needed to be exact about terms such as wff.
>>
>> > If you first decide if a wff can make a reference to something that
>> > is not a set, then if yes, then naturally these wffs are not sets,
>> > and if no, then the {x|~(x e x)} example is NOT a set and we still
>> > have each wff defining a set. So we don't really need to worry
>> > about what's in a set as we do in ZF. We just need to be careful
>> > about the formal system - what is the real syntax of a wff? Can it
>> > contain references to nonsets?
>>
>> The depth of your confusion is truly great. In this light your
>> profound ignorance of the history and content of set theory is more
>> understandable. I will read your posts with more compassion in the
>> future.
>
> You haven't answered the question either (the source of the problem
> with the Russell Paradox.)
The generally acknowledged source is implicit in ZF -- though you would
have to understand elementary ZF to appreciate the point. The source --
in the sense of the principle most central to its derivation -- is the
unrestricted principle of comprehension: That, for any formula "F(x)" in
the language of set theory with "x" free there is a set y such that, for
all x, x in y iff F(x). This principle was replaced by the schema of
separation, which does not permit one to prove the existence of sets ex
nihilo.
> A wff can reference relations (sets) e.g. (all x)P(x) refers to
> relation P.
What are you talking about? Let, e.g., P be "x=0", i.e., "x is the
empty set". So you are saying that "(all x)x=0" refers to the relation
"x is the empty set", i.e., the set {0}? It doesn't *refer* to anything
at all; it is simply the false statement that everything is identical to
the empty set.
> May a wff contain a reference to something instead of the relation and
> use a non-relation there? If f(some relation) is a wff then is
> f(something not a relation) necessarily a wff as well?
Your question is ill-formed as stated. It is allegedly a question about
set theory. So formulate your question in the language of set theory.
Can you even do that?
(FWIW, on the simplest way of cashing out your question, the answer is
trivially "yes" in ZF. Let s1 be a relation (i.e., a set of n-tuples,
for some n>0). Let s2 be a set that is not a relation. Then, if f is a
wff with a free variable x, then "f(s1)" and "f(s2)" are obviously both
wffs, where they are the result of substituting "s1" and "s2" for "x" in
f, respectively. Somehow I don't think this is what you have in mind.)
> When we see in a wff (all x) ... must the ... be a reference to a
> relation e.g. P(x) above or can wffs contain a non-relation for the
> ... ?
More incoherent gibberish. When we see a wff "(all x)...", the "..." is
obviously itself a wff -- this is just a trivial fact about formal
languages. Wffs don't ever "contain" relations or non-relations, they
are syntactic entities that contain other pieces of syntax. Some of
those pieces of syntax might themselves indicate relations in the
intended semantics of the language. You appear to be badly confusing
syntax generally with semantics; or something.
> The fact of the matter is, naive set theory is right,
If by naive set theory you mean the theory consisting of the axiom of
extensionality and every instance of the principle of of comprehension,
that theory is provably inconsistent. Though it does appear that you
have trouble distinguishing "inconsistent" from "right", so your claim
is understandable.
> they were just confused as to how to define wffs after it was
> discovered that there were things that are not sets. You are not
> showing any better ability to grapple with the question, even with a
> guide.
Mmm hmm. Zermelo, von Neumann, Gödel, et al were confused. And you're
not. You *might* want to rethink that.
> If (all x)_(x) is a wff for something in place of the _ could that
> something be other than a relation?
Really, for your own good, go educate yourself.
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 13, 3:43 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > On Mar 13, 2:53 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
> >> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> >> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
> >> >> > you want is fine with me - like whether Peano starts with 0 or 1.
>
> >> >> So all finite sets have the same cardinality, namely aleph-0?
>
> >> > On the infinity scale viz. finite.
>
> >> > It all has to do with loops in computer programs, you know - how many
> >> > loops it takes to process the finite subset of the world that man will
> >> > ever see.
>
> >> I asked a yes/no question.
>
> > I gave an implicit yes.
>
> If you say so. Okay, so every finite set has the same cardinality.
> Well, that *is* revolutionary.
No, I said with respect to the infinity scale. There is no point to
any of this, you do realize that don't you?
> >> Maybe you're not so good with yes/no. I'll try true/false:
>
> >> T/F Every finite set has the same cardinality.
>
> > Are you saying that this is a request directly from Torkel/Franzen?
> > Did you know that he spent his last days of this level of abstraction
> > working in CBL? It's true. Look up his last posts.
>
> > In ZFC or CBL?
>
> I've never seen any hint that CBL has a definition of cardinality.
I thought you just quoted it.
"sigh"
C-B
> > Is this a trick question?
>
> I wouldn't have thought so, no.
>
> --
> Jesse F. Hughes
> "You do know that after the get done with [outlawing] cigarettes,
> they're gonna come after guns, right?"
> -- AM talk radio host Mike Gallagher- Hide quoted text -
Charlie-Boo
> On Thu, 13 Mar 2008 10:44:50 -0700 (PDT), Charlie-Boo
> <shymath...@gmail.com> said:
>
>
>
>
>
> > On Mar 12, 11:36 pm, Chris Menzel <cmen...@remove-this.tamu.edu>
> > wrote:
> >> On Wed, 12 Mar 2008 19:55:01 -0700 (PDT), Charlie-Boo
> >> <shymath...@gmail.com> said:
>
> >> > ...
> >> > Wffs refer to relations (sets.) Can they refer to non-sets there?
> >> > Wffs contain operations on relations. Can those operations be done on
> >> > nonrelations?
>
> >> > The problem was they figured every wff defined a set based on the wff
> >> > being true when a value is substituted for a free variable. Then they
> >> > thought of {x|~(x e x)} and there was a wff that was not a set. So
> >> > they said, ok, a wff is not always a set.
>
> >> My god. What must it be like to be so profoundly muddle-headed? I
> >> really do feel badly for you.
>
> >> > But there are only aleph-1 wffs
>
> >> Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
>
> >> > and aleph-2 sets of numbers alone,
>
> > I give a cardinality of aleph-0 to finite sets,
>
> So, in your mouth, "aleph-0" means "finite".
This is all stupid shit. I just said that when you are examining
issues regarding infinite sets, there are situations where all finite
sets are treated the same. We never went into any detail about what I
was talking about and you waste time trying to compare it to the
cardinality of finite sets, which has no place in what I was talking
about.
Work on showing specific results rather than a feeble attempt at
character assassination.
C-B
> Really, for your own good, go educate yourself.- Hide quoted text -
>
> - Show quoted text -- Hide quoted text -
Charlie-Boo
This is all pretty simple and if you'd put your weapons down for a
second, you can see the point,
So you answer that a wff can contain a reference to a non-relation?
Then (all x)P(x) is a wff even if P is not a relation?
If we assume that, then naturally a wff does not necessarily define a
set since it can refer to non-sets. If a wff doesn't refer to non-
sets, then the wff defines a set. There's no paradox or
contradiction.
> > When we see in a wff (all x) ... must the ... be a reference to a
> > relation e.g. P(x) above or can wffs contain a non-relation for the
> > ... ?
>
> More incoherent gibberish. When we see a wff "(all x)...", the "..." is
> obviously itself a wff -- this is just a trivial fact about formal
> languages. Wffs don't ever "contain" relations or non-relations, they
> are syntactic entities that contain other pieces of syntax. Some of
> those pieces of syntax might themselves indicate relations in the
> intended semantics of the language. You appear to be badly confusing
> syntax generally with semantics; or something.
>
> > The fact of the matter is, naive set theory is right,
>
> If by naive set theory you mean the theory consisting of the axiom of
> extensionality and every instance of the principle of of comprehension,
> that theory is provably inconsistent. Though it does appear that you
> have trouble distinguishing "inconsistent" from "right", so your claim
> is understandable.
>
> > they were just confused as to how to define wffs after it was
> > discovered that there were things that are not sets. You are not
> > showing any better ability to grapple with the question, even with a
> > guide.
>
> Mmm hmm. Zermelo, von Neumann, Gödel, et al were confused. And you're
> not. You *might* want to rethink that.
I am addressing the quesion of WHICH wffs define sets. To say that a
wff is not a set is throwing the baby out with the bathwater. We can
do better by telling which wffs are sets and which are not.
Where did Zermelo, von Neumann, Gödel, et al address that?
C-B
> > If (all x)_(x) is a wff for something in place of the _ could that
> > something be other than a relation?
>
> Really, for your own good, go educate yourself.- Hide quoted text -
>
> - Show quoted text -- Hide quoted text -
Charlie-Boo
> On Wed, 12 Mar 2008 10:06:55 -0700 (PDT), Charlie-Boo
> <shymath...@gmail.com> said:
>
> > ...
> > ZF does nothing useful.
>
> Well, usefulness is admittedly relative to one's purposes. If you have
> no interest in sets, for example, ZF is of course not very useful to
> you.
>
> > The real intent was to say they fixed the Russell Paradox
>
> Actually, no one ever said that. The original motivation was simply to
> *avoid* RP
Nobody said "fix", they all said "avoid"?
> by blocking the usual routes to its derivation. In addition,
> the intent was to make clear and explicit all of the assumptions needed
> to be able to do all of the desired mathematics. Mathematicians since
> Euclid have thought this sort of thing was a pretty good idea. Don't
> you agree?
That they said it or that it's a good idea? You're talking about
formalizing, which is exactly what CBL does.
> As research in ZF progressed, a clear picture of the
> structure of the set theoretic universe began to emerge more clearly.
Clear pictures oughta be clear, I always say.
And I always thought that they added one set of axioms on top of
another, never could figure out which one is right, and now they say
that you can assume whatever (axioms) you want - whatever helps you
conclude what you wanted to conclude in the first place.
I also thought that clear meant, "Ok, here's the answer, we all agree,
and we've got it all figured out." I didn't know it included a dozen
conflicting answers.
> With this, ZF began to be viewed less pragmatically than it had
> originally and more as the principles describing a particular
> well-defined mathematical structure (or perhaps more accurately, a class
> of them), just as the axioms of PA describe the natural number
> structure.
Actually, they assure that the relations TRUE, ADD and MULTIPLY are
representable (speaking of being formal.) Requiring systems to
contain the Peano axioms is stupid, when they are equivalent to this
simple fact. It is simpler and more general to talk in terms of what
is representable, without requiring a particular set of axioms. Other
axioms can achieve the same result. The definition should be at the
higher level of abstraction that includes all such axiomatizations.
This is an instance of a principle that I noticed in the formalization
of programming languages. They wanted to define the passing of input
from one program to another in terms of low level data structures used
in an existing popular implementation. I argued that the definition
should be at a higher level based on the functionality provided by
these data structures. This would allow implementors to implement the
best design, and not have to change their implementation when it
provides the intended functionality. The same principle is in play
here.
> You should perhaps actually *learn* something about the
> history of set theory rather than pulling myths out of your ass.
>
> > because it is all formal, but what they have is no solution as it
> > doesn't provide the facilities needed in an axiomatization: to be able
> > to decide questions about Set Theory.
>
> That's a bizarre claim (whatever it's supposed to mean).
How do yoi know it's bizarre if you don't know what it means? I'm
talking about big unanswered questions of set theory (e.g. the
Continuum Hypothesis) being independent of the ZF axioms.
> All that is
> needed in an axiomatization are some axioms. Of course, there are lots
> of adequacy conditions we might impose relative to the purpose of the
> axiomatization. The original conditions on ZF were (i) to block the
> usual derivations of the paradoxes and (ii) to preserve all of the
> useful mathematics that set theory had enabled. By those criteria it
> was a resounding success.
Then why were two dozen alternatives proposed? (If you really know
the history and research behind ZF, then you know the answer to that.)
> > (CBL decides numerous questions about all sorts of branches of CS.)
>
> That is really doubtful. I doubt whether you have even formulated a
> rigorous definition of what it is for CBL to decide a question.
I've given axioms and proofs, the resulting theorems have never been
challenged, and nobody was ever able to show a simpler proof than at
least one of the proofs generated (for Rosser 1936.)
Reality Check:
Who in this whole world has ever actually shown a new proof formally
generated, especially one shown to be superior to what has been done
by hand?
> > What new facts has ZF shown us?
>
> Oh, I was under the impression you at least knew a little set theory.
> My mistake. How about that every singular limit ordinal k with
> cofinality < card(k) lacks the Souslin property? Or maybe the Stone
> Representation theorem (every Boolean Algebra is isomorphic to a field
> of sets)? The fact that every normal function on the ordinals has
> arbitrarily large fixed points?
Ok, prove any of that using just the ZF axioms.
> > Rememeber, that's ZF, the 8 or 10 axioms.
>
> (First-order) ZF has infinitely many axioms. You don't know this?
Playing games with syntax ("avoided" not "fixed", now how you count
the "axioms") is not productive.
> > (The real source of the problem is that they are inconsistent about
> > what a wff can contain.
>
> Who are "they"?
The descriptions of the problems caused by Russell's Paradox.
> > "Can a wff contain a reference to something that is not a set?"
>
> In ZF, the answer to this is trivially "no".
You said yes elsewhere. (I can run with either.)
> > The Russell Paradox occurs because they are inconsistent on this
> > question.
>
> You really have absolutely no idea what you're talking about.
What is the analogy to the Russell Paradox in Logic? In the Theory of
Computation? In English?
> > Pick an answer (yes or no) and there is no Paradox if you keep that
> > answer in mind. They never thought of it because they didn't even
> > know there was such a thing as a non-set. In fact, some still say to
> > this day that "Everything is a set."!!
>
> And in the context of pure ZF, that is trivially true. It is of course
> not true in other theories like VNBG or KPU.
Is {x|~(x e x)} a set?
> > {x| ~(x e x)} is not.
>
> Indeed. And in ZF you can't refer to it.
Can you refer to {x|x>3}? Why the difference?
> > This is common in "Paradoxes" e.g. Unexpected Exam/Hanging and God
> > Paradox are the same. "Can we expect more than once?" is not
> > addressed and is inconsistently implied and refuted by the logic used.
> > This is all shown clearly by CBL, which is why I am able to post so
> > many proofs of theorems of Godel/Rosser/Turing et. al. One proof
> > generated by CBL was called the shortest one for Godel-1 by an author
> > of a book on Godel's Theorems, and I immediately provided a shorter
> > one - so that must be unpublished so far (outside of Google
> > Groups.)
>
> Name of the "author" and a reference to your historic proof might make
> your claim a bit more credible.
Peter Smith - earlier post.
C-B
Charlie-Boo
>
> > ZF does nothing useful.
>
> At the very least it provides an axiomatization for a vast amount of
> mathematics. If that is not useful to you personally, then so be it.
The Peano Axioms prove statements about arithmetic. (Actually, CBL
can be used to show general forms of what can be proven. Any true
statement of the form x+y=z is provable because addition is
representable (r.e.) CBL can be used to show other wffs are r.e. with
a similar conclusion.)
The additional 8 or 10 ZF set axioms prove dinky statements about sets
that were already known.
What significant theorem can you prove using the 8 or 10 ZF axioms?
I mean that weren't already proven by hand.
C-B
Charlie-Boo
> On Mar 10, 2:16 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On Mar 10, 3:58 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > On Mar 10, 12:11 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > wrote:
> > > > > Be a sport,
>
> > > > When have I not? (Unsubstantiated innuendo?)
>
> > > (1) No, he didn't insinuate that you're not a sport.
>
> > would be amazed at the results (that other people get) if you applied
> > a little bit of intelligence to a probelm rather than flying off the
> > handle all the time and attacking people's character.
>
> I don't "all the time" attack people's character. In a few certain
> cases, I do comment on what I find to be the poor character of some
> people in their role of posting.
You said that insuation was free and guiltless, so I thought that I'd
have some. So, did you ever find a school to accept you?
> > > (2) But the
> > > answer to your question includes such instances as never getting back
> > > to me as to the purpose of your question about set theory that I
> > > answered in full (our very first discussion),
>
> > Oh No!! : ( MoeBlee mon ami, my budski - plz copy or link.
>
> I've asked you about it for about two years since and NOW you ask me
> for a link. I've given you refs to it already; I'm not going to again
> try to track down where it was. It was in a thread in which you asked
> for a formulation of the language of set theory. I gave you such a
> formulation, but you would never answer as to what was the point of
> that.
>
> > It's called "discovery", where you smoke out each other instead of
> > fighting battles. Like playing a game of chess rather than waging a
> > war. Sometimes they stand up and get shot at just to see the size and
> > direction of the enemy's line of fire.
>
> More evidence that you're a putz.
But not proof. More like the Raven Paradox than the Russell Paradox.
> > > and not recognizing the
> > > examples given to you of theorems of mathematics proven by ZFC.
>
> > Oh, like 1+1=2?
>
> That's one, but not one that I mentioned. I mentioned a theorem in
> topology (I could have mentioned hundreds, but I cited one just at
> will). I mentioned the Bolzano-Weierstrass theorem (I could have
> mentioned hundreds in analysis, but I cited one just at will).
You can prove it using just the ZF axioms? Where is that? Does it
just use Peano's Axioms, or does it actually need the 8 to 10 axioms
particular to ZF?
> > Can you prove the Pythagorean theorem in ZFC?
>
> I'm working on a formulation of basic geometry as defined to be a
> structure in Z set theory. Several theorems about lines, planes,
> angles, and triangles are easy to prove right away. As I progress with
> the work, I don't expect that the Pythagorean theorem will be
> difficult to prove in this formulation. I already mentioned that if I
> had a place to post PDF files then I could display the work as it
> progresses.
Put it on my Self Reference Google Group. I'll do it if you can't.
Speaking of which, someone again asked for a copy of the theorem-
generator that I published a few years ago. (I forget who.) I have
posed the article here:
> > > By the way, did you ever figure out how to prove in Z set theory that
> > > if a set and its complement are recursively enumerable then the set is
> > > recursive?
>
> > In Z? (What's Z? There's the integers
> > and sports cars.)
>
> Z SET THEORY [all caps now added], as I said and as you just QUOTED
> me.
>
> > Was I supposed to do that?
>
> You kept saying that you don't know how it could be done
?? In CBL? P(I) , P(x) + ~P(x) ?
> and asked me
> about it. Then I gave you a ref to the Boolos book, which you have.
> You haven't said what in that proof you don't think can be carried out
> in Z set theory.
>
> > It's probably easy in CBL..
>
> Yeah, sure.
Everything else is. Did you know that nobody has been able to
simplify Godel's First Theorem based on w-consistency, but CBL can
formally prove it in about a dozen steps?
C-B
> MoeBlee- Hide quoted text -
Alan Smaill
> On Mar 13, 8:54 am, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 12, 12:11 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> >> Charlie-Boo <shymath...@gmail.com> writes:
>> >> > On Mar 11, 1:07 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
...
>> >> >> where can I find the list of all CBL axioms?
>>
>> >> > Here:
>>
>> >> > 1. Program Synthesis e.g. for PHP programs
>>
>> >> "e.g." doesn't cut it.
>>
>> > Please read the rest and comprehend. There are an infinite number of
>> > programming languages. I show the axioms for one enough to synthesize
>> > a useful program nobody else has ever synthesized, the test for being
>> > a factor.
>>
>> That's just it ... I ask for the list of *all* axioms, and
>> you reply with examples.
>
> There are an infinite number of programming languages. For the ones
> used as output to your Program Synthesis system, you give axioms for
> the constructs in that language. Most languages are terribly
> redundant - theoretically all they need is constants, if, addition,
> loops. But there are bigger constructs such as multiplication and it
> makes better programs if it can use that as well, so we need to
> include enough to cover the domain we are in.
And if you end up with a system that can't prove associativity of
multiplication, you chuck in an extra axiom, etc etc etc.
This just shows the flexibility of CBL, of course.
> Some BSers go so far as to say, "We produce XYZ wffs and of course we
> can easily translate them into computer programs." and never do. But
> they are not even showing that they are in fact faithfully
> representing the wffs and that they are in fact able to solve the
> problem of creating computer programs from that.
As you have been told before, you can get hold of systems that do
exactly what you claim does not happen; but you prefer a well-defended
ignorance.
>> You yourself don't even know what the axioms are in an area you claim
>> CBL is a world beater.
>
> See above. I can't list all infinity (aleph-whatever) Programming
> Languages.
The question at issue was about basic recursion theory, not
programming languages.
>> > People who write about a Program Synthesis system without reference to
>> > the programming language are already BSing you. The axioms depend on
>> > the language.
>>
>> Of course they do;
>> but those devious academics nevertheless gove a *complete* axiomatisation
>> of the systems they are working in.
>
> As far as Program Synthesis goes, they don't give anything at all -
> example programs, the formal program spec, how the program is
> created. They show a bunch of their buzzwords and junk, and there is
> no standard in use as to how they can be held accountable.
simply wrong --
but by all means cherish these beliefs if it makes you feel better.
--
Alan Smaill
Jesse F. Hughes
> On Mar 13, 5:08 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 13, 3:43 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> >> Charlie-Boo <shymath...@gmail.com> writes:
>> >> > On Mar 13, 2:53 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> >> >> Charlie-Boo <shymath...@gmail.com> writes:
>> >> >> > I give a cardinality of aleph-0 to finite sets, but whatever numbers
>> >> >> > you want is fine with me - like whether Peano starts with 0 or 1.
>>
>> >> >> So all finite sets have the same cardinality, namely aleph-0?
>>
>> >> > On the infinity scale viz. finite.
>>
>> >> > It all has to do with loops in computer programs, you know - how many
>> >> > loops it takes to process the finite subset of the world that man will
>> >> > ever see.
>>
>> >> I asked a yes/no question.
>>
>> > I gave an implicit yes.
>>
>> If you say so. Okay, so every finite set has the same cardinality.
>> Well, that *is* revolutionary.
>
> No, I said with respect to the infinity scale. There is no point to
> any of this, you do realize that don't you?
I don't know what that means, but I do know that you said that you
said "yes" to my question. My question was:
[Do] all finite sets have the same cardinality, namely aleph-0?
A "yes" to this seems to justify the following conclusion:
Every finite set has the same cardinality.
And now you say that this conclusion is wrong. Did you want to
retract the earlier "yes"?
>> I've never seen any hint that CBL has a definition of cardinality.
>
> I thought you just quoted it.
I quoted no definition at all. I asked a simple question, the
affirmation of which would not serve as a definition of cardinality.
At best, it may serve as a definition of aleph-0.
You *do* know what a definition is, right? Here, I'll get you
started:
Let X and Y be sets. We say that X and Y have the same
/cardinality/ just in case ...
(Hint: don't answer "yes" to this one. It's fill-in-the-blank.)
--
"[In the movie, Tom Green] delivers a child, severs the umbilicus with
his teeth and then swings the baby over his head before tenderly
handing it to the stunned, blood-spattered mother[...] This was, I
have to say, a bit much." -- New York Times movie reviewer A. O. Scott
Chris Menzel
<shyma...@gmail.com> said:
>> ...
>>>>> But there are only aleph-1 wffs
>>>>
>>>> Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
>>>>
>>>>> and aleph-2 sets of numbers alone,
>>>
>>> I give a cardinality of aleph-0 to finite sets,
>>
>> So, in your mouth, "aleph-0" means "finite".
>
> This is all stupid shit.
I confess I don't see why. I simply pointed out that you are using the
names of the infinite cardinals completely incorrectly. How do you
expect to communicate your ideas to others if you are using words that
have universally understood meanings to mean something else entirely?
> I just said that when you are examining issues regarding infinite
> sets, there are situations where all finite sets are treated the same.
A perfectly reasonable point. My point was simply that the word you
were using to make your point was the wrong one. You used "aleph-0" as
a synonym for "finite". Since aleph-0 is the first infinite cardinal,
it will surely hinder your ability to make points like the one above if
you continue to use it incorrectly. You're welcome.
> We never went into any detail about what I was talking about
I went into great detail in the remainder of the post. You even
included it in this reply, but you didn't respond to it. I give you
another chance below.
> and you waste time trying to compare it to the cardinality of finite
> sets,
That's certainly an odd take on what I was doing. (I'm not even sure
what that take is, frankly.)
> which has no place in what I was talking about.
I myself find it important that my interlocutors and I agree on the
meanings of the words we use. Don't you?
> Work on showing specific results rather than a feeble attempt at
> character assassination.
Ah, so in addition to "aleph-0" = "finite", we also have "pointing out
mistakes" = "character assassination". I'll try to bear that in mind.
Meanwhile, the remainder of the post addressed several specific issues
you'd raised in connection with Russell's paradox. You are hostage to a
number of serious confusions that I have tried to sort out for you. You
might want to give it a read. I've edited so as to leave only
substantive discussion.
-cm
*****
...
Charlie-Boo
CBL was designed to prove metamathematical statements about truth,
provability and related concepts. As far as applying CBL to simple
mathematical facts, I have recently considered that as it may in fact
enhance the metamathematical proofs.
If P expresses a representable set then P(a) <=> |-P(a) ? I may be
able to prove associativity of addition simply by showing that a
particular relation is representable and adding this new,
"Mathematical" rule to CBL:
P(x) <=> P(a) , |- P(a)
Wff P represents an r.e relation <=> P is true iff P is provable.
Sometimes I post questions to verify my using traditional principles
in CBL proofs, and I usually get a wrong answer with the addendum that
it is a "trivial" problem.
But if you would like to start a thread with that as the challenge
then I will accept that as an official challenge. I forget what
happened when that was discussed before. But CBL of course continues
to become more and more powerful (as evidenced by my posts.) You can
list (or request) the whole set of challenges and their status: There
is a UTM (easy). Addition is Associative (may be straightforward -
have to use methods of Math not Metamath). P(I) , P(x) + P(x) (May
need a general axiom or rule there. It is a common technique - an
instance of dovetailing.)
> This just shows the flexibility of CBL, of course.
>
> > Some BSers go so far as to say, "We produce XYZ wffs and of course we
> > can easily translate them into computer programs." and never do. But
> > they are not even showing that they are in fact faithfully
> > representing the wffs and that they are in fact able to solve the
> > problem of creating computer programs from that.
>
> As you have been told before, you can get hold of systems that do
> exactly what you claim does not happen; but you prefer a well-defended
> ignorance.
They just don't have any examples.
> >> You yourself don't even know what the axioms are in an area you claim
> >> CBL is a world beater.
>
> > See above. I can't list all infinity (aleph-whatever) Programming
> > Languages.
>
> The question at issue was about basic recursion theory, not
> programming languages.
That's so cute.
If you can't relate to the fact that each programming language has its
own set of axioms (in the same format - could abstract it to a higher
level pretty easily, I think) and since there is an infinite number of
programming languages, I can only list some of them, then we have a
serious communication problem here.
> >> > People who write about a Program Synthesis system without reference to
> >> > the programming language are already BSing you. The axioms depend on
> >> > the language.
>
> >> Of course they do;
> >> but those devious academics nevertheless gove a *complete* axiomatisation
> >> of the systems they are working in.
What are the axioms of program synthesis? (Answer: ARXIV 2000 paper.)
> > As far as Program Synthesis goes, they don't give anything at all -
> > example programs, the formal program spec, how the program is
> > created. They show a bunch of their buzzwords and junk, and there is
> > no standard in use as to how they can be held accountable.
>
> simply wrong --
> but by all means cherish these beliefs if it makes you feel better.
Show the simplest self-contained formal derivation of a computer
program.
Thm. ~LT(I,J)* Is one number not less than another? (Generate a
program to decide the not less than relation)
1. "I<J" # LT(I,J)* Axiom: Program "I<J" decides the less than
relation.
2. M # P(I)* => not(M) # ~P(I)* The complement of a recursive
relation is recursive.
3. not("I<J") # ~LT(I,J)* Not applied to program "I<J" decides the
not less than relation.
4. ~LT(I,J)* w , M # w A relation is recursive/r.e./etc. iff there
is a program to decide/enumerate/etc. it.
qed
This proves the program exists. The fact that not(I), function not is
recursive, means we can write a program to carry out the program
construction.
C-B
Chris Menzel
<shyma...@gmail.com> said:
>> ...
Once again, my answer is that your question is so ill-formed that one
can only guess at what you mean. Spelled out the only way that I could
think of, the answer was trivial.
> Then (all x)P(x) is a wff even if P is not a relation?
Well, there you go again. You *think* you are asking a question but it
is completely ill-formed. You are badly confusing syntax and semantics.
What does or does not count as a wff is wholly a matter of the grammar
of the language in question. If you have a question about a specific
expression, that is, a specific string of symbols in the language of set
theory, I can tell you in two seconds whether or not it is a wff. In
particular, if P(x) is a wff (containing, presumably, free occurrences
of "x"), then, by the grammar for first order languages, we know
immediately that "(all x)P(x)" is a wff. If P(x) is not a wff, then we
know immediately that "(all x)P(x)" is also not a wff. This is just
elementary formal syntax.
Your question also seems to involve the issue of whether or not, for a
given wff P(x) containing free occurrences of "x", there is a set of
things of which P(x) is true. That, of course, is settled by the axioms
of ZF. But your question as it stands is just gibberish. Really, the
best thing you could do for yourself is study basic mathematical logic
and set theory.
> If we assume that, then naturally a wff does not necessarily define a
> set since it can refer to non-sets. If a wff doesn't refer to non-
> sets, then the wff defines a set. There's no paradox or
> contradiction.
If you were actually to study set theory, you would see very early on
why your assertion here is just a confused mess.
>> > When we see in a wff (all x) ... must the ... be a reference to a
>> > relation e.g. P(x) above or can wffs contain a non-relation for the
>> > ... ?
>>
>> More incoherent gibberish. When we see a wff "(all x)...", the "..." is
>> obviously itself a wff -- this is just a trivial fact about formal
>> languages. Wffs don't ever "contain" relations or non-relations, they
>> are syntactic entities that contain other pieces of syntax. Some of
>> those pieces of syntax might themselves indicate relations in the
>> intended semantics of the language. You appear to be badly confusing
>> syntax generally with semantics; or something.
>>
>> > The fact of the matter is, naive set theory is right,
>>
>> If by naive set theory you mean the theory consisting of the axiom of
>> extensionality and every instance of the principle of of comprehension,
>> that theory is provably inconsistent. Though it does appear that you
>> have trouble distinguishing "inconsistent" from "right", so your claim
>> is understandable.
>>
>> > they were just confused as to how to define wffs after it was
>> > discovered that there were things that are not sets. You are not
>> > showing any better ability to grapple with the question, even with a
>> > guide.
>>
>> Mmm hmm. Zermelo, von Neumann, Gödel, et al were confused. And you're
>> not. You *might* want to rethink that.
>
> I am addressing the quesion of WHICH wffs define sets.
That is pretty much exactly the question addressed by ZF. The problem
with naive set theory answered that question too permissively. ZF found
a reasonable way to answer it more carefully while preserving the
useful, legitimate mathematics that had been done with the naive theory.
> To say that a wff is not a set is throwing the baby out with the
> bathwater.
Well, no wff *is* a set (at least, not in the way you mean it). Do you
mean: "To deny that every wff defines a set is to throw the baby out
with the bathwater"? That's a clear assertion. It is also wrong. To
affirm that every wff (with a free variable) defines a set leads to
inconsistency. Inconsistency is the bathwater. The baby is the useful
mathematics that can be done in, or with the aid of, set theory. ZF
does a remarkably good job of tossing out the bathwater and hanging on
to the baby. Again, if you'd commit six months to actually learning the
basics, you could discover this for yourself.
> We can do better by telling which wffs are sets and which are not.
Again, if you mean "by telling which wffs define sets and which do not",
that (among other things) is pretty much exactly what axiomatic set
theory does for you.
> Where did Zermelo, von Neumann, Gödel, et al address that?
In ZF set theory and VonNeumann/Gödel/Bernays set theory, of course.
Charlie-Boo
You left out "in CBL". This is absolutely pointless. It has nothing
to do with Cantor's use of the term "aleph". You can say that finite
sets have their own individual cardinalities if you want (number of
elements), but I have found it easier if you treat the finite sets as
one class, the r.e. sets as the second, the reals/subsets as the 3rd.,
etc.
> >> I've never seen any hint that CBL has a definition of cardinality.
>
> > I thought you just quoted it.
>
> I quoted no definition at all. I asked a simple question, the
> affirmation of which would not serve as a definition of cardinality.
> At best, it may serve as a definition of aleph-0.
Take it at its best.
> You *do* know what a definition is, right? Here, I'll get you
> started:
>
> Let X and Y be sets. We say that X and Y have the same
> /cardinality/ just in case ...
In CBL or what?
> (Hint: don't answer "yes" to this one. It's fill-in-the-blank.)
"someone is just trying to make someone else look dumb" ?
C-B
> --
> "[In the movie, Tom Green] delivers a child, severs the umbilicus with
> his teeth and then swings the baby over his head before tenderly
> handing it to the stunned, blood-spattered mother[...] This was, I
> have to say, a bit much." -- New York Times movie reviewer A. O. Scott- Hide quoted text -
Alan Smaill
great, eh -- a new rule.
truly CBL is a never-ending mystery.
Why not crank the handle and find out if CBL proves associativity
when you add the rule? After all, that's its great advantage, isn't
it -- automatic generation of proofs?
Yet you can't tell us whether your new enhanced version can prove
one of the most basic facts about addition.
--
Alan Smaill
Charlie-Boo
wrote:
> On Fri, 14 Mar 2008 02:16:50 -0700 (PDT), Charlie-Boo
> <shymath...@gmail.com> said:
>
> >> ...
> >>>>> But there are only aleph-1 wffs
>
> >>>> Goodness me. (aleph_1 is uncountable. You probably mean aleph_0.)
>
> >>>>> and aleph-2 sets of numbers alone,
>
> >>> I give a cardinality of aleph-0 to finite sets,
>
> >> So, in your mouth, "aleph-0" means "finite".
>
> > This is all stupid shit.
>
> I confess I don't see why.
What is the value in spending precious bandwidth debating something as
nebulous and arbitrary as what is the most common use of terminology?
It was only a passing reference to the notion of cardinality and was
not part of any theorem or proof.
There is no practical nor theoretical gain to this.
> I simply pointed out that you are using the
> names of the infinite cardinals completely incorrectly. How do you
> expect to communicate your ideas to others if you are using words that
> have universally understood meanings to mean something else entirely?
>
> > I just said that when you are examining issues regarding infinite
> > sets, there are situations where all finite sets are treated the same.
>
> A perfectly reasonable point. My point was simply that the word you
> were using to make your point was the wrong one. You used "aleph-0" as
> a synonym for "finite". Since aleph-0 is the first infinite cardinal,
> it will surely hinder your ability to make points like the one above if
> you continue to use it incorrectly. You're welcome.
It was a passing remark - scratch it.
> > We never went into any detail about what I was talking about
>
> I went into great detail in the remainder of the post. You even
> included it in this reply, but you didn't respond to it. I give you
> another chance below.
>
> > and you waste time trying to compare it to the cardinality of finite
> > sets,
>
> That's certainly an odd take on what I was doing. (I'm not even sure
> what that take is, frankly.)
>
> > which has no place in what I was talking about.
>
> I myself find it important that my interlocutors and I agree on the
> meanings of the words we use. Don't you?
Yes, agree. And I said you can use it as you wish, which is giving my
side of the agreement.
> > Work on showing specific results rather than a feeble attempt at
> > character assassination.
>
> Ah, so in addition to "aleph-0" = "finite", we also have "pointing out
> mistakes" = "character assassination".
Ok, I was a total idiot to say that the finite sets are or should be
lumped into one category and called "aleph-0" because there is "no"
infinity there, and N is aleph-1 because we use infinity once, and the
reals are aleph-2 because we take a 1-infinity and make it into a 2-
infinity, so nobody should take anything I say seriously because it's
always a good idea to "consider the source".
> I'll try to bear that in mind.
> Meanwhile, the remainder of the post addressed several specific issues
> you'd raised in connection with Russell's paradox. You are hostage to a
> number of serious confusions that I have tried to sort out for you. You
> might want to give it a read. I've edited so as to leave only
> substantive discussion.
>
> -cm
>
> *****
>
> ...
>
> > You haven't answered the question either (the source of the problem
> > with the Russell Paradox.)
>
> The generally acknowledged source is implicit in ZF -- though you
> would have to understand elementary ZF to appreciate the point. The
> source -- in the sense of the principle most central to its
> derivation -- is the unrestricted principle of comprehension: That,
> for any formula "F(x)"
And so I asked if a formula can contain a reference to non-relations,
you said "yes", and so the answer to Russell is that any wff that
starts with a non-relation is liable to end up with one, and if we
start with only relations, then we end up with one. So the question
becomes, which wffs define sets.
> in the language of set theory with "x" free
> there is a set y such that, for all x, x in y iff F(x). This
> principle was replaced by the schema of separation, which does not
> permit one to prove the existence of sets ex nihilo.
In CBL it's:
P/TW => P/SE If P is expressible, then P defines a set.
> > A wff can reference relations (sets) e.g. (all x)P(x) refers to
> > relation P.
>
> What are you talking about? Let, e.g., P be "x=0", i.e., "x is the
> empty set". So you are saying that "(all x)x=0" refers to the
> relation "x is the empty set",
Yikes. No, the relation is x=0.
> i.e., the set {0}? It doesn't *refer*
> to anything at all;
Is it a good idea to take a word that is vaguely defined and make a
definitive statement about it? I mean, words like "fix", "avoid",
"refer"?
> it is simply the false statement that everything
> is identical to the empty set.
>
> > May a wff contain a reference to something instead of the relation
> > and use a non-relation there? If f(some relation) is a wff then is
> > f(something not a relation) necessarily a wff as well?
>
> Your question is ill-formed as stated. It is allegedly a question
> about set theory. So formulate your question in the language of set
> theory. Can you even do that?
Well, it's about the system's syntax and semantics, actually.
> (FWIW, on the simplest way of cashing out your question, the answer is
> trivially "yes" in ZF. Let s1 be a relation (i.e., a set of n-tuples,
> for some n>0). Let s2 be a set that is not a relation. Then, if f is a
> wff with a free variable x, then "f(s1)" and "f(s2)" are obviously both
> wffs, where they are the result of substituting "s1" and "s2" for "x" in
> f, respectively. Somehow I don't think this is what you have in mind.)
>
> > When we see in a wff (all x) ... must the ... be a reference to a
> > relation e.g. P(x) above or can wffs contain a non-relation for the
> > ... ?
>
> More incoherent gibberish. When we see a wff "(all x)...", the "..." is
> obviously itself a wff -- this is just a trivial fact about formal
> languages.
Given the definition, which I asked for, and you eventually said yes,
a wff can refer to a non-relation.
> Wffs don't ever "contain" relations or non-relations,
So they don't contain anything, sort of like {} ?
> they
> are syntactic entities that contain other pieces of syntax. Some of
> those pieces of syntax might themselves indicate relations in the
> intended semantics of the language. You appear to be badly confusing
> syntax generally with semantics; or something.
>
> > The fact of the matter is, naive set theory is right,
>
> If by naive set theory you mean the theory consisting of the axiom of
> extensionality and every instance of the principle of of comprehension,
> that theory is provably inconsistent. Though it does appear that you
> have trouble distinguishing "inconsistent" from "right", so your claim
> is understandable.
We can show which wffs define sets (e.g. using CBL) instead of denying
the ability to say that a given wff defines a set.
> > they were just confused as to how to define wffs after it was
> > discovered that there were things that are not sets. You are not
> > showing any better ability to grapple with the question, even with a
> > guide.
>
> Mmm hmm. Zermelo, von Neumann, Gödel, et al were confused. And you're
> not. You *might* want to rethink that.
>
> > If (all x)_(x) is a wff for something in place of the _ could that
> > something be other than a relation?
>
> Really, for your own good, go educate yourself.
You didn't say whether these dignitaries had considered the problem of
deciding whether a given wff defines a set or not.
C-B
Charlie-Boo
wrote:
It's a question of definitions, not a problem to claim trivial in your
pointless meager efforts to debase the intellectual capabilities of
those who disagree with you.
> > Then (all x)P(x) is a wff even if P is not a relation?
>
> Well, there you go again. You *think* you are asking a question but it
> is completely ill-formed. You are badly confusing syntax and semantics.
> What does or does not count as a wff is wholly a matter of the grammar
> of the language in question.
But whether it defined a set or not depends on the parts of the wff.
> If you have a question about a specific
> expression, that is, a specific string of symbols in the language of set
> theory, I can tell you in two seconds whether or not it is a wff.
(x e y) v (y e x)
> In
> particular, if P(x) is a wff (containing, presumably, free occurrences
> of "x"), then, by the grammar for first order languages, we know
> immediately that "(all x)P(x)" is a wff. If P(x) is not a wff, then we
> know immediately that "(all x)P(x)" is also not a wff. This is just
> elementary formal syntax.
So you include non-relations.
> Your question also seems to involve the issue of whether or not, for a
> given wff P(x) containing free occurrences of "x", there is a set of
> things of which P(x) is true. That, of course, is settled by the axioms
> of ZF. But your question as it stands is just gibberish. Really, the
> best thing you could do for yourself is study basic mathematical logic
> and set theory.
Study it? I'm trying to fix it. (Sometimes I think the only solution
is to throw it out and replace it with CBL. But I know that users
don't like to have their systems replaced. First they worry the new
system will be hard to learn and use, and at some point they wonder if
the information in the existing system will be available in the new
one.)
> > If we assume that, then naturally a wff does not necessarily define a
> > set since it can refer to non-sets. If a wff doesn't refer to non-
> > sets, then the wff defines a set. There's no paradox or
> > contradiction.
>
> If you were actually to study set theory, you would see very early on
> why your assertion here is just a confused mess.
This isn't Set Theory, it's CBL. Maybe that's your problem.
Ok, does (x e y) v (ye x) define a set?
> > To say that a wff is not a set is throwing the baby out with the
> > bathwater.
>
> Well, no wff *is* a set (at least, not in the way you mean it).
You have now joined the ranks of Bill Clinton by adding to the list
[fix, avoid, refer] the word "is".
"The answer depends on what the meaning of the word "is" is. If it
means is and always has been . . ." - Pres. Clinton to special
prosecutor Ken Star.
"Everthing he said that I said about Rosie O'Donnell is a lie." -
Barbara Walters on Donald Trump on Barbara Walters on Rosie O'Donnell.
> Do you
> mean: "To deny that every wff defines a set is to throw the baby out
> with the bathwater"? That's a clear assertion. It is also wrong. To
> affirm that every wff (with a free variable) defines a set leads to
> inconsistency. Inconsistency is the bathwater. The baby is the useful
> mathematics that can be done in, or with the aid of, set theory. ZF
> does a remarkably good job of tossing out the bathwater and hanging on
> to the baby. Again, if you'd commit six months to actually learning the
> basics, you could discover this for yourself.
>
> > We can do better by telling which wffs are sets and which are not.
>
> Again, if you mean "by telling which wffs define sets and which do not",
> that (among other things) is pretty much exactly what axiomatic set
> theory does for you.
>
> > Where did Zermelo, von Neumann, Gödel, et al address that?
>
> In ZF set theory and VonNeumann/Gödel/Bernays set theory, of course.
What is the procedure to determine if a given wff defines a set?
C-B
Charlie-Boo
CBL proves properties of proving. Now you want to prove properties of
number and relations.
> Why not crank the handle and find out if CBL proves associativity
> when you add the rule? After all, that's its great advantage, isn't
> it -- automatic generation of proofs?
>
> Yet you can't tell us whether your new enhanced version can prove
> one of the most basic facts about addition.
You'll just have to make that an official challenge, I'm afraid
(directions above.)
C-B
> --
> Alan Smaill
Jesse F. Hughes
> On Mar 14, 7:38 am, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>>
>> I don't know what that means, but I do know that you said that you
>> said "yes" to my question. My question was:
>>
>> [Do] all finite sets have the same cardinality, namely aleph-0?
>>
>> A "yes" to this seems to justify the following conclusion:
>>
>> Every finite set has the same cardinality.
>>
>> And now you say that this conclusion is wrong. Did you want to
>> retract the earlier "yes"?
>
> You left out "in CBL". This is absolutely pointless. It has nothing
> to do with Cantor's use of the term "aleph". You can say that finite
> sets have their own individual cardinalities if you want (number of
> elements), but I have found it easier if you treat the finite sets as
> one class, the r.e. sets as the second, the reals/subsets as the 3rd.,
> etc.
But if I add "in CBL" to the sentence, the whole statement appears
meaningless, since I have not seen a definition of cardinality in
CBL.
>> I quoted no definition at all. I asked a simple question, the
>> affirmation of which would not serve as a definition of cardinality.
>> At best, it may serve as a definition of aleph-0.
>
> Take it at its best.
Okay, so at its best, this is what I've got: When Charlie says
"the set X has cardinality aleph-0", he means "the set X is finite",
nothing more nor less. The sentence "X has cardinality aleph-n" is
thus far undefined for every n, as is the term "the cardinality of X"
for arbitrary sets X.
>> You *do* know what a definition is, right? Here, I'll get you
>> started:
>>
>> Let X and Y be sets. We say that X and Y have the same
>> /cardinality/ just in case ...
>
> In CBL or what?
Sure, in CBL is fine. What is the definition of cardinality in CBL?
--
Jesse F. Hughes
"The Cantorians are conducting a campaign of psychological warfare
against humanity."
-- David Petry, on why set theory is evil.
Chris Menzel
<shyma...@gmail.com> said:
> ...You can say that finite sets have their own individual
> cardinalities if you want (number of elements), but I have found it
> easier if you treat the finite sets as one class, the r.e. sets as the
> second, the reals/subsets as the 3rd., etc.
Finite sets are r.e. Does this mean your first class is included in
your second class? Also, where do denumerable non-r.e. sets fit into
your picture? (NB: For mathematicians, "denumerable" = "has cardinality
aleph_0", so you'll need to be careful when you frame your answer, given
that, in your unique idiolect, "aleph_0" = "finite".)
Alan Smaill
> On Mar 14, 2:47 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 14, 7:28 am, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
...
>> >> And if you end up with a system that can't prove associativity of
>> >> multiplication, you chuck in an extra axiom, etc etc etc.
>>
>> > CBL was designed to prove metamathematical statements about truth,
>> > provability and related concepts. As far as applying CBL to simple
>> > mathematical facts, I have recently considered that as it may in fact
>> > enhance the metamathematical proofs.
>>
>> > If P expresses a representable set then P(a) <=> |-P(a) ? I may be
>> > able to prove associativity of addition simply by showing that a
>> > particular relation is representable and adding this new,
>> > "Mathematical" rule to CBL:
>>
>> > P(x) <=> P(a) , |- P(a)
>>
>> great, eh -- a new rule.
>>
>> truly CBL is a never-ending mystery.
>
> CBL proves properties of proving. Now you want to prove properties of
> number and relations.
I want to know what it is, first.
You know, if you're in the business of being precise, why not start
by being precise.
If you're in another business, well, enjoy yourself.
>> Why not crank the handle and find out if CBL proves associativity
>> when you add the rule? After all, that's its great advantage, isn't
>> it -- automatic generation of proofs?
>>
>> Yet you can't tell us whether your new enhanced version can prove
>> one of the most basic facts about addition.
>
> You'll just have to make that an official challenge, I'm afraid
> (directions above.)
It's your pronouncement about your system;
the judgement is easy as soon as you tell us "I may be able to prove".
> C-B
--
Alan Smaill
MoeBlee
> What is the value in spending precious bandwidth debating something as
> nebulous and arbitrary as what is the most common use of terminology?
He's not debating. Rather, he's doing you the favor of informing you.
And it's not just that the terminology is common - it's terminology
that is virtually agreed upon. But the radically personal way you were
using the terminology would pretty much ensure that you'd be
misunderstood by anyone. On the other hand, taking a bit of care to
learn some terminology contribues to communication. Chronic lack, such
as yours, of coherent or recognizable notation and terminology is
indicative of someone who really is not that interested in
communication.
MoeBlee
> C-B- Hide quoted text -
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 14, 7:38 am, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>
> >> I don't know what that means, but I do know that you said that you
> >> said "yes" to my question. My question was:
>
> >> [Do] all finite sets have the same cardinality, namely aleph-0?
>
> >> A "yes" to this seems to justify the following conclusion:
>
> >> Every finite set has the same cardinality.
>
> >> And now you say that this conclusion is wrong. Did you want to
> >> retract the earlier "yes"?
>
> > You left out "in CBL". This is absolutely pointless. It has nothing
> > to do with Cantor's use of the term "aleph". You can say that finite
> > sets have their own individual cardinalities if you want (number of
> > elements), but I have found it easier if you treat the finite sets as
> > one class, the r.e. sets as the second, the reals/subsets as the 3rd.,
> > etc.
>
> But if I add "in CBL" to the sentence, the whole statement appears
> meaningless, since I have not seen a definition of cardinality in
> CBL.
So if you haven't heard of it it must be meaningless? So do I need to
show everything to you to make sure it's meaningful?
> >> I quoted no definition at all. I asked a simple question, the
> >> affirmation of which would not serve as a definition of cardinality.
> >> At best, it may serve as a definition of aleph-0.
>
> > Take it at its best.
>
> Okay, so at its best, this is what I've got: When Charlie says
> "the set X has cardinality aleph-0", he means "the set X is finite",
> nothing more nor less. The sentence "X has cardinality aleph-n" is
> thus far undefined for every n, as is the term "the cardinality of X"
> for arbitrary sets X.
No, read what I said.
> >> You *do* know what a definition is, right? Here, I'll get you
> >> started:
>
> >> Let X and Y be sets. We say that X and Y have the same
> >> /cardinality/ just in case ...
>
> > In CBL or what?
>
> Sure, in CBL is fine. What is the definition of cardinality in CBL?
All this time you didn't even know the fundamentals of the subject you
were discussing. My goodness!
C-B
Charlie-Boo
Is that the best you can some up with?
How about telling us the very best theorem that you have ever
discovered yourself?
C-B
Jesse F. Hughes
> On Mar 14, 3:30 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > On Mar 14, 7:38 am, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>>
>> >> I don't know what that means, but I do know that you said that you
>> >> said "yes" to my question. My question was:
>>
>> >> [Do] all finite sets have the same cardinality, namely aleph-0?
>>
>> >> A "yes" to this seems to justify the following conclusion:
>>
>> >> Every finite set has the same cardinality.
>>
>> >> And now you say that this conclusion is wrong. Did you want to
>> >> retract the earlier "yes"?
>>
>> > You left out "in CBL". This is absolutely pointless. It has nothing
>> > to do with Cantor's use of the term "aleph". You can say that finite
>> > sets have their own individual cardinalities if you want (number of
>> > elements), but I have found it easier if you treat the finite sets as
>> > one class, the r.e. sets as the second, the reals/subsets as the 3rd.,
>> > etc.
>>
>> But if I add "in CBL" to the sentence, the whole statement appears
>> meaningless, since I have not seen a definition of cardinality in
>> CBL.
>
> So if you haven't heard of it it must be meaningless? So do I need to
> show everything to you to make sure it's meaningful?
Meaningless to me, then.
But you can help make the statement meaningful. Tell me your
definition of cardinality.
>> Okay, so at its best, this is what I've got: When Charlie says
>> "the set X has cardinality aleph-0", he means "the set X is finite",
>> nothing more nor less. The sentence "X has cardinality aleph-n" is
>> thus far undefined for every n, as is the term "the cardinality of X"
>> for arbitrary sets X.
>
> No, read what I said.
I haven't seen you offer any definition of cardinality in this thread,
but perhaps I missed it. Could you point it out for me?
>> >> You *do* know what a definition is, right? Here, I'll get you
>> >> started:
>>
>> >> Let X and Y be sets. We say that X and Y have the same
>> >> /cardinality/ just in case ...
>>
>> > In CBL or what?
>>
>> Sure, in CBL is fine. What is the definition of cardinality in CBL?
>
> All this time you didn't even know the fundamentals of the subject you
> were discussing. My goodness!
What an odd response! I was *asking* you for the definition. Of
course, I don't know the definition.
So I'm ignorant. Teach me.
--
Jesse F. Hughes
"Maybe I screwed up on one of my assumptions [...]. Otherwise, um,
it's very easy to factor, and things are about to get really, really
weird." -- James S. Harris
Jesse F. Hughes
Right. You've got him beat. You've come up with *lots* of great
theorems, so what does it matter that your logic is an utterly
incoherent mess?
--
"Memoirists like Frey and Augusten Burroughs belong to the long list of
those who should never have stopped using drugs. The drugs might have
made Frey more interesting, or they might have killed him. Either way,
American literature would have benefited." --John Dolan, www.exile.ru
Charlie-Boo
I just wrote 2 or 3 fairly extensive descriptions of CBL and its use
and purpose. You should be able to tell the difference between
mathematics and metamathematics. CBL is designed to prove statements
about proving. Its fundamental expressions are (as I explained in
detail):
M # P / Q : M characterizes relation P in base Q. P is typically one-
place and Q is two places, in which case
P(x) <=> Q(M,x). This allows us to represent properties of wffs and
computer programs.
P / Q : There is an M such that M # P / Q. This allows us to
represent the assertions that P is recursively enumerable, P is
expessible (in the Logic), P is representable, P is a well-founded
set, P is expressible in English, etc.
P,Q : P and Q are logically equivalent.
- P,Q : P and Q are not equivalent. For example, -PR,TW means truth
does not equal provability. -PR,~DIS means provability does not equal
non-refutability.
When we reach a statement of the form P,Q or -P,Q we can apply
Propositional Calculus to produce statements like TW(M)+~PR(M) : There
is a sentence that is true and not provable.
Does this give you a flavor of what CBL was designed to do? You will
also notice the same flavor in the dozen or so proofs that I have
posted. Each shows that two sets are not equal (this is the case in
incompleteness theorems e.g. Godel-1 and Rosser 1936) or that a
particular set is not expressible/representable/r.e. etc. This the
case in Turing 1937 and Godel-2.
If you want proofs of specific wffs e.g. the wff that expresses
Associativity of Addition, I can start with P/PR (P is representable)
and we have P(x) <=> |-P(x) and I can prove facts about specific wff
P. This is the link between the Metamathematical assertion concerning
representability in the Logic, and the Mathematical proof of
individual wffs.
I stated earlier the procedue for issuing a challenge.
Charlie-Boo
> On Mar 14, 12:02 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > What is the value in spending precious bandwidth debating something as
> > nebulous and arbitrary as what is the most common use of terminology?
>
> He's not debating. Rather, he's doing you the favor of informing you.
Can you say that with a str8 face?
> And it's not just that the terminology is common - it's terminology
> that is virtually agreed upon.
It was a passing comment concerning characterizing sets. It really
has nothing to do with CBL. Notice that there is no mention of
cardinality in any of the CBL expression (operators) that I list every
time I write a description of how CBL works?
I said that for my purposes, the distinction is between the finite
sets, the denumerable sets (I shouldn't have said "r.e."), the power
sets of the denumerable sets, etc. But in none of my proofs do I
refer to cardinality.
Think of something useful, ok? This is a pathetic waste of time.
C-B
Charlie-Boo
Ok. Take any of my treatises on CBL and tell me what is unclear. I
will rewrite it until you say it is clear. It can be the start of a
formal definition of CBL that everyone agrees is coherent.
C-B
> --
> Jesse F. Hughes
> "Maybe I screwed up on one of my assumptions [...]. Otherwise, um,
> it's very easy to factor, and things are about to get really, really
> weird." -- James S. Harris- Hide quoted text -
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 14, 3:27 pm, Chris Menzel <cmen...@remove-this.tamu.edu> wrote:
> >> On Fri, 14 Mar 2008 11:39:21 -0700 (PDT), Charlie-Boo
> >> <shymath...@gmail.com> said:
>
> >> > ...You can say that finite sets have their own individual
> >> > cardinalities if you want (number of elements), but I have found it
> >> > easier if you treat the finite sets as one class, the r.e. sets as the
> >> > second, the reals/subsets as the 3rd., etc.
>
> >> Finite sets are r.e. Does this mean your first class is included in
> >> your second class? Also, where do denumerable non-r.e. sets fit into
> >> your picture? (NB: For mathematicians, "denumerable" = "has cardinality
> >> aleph_0", so you'll need to be careful when you frame your answer, given
> >> that, in your unique idiolect, "aleph_0" = "finite".)
>
> > Is that the best you can some up with?
>
> > How about telling us the very best theorem that you have ever
> > discovered yourself?
>
> Right. You've got him beat. You've come up with *lots* of great
> theorems, so what does it matter that your logic is an utterly
> incoherent mess?
That's right. The proof is in the pudding. CBL generates incredibly
short proofs, incredibly large numbers of proofs, new proofs, and
nobody has found anything wrong with any of the proofs. All you can
say is you don't like the way it's described?
If a system somehow comes up with all of the above, doesn't that tell
you there is something to it? Doesn't that make you consider the
possibility that instead of condemning the system because you don't
like the way it created its dozens of proofs, that maybe there is some
value to how it produced them?
The proof is in the pudding. You can't knock success.
If you can find something wrong with the theorems and proofs that it
produces, then the system is not good. But if you can't, and the
theorems and proofs are real, then is it a coincidence? Or must it
have some way of logically coming up with these results? And instead
of trying to tear it down because of how it's described, see the value
in the results - maybe even be interested in how it actually works
(how it comes up with these proofs)? Wouldn't that be more
productive?
And if my description is in fact poorly written, tell me what wording
is unclear. I will glady - eagerly - try to make it more
intelligible. But don't say that because the description is hard to
understand, the system shits. Not cool.
C-B
> --
> "Memoirists like Frey and Augusten Burroughs belong to the long list of
> those who should never have stopped using drugs. The drugs might have
> made Frey more interesting, or they might have killed him. Either way,
> American literature would have benefited." --John Dolan,www.exile.ru- Hide quoted text -
Chris Menzel
<shyma...@gmail.com> said:
>>
>> Once again, my answer is that your question is so ill-formed that one
>> can only guess at what you mean. Spelled out the only way that I
>> could think of, the answer was trivial.
>
> It's a question of definitions, not a problem to claim trivial in your
> pointless meager efforts to debase the intellectual capabilities of
> those who disagree with you.
I have never debased your intellectual capabilities. I *have* mocked
your attempts to criticize modern set theory, logic, and computability
theory when it is evident from your muddled criticisms that you are
monumentally ignorant of the subject matter and its history.
>> > Then (all x)P(x) is a wff even if P is not a relation?
>>
>> Well, there you go again. You *think* you are asking a question but it
>> is completely ill-formed. You are badly confusing syntax and semantics.
>> What does or does not count as a wff is wholly a matter of the grammar
>> of the language in question.
>
> But whether it defined a set or not depends on the parts of the wff.
Nope. THAT depends on the *theory*.
>> If you have a question about a specific expression, that is, a
>> specific string of symbols in the language of set theory, I can tell
>> you in two seconds whether or not it is a wff.
>
> (x e y) v (y e x)
wff, obviously.
>> In particular, if P(x) is a wff (containing, presumably, free
>> occurrences of "x"), then, by the grammar for first order languages,
>> we know immediately that "(all x)P(x)" is a wff. If P(x) is not a
>> wff, then we know immediately that "(all x)P(x)" is also not a wff.
>> This is just elementary formal syntax.
>
> So you include non-relations.
You are confusing syntax and semantics again. I gave you an answer
about syntax. To talk about a wff "including non-relations" is
completely senseless. Relations are not syntax hence can't be
"included" in a wff.
>> Your question also seems to involve the issue of whether or not, for
>> a given wff P(x) containing free occurrences of "x", there is a set
>> of things of which P(x) is true. That, of course, is settled by the
>> axioms of ZF. But your question as it stands is just gibberish.
>> Really, the best thing you could do for yourself is study basic
>> mathematical logic and set theory.
>
> Study it? I'm trying to fix it.
Remarks like this, among others, are why you are not taken seriously.
It is more than evident to anyone with a bit of study behind them that
you are profoundly confused about, and ignorant of, elementary set
theory, mathematical logic, and their history. For you, in this state,
(a) to claim something is wrong with set theory and (b) that you know
how to fix it is simply, and rather sadly, ludicrous.
>> > If we assume that, then naturally a wff does not necessarily define
>> > a set since it can refer to non-sets. If a wff doesn't refer to
>> > non-sets, then the wff defines a set. There's no paradox or
>> > contradiction.
>>
>> If you were actually to study set theory, you would see very early on
>> why your assertion here is just a confused mess.
>
> This isn't Set Theory, it's CBL. Maybe that's your problem.
Well, then it is CBL that is confused -- a point I have already
illustrated in a number of posts.
Do you mean: Is there, in ZF, a set {<x,y> | (x e y) v (y e x)}? No.
It is very easy to show in ZF that there is no such set. (Sketch of
proof: Suppose there is such a set S. Then by the axiom of separation,
the set {<x,y> e S | x e y} exists. (Note that that is simply the
membership relation.) If the membership relation is a set, its domain D
is a set. Since every set is a member of some set, D is in fact the set
of all sets. By the axiom of foundation, every set, hence every member
of D, is not a member of itself. Hence, D is the set of all
non-self-membered sets, from which, by the usual reasoning, it follows
that D e D iff ~(D e D), contradiction.)
>> > To say that a wff is not a set is throwing the baby out with the
>> > bathwater.
>>
>> Well, no wff *is* a set (at least, not in the way you mean it).
>
> You have now joined the ranks of Bill Clinton by adding to the list
> [fix, avoid, refer] the word "is".
Well, I feared I'd confuse you if I added that qualification. What
*you* mean when you say "a wff is a set" is that the wff *defines* a set
in the sense indicated above. Your way of putting it again confuses
syntax and semantics. What *I* meant by adding the qualification above
is that, if one does the metatheory of a language in pure ZF, then the
lexical elements of the language can themselves be identified with
arbitrary pure sets. So, in that special case, wffs are literally sets.
But that's an irrelevant theoretical nicety that is only a red herring
here.
As for your "list", I'm afraid it simply reflects your inability to get
the point.
>> Do you mean: "To deny that every wff defines a set is to throw the
>> baby out with the bathwater"? That's a clear assertion. It is
>> also wrong. To affirm that every wff (with a free variable) defines
>> a set leads to inconsistency. Inconsistency is the bathwater. The
>> baby is the useful mathematics that can be done in, or with the aid
>> of, set theory. ZF does a remarkably good job of tossing out the
>> bathwater and hanging on to the baby. Again, if you'd commit six
>> months to actually learning the basics, you could discover this for
>> yourself.
>>
>> > We can do better by telling which wffs are sets and which are not.
>>
>> Again, if you mean "by telling which wffs define sets and which do not",
>> that (among other things) is pretty much exactly what axiomatic set
>> theory does for you.
>>
>> > Where did Zermelo, von Neumann, Gödel, et al address that?
>>
>> In ZF set theory and VonNeumann/Gödel/Bernays set theory, of course.
>
> What is the procedure to determine if a given wff defines a set?
Well, I doubt there is a general procedure. I'm not enough of a set
theorist to be able to come up with an example off the top of my head,
but it strikes me there must be, say, definable properties P of ordinals
such that it is not known, and perhaps provably unknowable in ZF,
whether there is an upper bound on the ordinals that have P. (Anybody?)
If a wff A(x) defines such a P, then there is no procedure for
determining whether A(x) defines a set, just as there is no general
procedure for determining whether a given wff of first-order logic is a
logical truth. Thanks to Gödel we know there are limitations of this
sort that we just have to live with.
I'm relative certain you'll claim CBL has such a procedure. No
surprise, though, CBL can do anything if we wish hard enough, right?
Jesse F. Hughes
I have to read a whole treatise just to learn what your definition of
cardinality is?
--
Jesse F. Hughes
"Readers should remember that being able to post on Usenet does not mean
a person actually has expertise in a particular area or even knows
ANYTHING significant in that area." -- James S. Harris
Jesse F. Hughes
> On Mar 14, 9:09 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>>
>> Right. You've got him beat. You've come up with *lots* of great
>> theorems, so what does it matter that your logic is an utterly
>> incoherent mess?
>
> That's right. The proof is in the pudding. CBL generates incredibly
> short proofs, incredibly large numbers of proofs, new proofs, and
> nobody has found anything wrong with any of the proofs. All you can
> say is you don't like the way it's described?
Right. That's the only complaint. Nothing wrong with any of the
proofs, aside from that pesky bit that only you know what counts as a
proof.
Say, how's that work on David Ullrich's request coming along?
--
One these mornings gonna wake | Ain't nobody's doggone business how
up crazy, | my baby treats me,
Gonna grab my gun, kill my baby. | Nobody's business but mine.
Nobody's business but mine. | -- Mississippi John Hurt
William Hale
<9df49f3b-9476-475f...@t54g2000hsg.googlegroups.com>,
Charlie-Boo <shyma...@gmail.com> wrote:
[cut]
> And if my description is in fact poorly written, tell me what wording
> is unclear. I will glady - eagerly - try to make it more
> intelligible.
I find it hard to understand CBL because you usually give all the things
that CBL can do. Such a presentation forces me to try to see how all
that fits together and raises questions for me that concern this
inter-relation between all these things. But, I would prefer to
concentrate on just one of the things that CBL can do and work from
there.
I would like to chose "Set Theory" of the many things that CBL does.
I think it would help to present CBL with regards to "Set Theory" only.
I quote from a former post of yours:
==========================
5. Set Theory
We can state most of the standard axioms of Set Theory pretty easily.
Many are theorems from more primitive axioms than those given in
print. For example, Pairing is theorem EQ(I,x)vEQ(J,x) from axioms
EQ(I,x) for every thing there is a set that contains just it, and P,Q
=> PvQ the union of two sets is a set. Comprehension is P/SE , Q/TW
=> P^Q/SE.
When you formalize these axioms in CBL you notice that they refer to
other mathematical objects like functions and wffs, without giving
axioms (formal definitions) for them. And remember that not being
exact about what a wff consists of is what gets us in trouble with the
Russell Paradox.
==========================
Request 1: What is the starting explanation of how CBL does "Set
Theory"? Keep it brief; I can ask you to expand on it further later.
From that former post that I mentioned above, I suspect that you will
give the axioms, terms, etc that form the basis of CBL Set Theory.
Request 2: I object to the wording "axioms (formal definitions)" above.
For me, "axiom" does not mean "formal definition." I think the standard
terminology is that "functions are primitive" something. I forget what
that "something" is.
Request 3: If you can, include Pairing that you mentioned above, unless
it will take pages to get to that point (if so, we can come to pairing
later after request 1 is done).
Charlie-Boo
wrote:
> On Fri, 14 Mar 2008 12:26:58 -0700 (PDT), Charlie-Boo
> <shymath...@gmail.com> said:
>
>
>
> >> Once again, my answer is that your question is so ill-formed that one
> >> can only guess at what you mean. Spelled out the only way that I
> >> could think of, the answer was trivial.
>
> > It's a question of definitions, not a problem to claim trivial in your
> > pointless meager efforts to debase the intellectual capabilities of
> > those who disagree with you.
>
> I have never debased your intellectual capabilities.
Why the references to "trivial"? Why is it so common here, do you
suppose?
> I *have* mocked
> your attempts to criticize modern set theory, logic, and computability
> theory when it is evident from your muddled criticisms that you are
> monumentally ignorant of the subject matter and its history.
It's not the subject mattter - that is referring to something real.
It is the BS authors who make unsubstantiated claims. One of the
worst cases is the Boyer/Moore article about a "mechanical proof of
the unsolvability of the halting problem". Now, look through the
books on the Theory of Computation, and what do you read about this
proof? There is nothing about what they did and the useful principles
developed and used.
I'm not talking about them and their articles and claims. I mean
reality - what axioms, rules, algorithms, insite have they produced
from this supposed proof? How does one study their technology?
"Read the manuals." - That misses the whole point. Is it an
accomplishment to write a manual? What have they done that is so
valuable that we should be interested in the first place? What is
there to "study"? Their neat new axioms? Their rules of inference?
The array of Theory of Computation results that they proved using the
same process - unsolvability of the ever-halting, always-halting, self-
halting or membership problem? Their article mentions none of these,
not even the self-halting problem whose unsolvability is a lemma in
Turing's proof.
In my M Computing article, I list a program that creates 27 theorems.
I show a general expression that represnts the 27 theorems as special
cases. I show how Turing's proof is represented. I show the program
transformations use formalized. I give a program that produces the
theorems - the expressions for each. There is all sorts of real
information there. There is nothing in the Boyer Moore article. They
don't even describe the proof being formalized. (No, it's not a
matter of my knowing the proof anyway. The question is how they
formally represented and synthesized it. Nothing is given in the
paper.)
So what do I study? It's not so much that the technology is "bad" and
we can study and learn more about it. It's that we have papers with
grandiose titles and nothing between the covers. There is nothing to
study.
Turing and Godel's results were real, and we have lots of results -
many theorems, new concepts such as the (primitive then general)
recursive functions/relations, the new idea that some mathematical
functions cannot be carried out by a computer. What are the results,
technology, new algorithms from Boyer/Moore that we should study and
learn more about?
I have quoted authors, results, my theorems and theirs. If they are
so good, why can't you show where I am wrong?
Who has formally generated a computer program - where is the program
and what were the axioms/rules used?
Who has axiomatized the Theory of Computation and shown how to
formally represent its theorems and their proofs?
Who has axiomatized Recursion Theory? Incompleteness in Logic (Proof
Theory)?
You make no refences to the real problem. You do not refute what I am
saying. Your only contribution is baseless claims. Stupid arguments
trying to score points because I take a different approach - my
handling of the problems is different, so I must not know how to do it
right.
No, my handling is different because I show real results - a dozen
proofs and NONE of them has ever been challenged, much less refuted.
Now why don't you show valuable material like that? I show how I
axiomatized these branches of computer science. Is there something
wrong with the theorems created? Where have these axiomatizations
been developed and presented?
That is my point. And as these published axiomatizations don't exist,
there never is an answer to the question of substantiating claims that
it's been done before. Yet people still debate - but about what? The
meaning of "is".
> >> > Then (all x)P(x) is a wff even if P is not a relation?
>
> >> Well, there you go again. You *think* you are asking a question but it
> >> is completely ill-formed. You are badly confusing syntax and semantics.
> >> What does or does not count as a wff is wholly a matter of the grammar
> >> of the language in question.
>
> > But whether it defined a set or not depends on the parts of the wff.
>
> Nope. THAT depends on the *theory*.
What is your method for deciding if a wff defines a set, then?
> >> If you have a question about a specific expression, that is, a
> >> specific string of symbols in the language of set theory, I can tell
> >> you in two seconds whether or not it is a wff.
>
> > (x e y) v (y e x)
>
> wff, obviously.
Does it define a set?
> >> In particular, if P(x) is a wff (containing, presumably, free
> >> occurrences of "x"), then, by the grammar for first order languages,
> >> we know immediately that "(all x)P(x)" is a wff. If P(x) is not a
> >> wff, then we know immediately that "(all x)P(x)" is also not a wff.
> >> This is just elementary formal syntax.
>
> > So you include non-relations.
>
> You are confusing syntax and semantics again. I gave you an answer
> about syntax. To talk about a wff "including non-relations" is
> completely senseless. Relations are not syntax hence can't be
> "included" in a wff.
The problem is that some wffs are not sets (relations). Right?
Wffs contain smaller parts, right?
Those parts include references to relations, right?
There are things that aren't sets (relations), right?
What's the problem?
> >> Your question also seems to involve the issue of whether or not, for
> >> a given wff P(x) containing free occurrences of "x", there is a set
> >> of things of which P(x) is true. That, of course, is settled by the
> >> axioms of ZF.
You still haven't substantiated this by giving your procedure for
deciding if a wff defines a set or not.
> But your question as it stands is just gibberish.
> >> Really, the best thing you could do for yourself is study basic
> >> mathematical logic and set theory.
>
> > Study it? I'm trying to fix it.
>
> Remarks like this, among others, are why you are not taken seriously.
> It is more than evident to anyone with a bit of study behind them that
> you are profoundly confused about, and ignorant of, elementary set
> theory, mathematical logic, and their history.
Lots of claims - any evidence? If I do it differently than your fav
authors, it's not because I am making mistakes in using their
technology. It is not an attempt to copy them. They have already
published their results. Like any research, it is showing a better
way.
It's just a choice of words - defines or is. Mostly I say "defines"
and perhaps occasionally I say "is", so you try to say there's a
problem with "confusing syntax with semantics"?
If you're so picky, how can you say both "No wff *is* a set." and "In
that case wffs are sets."?
> What *I* meant by adding the qualification above
> is that, if one does the metatheory of a language in pure ZF, then the
> lexical elements of the language can themselves be identified with
> arbitrary pure sets. So, in that special case, wffs are literally sets.
> But that's an irrelevant theoretical nicety that is only a red herring
> here.
>
> As for your "list", I'm afraid it simply reflects your inability to get
> the point.
>
>
>
>
>
> >> Do you mean: "To deny that every wff defines a set is to throw the
> >> baby out with the bathwater"?
No, the problem itself is that not every wff defines a set.
> > > That's a clear assertion. It is
> >> also wrong. To affirm that every wff (with a free variable) defines
> >> a set leads to inconsistency. Inconsistency is the bathwater. The
> >> baby is the useful mathematics that can be done in, or with the aid
> >> of, set theory. ZF does a remarkably good job of tossing out the
> >> bathwater and hanging on to the baby. Again, if you'd commit six
> >> months to actually learning the basics, you could discover this for
> >> yourself.
>
> >> > We can do better by telling which wffs are sets and which are not.
>
> >> Again, if you mean "by telling which wffs define sets and which do not",
> >> that (among other things) is pretty much exactly what axiomatic set
> >> theory does for you.
>
> >> > Where did Zermelo, von Neumann, Gödel, et al address that?
>
> >> In ZF set theory and VonNeumann/Gödel/Bernays set theory, of course.
>
> > What is the procedure to determine if a given wff defines a set?
>
> Well, I doubt there is a general procedure.
Finally!!!!!!!!!!!!!!!!!!!
> I'm not enough of a set
> theorist to be able to come up with an example off the top of my head,
> but it strikes me there must be, say, definable properties P of ordinals
> such that it is not known, and perhaps provably unknowable in ZF,
> whether there is an upper bound on the ordinals that have P. (Anybody?)
> If a wff A(x) defines such a P, then there is no procedure for
> determining whether A(x) defines a set, just as there is no general
> procedure for determining whether a given wff of first-order logic is a
> logical truth. Thanks to Gödel we know there are limitations of this
> sort that we just have to live with.
>
> I'm relative certain you'll claim CBL has such a procedure. No
> surprise, though, CBL can do anything if we wish hard enough, right?
Yuh, right.
C-B
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 14, 9:07 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > On Mar 14, 3:30 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
> >> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> >> > On Mar 14, 7:38 am, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>
> >> >> >> You *do* know what a definition is, right? Here, I'll get you
> >> >> >> started:
>
> >> >> >> Let X and Y be sets. We say that X and Y have the same
> >> >> >> /cardinality/ just in case ...
>
> >> >> > In CBL or what?
>
> >> >> Sure, in CBL is fine. What is the definition of cardinality in CBL?
>
> >> > All this time you didn't even know the fundamentals of the subject you
> >> > were discussing. My goodness!
>
> >> What an odd response! I was *asking* you for the definition. Of
> >> course, I don't know the definition.
>
> >> So I'm ignorant. Teach me.
>
> > Ok. Take any of my treatises on CBL and tell me what is unclear. I
> > will rewrite it until you say it is clear. It can be the start of a
> > formal definition of CBL that everyone agrees is coherent.
>
> I have to read a whole treatise just to learn what your definition of
> cardinality is?
No, CBL doesn't refer to cardinality. The concept was mentioned in
some discussion (I forget the context) but it isn't used in CBL. I
only humored those who (1) heard the conversation, (2) concluded that
I was using a term "wrongly", (3) tried to say that was part of CBL
and so CBL is broken. Just the typical silly waste of time.
C-B
> --
> Jesse F. Hughes
> "Readers should remember that being able to post on Usenet does not mean
> a person actually has expertise in a particular area or even knows
> ANYTHING significant in that area." -- James S. Harris- Hide quoted text -
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 14, 9:09 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>
> >> Right. You've got him beat. You've come up with *lots* of great
> >> theorems, so what does it matter that your logic is an utterly
> >> incoherent mess?
>
> > That's right. The proof is in the pudding. CBL generates incredibly
> > short proofs, incredibly large numbers of proofs, new proofs, and
> > nobody has found anything wrong with any of the proofs. All you can
> > say is you don't like the way it's described?
>
> Right. That's the only complaint. Nothing wrong with any of the
> proofs, aside from that pesky bit that only you know what counts as a
> proof.
Why is the state of my mind a criterion for the evaluation of the
proofs?
Why has nobody (including yourself) shown anything wrong with them?
> Say, how's that work on David Ullrich's request coming along?
Write a prgram to syntax check proofs? Why? Here's an article that I
just posted that contains a computer program that generates (lists) 27
theorems, including Turing's. See, there is no need for a syntax
checker, as the program creates the syntax.
(Boyer and Moore claim that they ran a proof of one theorem of
Turing's through a syntax checker to "verify the proof." But that
only says that the user entered in the right syntax for some proof.
That doesn't say anything about what the proof proves or anything
about the halting problem. What's the point?)
(BTW Did you know that Boyer and Moore only represent Propositional
Calculus, no Predicate Calculus wffs at all? Yet they proved the
unsolvability of the Halting Problem? How does one prove any set not
recursive - using Predicate Calculus, of all things?)
Has he written any programs to generate theorems, I wonder? That
would be useful.
C-B
Charlie-Boo
> In article
You mean how do I generate theorems of set theory? I can but don't
bother to, really. I mention Program Synthesis, Theory of Computaton,
Recursion Theory and Incompleteness in Logic (Proof Theory) as 4
systems that I have axiomatized. When people talk about the ZF
axioms, I sometimes mention (as above) that most of these axioms are
easy to represent, and as in the case just mentioned, I sometimes show
how some of the ZF "axioms" are CBL theorems. It is not a big
interest because nothing new is generated. In other branches of
Computer Science, we generate new, significant theorems that aren't so
obvious, e.g. those of Godel, Rosser, Turing and Smullyan.
But I can see that much of ZF's theorems can be easily proven in CBL,
and I can give as an example the generating of the ZF Pairing Axiom:
SE(x,y) means y is an element of set x. P(x)/Q(a,b) means set P can
be characterized in base (2 place relation) Q, which by definition of
the "/" operator means that there is an M which characterizes P(x)
meaning that P(x)<=>Q(M,x). So M is the set that contains the
elements of P.
The Pairing Axiom is wff EQ(I,x)vEQ(J,x): For any two values I and J
there is a set that contains every value that is equal to I or equal
to J. This means that EQ(I,x)vEQ(J,x)/SE (we declare SE as the
default base) which is saying that wff EQ(I,x)vEQ(J,x) defines a set.
We can prove that using simple general useful axioms:
EQ(I,x) For every thing, there is a set that contains only it.
UNION: P(x) , Q(x) => P(x) v Q(x) The union of two sets is a set.
SUB: P(I) => P(J) [The rule is trying to say that we can replace any
input variable by any other input.]
Thm. Pairing Axiom EQ(I,x)vEQ(J,x) There is a set that contains
every value that is equal to I or equal to J.
1. EQ(I,x) Axiom: For every thing there is a set that contains only
it.
2. EQ(J,x) SUB 1 For every second thing there is a set that contains
only it.
3. EQ(I,x)vEQ(J,x) There is a set that contains all values equal to a
given thing I or a second thing J.
qed
So the answer is that CBL does Set Theory the same way that it
axiomatizes any branch of Computer Science: via Axioms and Rules of
Inference. I have never bothered/tried to generate lots of Theorems
from Set Theory, because they generally are not enlightening, as they
are statements already known.
(Please don't make the mistake of confusing ZF with Set Theory. ZF is
one possible set of axioms for some sort of Set Theory. Set Theory
includes the syntax and semantics of wffs. You can use the syntax and
semantics of wffs to define sets or to even use the Set Theory wffs as
the set of expressions in a diffrerent system. But the ZF axioms
aren't used to prove anything outside of simple, fairly obvious,
statements about sets. (Refutations welcome.)
But, as I say, we can represent most of e.g. ZF's axioms. Continuing
the above discussion, we have:
1. Extensionality: Is the use of DEF inCBL.
ZF: If the elements of A are all the elements of B, then A=B.
CBL: If all the elements of A are all the elements of B, then we can
substitute A for B.
P , Q means all the elements of P are all the elements of Q.
2. Pairing: Is a theorem EQ(I,x)vEQ(J,x)/SE as explained above.
3. Separation: P/SE , Q/TW => P^Q/SE If P is expressible and Q is a
set, then P^Q is a set.
4. Sum Set: P(x) => (eA)P(A)^SE(A,x)/SE
5. Power Set: (aA)~SE(x,A) v SE(I,A)/SE
6. Infinity: TRUE / SE
7. Replacement: P/SE , Q/TW => P(x)^Q(x,y)/SE => (eA)P(A)^Q(A,x)/SE
8. Empty Set: ~TRUE / SE
9. Foundation: -~SE / SE
10. Choice: M # P / SE + -P,~TRUE => SE(M,aoc(M))
> Keep it brief; I can ask you to expand on it further later.
> From that former post that I mentioned above, I suspect that you will
> give the axioms, terms, etc that form the basis of CBL Set Theory.
Yes, above.
> Request 2: I object to the wording "axioms (formal definitions)" above.
> For me, "axiom" does not mean "formal definition." I think the standard
> terminology is that "functions are primitive" something.
What does ' "functions are primitive" refer to?
> I forget what that "something" is.
Axioms (and Rules) are part of an Axiomatic System, which is a
formalization of the subject matter being referred to. CBL axioms are
statements given as being true, as in any use of the notion of an
axiom.
> Request 3: If you can, include Pairing that you mentioned above, unless
> it will take pages to get to that point (if so, we can come to pairing
> later after request 1 is done).
See above.
C-B
Jesse F. Hughes
> No, CBL doesn't refer to cardinality. The concept was mentioned in
> some discussion (I forget the context) but it isn't used in CBL. I
> only humored those who (1) heard the conversation, (2) concluded that
> I was using a term "wrongly", (3) tried to say that was part of CBL
> and so CBL is broken. Just the typical silly waste of time.
There is no definition of cardinality in CBL and yet you mocked my
ignorance for not knowing the definition of cardinality in CBL?
Wow. That *is* a silly waste of time.
--
"It has been shown that no man can sit down to write without a very profound
design. Thus to authors in general trouble is spared. A novelist, for example,
need have no care of his moral. It is there -- that is to say, it is somewhere
-- and the moral and the critics can take care of themselves." --E.A. Poe
Jesse F. Hughes
> On Mar 14, 11:05 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>
>> Right. That's the only complaint. Nothing wrong with any of the
>> proofs, aside from that pesky bit that only you know what counts as a
>> proof.
>
> Why is the state of my mind a criterion for the evaluation of the
> proofs?
Because we don't know what counts as a proof in CBL. You haven't
stated that clearly and concisely.
> Why has nobody (including yourself) shown anything wrong with them?
If we don't know the criteria, how can we show that they fail to meet
them?
I'll skip discussion of your proof generator until you state clearly
the method for determining whether a bit of text is a proof. It
really is essential, you know.
--
"So, at this time, I'd like to assure you that I am not interested in
making sure mathematicians worldwide get fired."--JSH Apr 28, 2003
"I'll have prosecutors knocking on your doors. I have no problem with
any number of mathematicians spending time in jail."--JSH Jun 10, 2003
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On Mar 14, 11:05 pm, "Jesse F. Hughes" <je...@phiwumbda.org> wrote:
>
> >> Right. That's the only complaint. Nothing wrong with any of the
> >> proofs, aside from that pesky bit that only you know what counts as a
> >> proof.
>
> > Why is the state of my mind a criterion for the evaluation of the
> > proofs?
>
> Because we don't know what counts as a proof in CBL. You haven't
> stated that clearly and concisely.
>
> > Why has nobody (including yourself) shown anything wrong with them?
>
> If we don't know the criteria, how can we show that they fail to meet
> them?
I mean the proof, not its formal representation. e.g.
1. HALT(I,J)* Assumption: Assume the halting problem is solvable.
2. P(I)* => ~P(I)* Rule NOT: The complement of a recursive set is
recursive.
3. ~HALT(I,J)* Substitution 1,2: So the non-halting problem is
solvable.
. . .
4. False So the halting problem is not solvable after all.
qed
I have given the proofs: "Assume the halting problem is solvable. The
complement . . . So the halting problem is is not solvable after all."
and nobody has ever disagreed that these are actual proofs.
I suspect that this is a bit foreign to most everyone, a formal proof
that maps into an actual proof, which is what a theorem-prover must do
- generate proofs. Not "Here is a LISP program and it
proves . . ." (HUH??) but rather "Assume the halting problem is
solvable. . . . "
> I'll skip discussion of your proof generator until you state clearly
> the method for determining whether a bit of text is a proof.
I don't really need to do that, as I may have explained. But if you
want to, then of course the proofs are enumerated by your axioms and
rules. So that would give us a partial solution. But since the set
is recursive, why settle for that, right?
So, as always, a proof consists of a tree (displayed as a list) of
sentences, each an axiom or assumption or the result of a rule of
inference applied to its children. As a list, we can make sure that
every child node appears in the list before its parent (proof?), so
each item in the list is an axiom or assumptiomn or the result of a
rule of inference applied to earlier items in the list. (Can't we
always get rid of assumptions? I have asked this before.)
Now, what are the axioms and rules? Each branch of computer science
has its axioms and rules - with a dazzling array of overlaps. For
example, one axiom of Incompleteness in Logic is -~P/P which
represents diagonalization. In one step (substitution) we can prove
there is no set of sets that contain themselves, the set of programs
that don't halt yes is not r.e., there is no English sentence that
says that a given sentence is not true (and also follows certain rules
of truth), the set of unprovable sentences is not representable in the
Logic, etc.
(1) At the same time, an axiom of the Theory of Computation is -
~YES(x,x) the set of programs that do not halt yes on themselves is
not r.e. This is a theorem of Incompleteness in Logic. So an axiom
from one branch of Computer Science is a theorem of another. (This is
because the Theory of Computation is a special case of Incompleteness
in Logic because we use only one base, Turing Machines, and so can use
a simpler system where e.g. the base is omitted from wffs.)
(2) The same axiom sometimes appear in multiple branches of Computer
Science in different forms. For example, Recurson Theory has axiom
wr(I) # I for every number there is a program that writes only it,
while Set Theory has axiom EQ(I,x)*/SE which means for every thing I
there is a set that contains just it. This is saying it exists while
wr(I) # I gives a constructive proof that the program exists because
we also have wr(I) function wr is recursive.
Now, with (1) and (2) in mind, do we combine all of the axioms from
the various branches of Computer Science into one nice set of axioms
for all of Computer Science? Of course, at some point. This is just
continuing the process of abstraction that begins with abstracting the
various theorems and proofs into axioms and rules, and continues here
by abstracting the various axioms and rules into a higher level.
If I can just say that "the rule applies to the sentence . . ."
without giving details of what relation that is and how to decide it,
then I can talk in general terms without reference to whether it is
one branch of Computer Science or all of Computer Science.
Or I can give the procedure for one branch of CS - Program Synthesis,
Theory of Computation, Recursion Theory or Incompleteness in Logic -
and explicitly list every axiom and rule.
As far as CBL at the CS level (all branches) goes, I have developed
formalizations of the various branches per se e.g. Program Synthesis
is x # I / YES input the wff solved (I) and output all programs (x)
that solve it using Turing Machines (YES) as the system (programming
language.) The next thing to do there is to see if we can derive the
axioms from the definition of the branch of CS e.g. x # I / YES gives
us axioms of the form M # P / YES Turing Machine M accepts/enumerates
set P.
So the question is, would you like the procedure for any particular
branch of CS (list above) or for all of CS (in which case it would
help greatly if I could leave out the details of the actual axioms and
rules since I haven't reached that level of abstraction yet, as
described above.)?
> It really is essential, you know.
Not for a theorem generator (we need to enumerate proofs, not decide
them), but for you Jesse, anytime.
C-B
People like to throw huge complex unnecessary requirements at
solutions that don't need them. Sometimes I humor them and show the
pointless procedure just to prove them wrong (without appealing to its
being unnecessary.) But if it's too big and hairy, I will have to
show that it would take forever and is a total waste of time. In the
current case, I am continuing to humor people.