Misplaced Pages

Revision as of 06:35, 6 November 2007

m:User:CBM	Please leave new comments at the bottom of the page, using the "new section" button at the top of the page. I will respond on this page unless you request otherwise.	Archives 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

Paper re Godel and a machine-based proof

If it's not too much of a bother could you email me a cc also? pierab@aol.com. Thanks, Bill. (I'm still bugged by this whole thing. Turing's original first circle-testing proof is so different from the Davis "halting problem" proof. It didn't "quine" its own operating system, it tested numbers one after another until it hit its own number (same thing). Because it had to create a diagonal number for every successfully "non-circular" number, it had to "execute" its own code, thus causing it to start over and thereby "circle" (contrary to premise ... Q.E.D.). I want to double-check and be sure that these guys aren't re-inventing the wheel. Bill Wvbailey 13:57, 2 November 2007 (UTC)

Got it. Thanks, Bill Wvbailey 23:32, 4 November 2007 (UTC)

3meandEr

You commented on WP:AN last week concerning a proposed 0RR/1RR regime on the article Northern Cyprus, which is being disrupted by a SPA, User:3meandEr. I've posted a request for a block or community ban on this user at WP:AN/I#User:3meandEr and Northern Cyprus - your comments would be appreciated. -- ChrisO 11:21, 3 November 2007 (UTC)

Link to German username

I have registered de:User:CBM2. — Carl (CBM · talk) 13:46, 5 November 2007 (UTC)

Toolserveraccount

Hello CBM,
please send your real-name, your wikiname, your prefered login-name and the public part of your ssh-key to . We plan to create your account soon then. --DaB. 16:47, 5 November 2007 (UTC)

Halting problem

You claim that the CS definition of the problem is no good. It is referenced, it is accurate, and it is brief. It avoids the problem of defining the x,x business by quining, and it is not in any way original. I was hoping you could tell me what your complaints are.Likebox 19:50, 5 November 2007 (UTC)

BTW, the rewrite you gave is IMO not very satisfactory. It removed a complete proof and replaced with very vague language. Please discuss your changes.Likebox 20:05, 5 November 2007 (UTC)

Hi, I'm really sorry for being suspicious that you are not real! I hope you are not offended. But please, read and understand the proof in its entirety before condemning it. I believe you are sincere in wanting the recursion theoretic proof, and of course that's fine. But this proof is coherent and correct, and can be understood by non-specialists. I understand the recursion theoretic proof, and it does have some points in its favor, but the main issue is Kleene's fixed point theorem.

This theorem is just a restatement of the "existence of Quines", but in an unnecessarily complicated language. There is absolutely no reason for the recursion theoretic language complications, and the proof I gave is a demonstration by example that everything can be just as precise without any Kleeneisms. I hope you take the time to think about it carefully, again, and I can assure you beyond any shadow of a doubt that it is precise and correct. Again, I am sorry for doubting your authenticity.Likebox 22:35, 5 November 2007 (UTC)

The recursion theorem says more than just quines exist. It says that any recursive operator has a fixed point. There is no way to get that directly from the fact that quines exist.

In the end, for your changes to remain you will need to convince people on the article talk pages that they are valid, not merely claim that they are and continue to revert. I have been working to compromise the wording, rather than just removing the ideas you are interested in. I encourage you to do the same. — Carl (CBM · talk) 23:11, 5 November 2007 (UTC)

Look, I sympathize with your position, but do not edit a proof you think is invalid. Think about it for a few days first. Your edits make it imprecise and vague, by reverting to very, very unfortunate recursion theory language, language that should have been retired decades ago. I worked hard to make it correct and precise.Likebox 23:52, 5 November 2007 (UTC)

I know that we disagree philosophically on what is central, the computer or the arithmetic. Just please, I implore you to read Godel's statements on the matter. He retired recursion theory entirely, because he felt it was superceded by Turing's work. I also know that you thought this proof was rubbish until a few hours ago. A few hours is not enough time to absorb a philosophical position you are not familiar with. I ask patience. I am sure that once you are comfortable with the philosophical position, you will feel no need to rewrite the proof.Likebox 23:58, 5 November 2007 (UTC)

I'm quite familiar with the area; I have a PhD in mathematical logic and work in computability and proof theory. Godel did believe that Turing's definition of computability was compelling. But he certainly did not retire "recursion theory" - and I'm not certain what you even mean by that. — Carl (CBM · talk) 00:03, 6 November 2007 (UTC)

And I don't have a PhD in anything! Nor do I work in anything at all.Likebox 00:30, 6 November 2007 (UTC)

The fact that I have a PhD doesn't give me special authority on the wiki, but it does mean I am quite familiar with the subject area. There's no point in addressing comments to me about my lack of understanding of the content of the articles. — Carl (CBM · talk) 00:32, 6 November 2007 (UTC)

(deindent) The fact that you have a PhD means that you think you know more. This is very annoying, because you clearly don't understand the computational proof yet. I can tell, because you keep editing it to be wrong or vague.

Actually, maybe you do understand it. I can't read your mind. Here's a test. Prove the following theorem: "There does not exist a computer program that can decide whether any other computer program runs in polynomial or exponential time on its input." You can't use Rice's theorem BTW.

The following text is copied from the talk page on GIT. It explains what I mean about Godel abandoning the recursion theory:

Copied Text

The following note in "Postscriptum", dated June 3, 1964, appears in Davis 1965:71-73. Here is where he utterly blows off recursion theory (Church 1936 and his own §9 General recursive functions) in favor of Turing 1936 and Post 1936:

"As for previous equivalent deifintions of computability, which, however, are much less suitable for our purpose, see A. Church, Am. J.. math, vol. 58(19360 pp. 356-358 (this anthology, pp. 100-102). One of those definitions is given in §9 of these lectures."

A skeptic might think he was sick of mind, but he repeats his assertion in a differnt way to van Heijenoort two years later (after working for months with van H on a new and better translation of his 1931):

"In consequence of later advances, in particular of the fact that due to A. M. Turing's work69 a precise and unquestionably adequate definition of the general notion of formal system70 can now be given, a completely general version of Theorems VI and XI is now possible.... "

" In my opinion the term "formal system" or "formalism" should never be used for anything but this notion.... I suggested certain transfinite generalizations of fomalisms, but these are something radically different from formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices." (Gödel 1963, note at end of Gödel 1931 as appears in van Heijenoort 1967, 3rd printing 1972:616)

So yes, if you take the man at his word, he says the "proper" way to construct a formal system is with mechanical devices. Period. Bill Wvbailey 01:37, 15 October 2007 (UTC) —Preceding unsigned comment added by Likebox (talk • contribs) 2007-11-06T00:40:26

Wait, are you Wvbailey, or Likebox? Anyway, I don't think I know more. Trovatore, Arthur Rubin, and David Eppstein are all extremely knowledgeable in the area, and I would be willing to defer to them if you can convince them. I am certain they each know more than I do about various things.

I am likebox, copying a quote of Wvbailey. I know Trovatore, and Arthur Rubin, and whatnot, and I am sure that I understand this proof better than all of them put together. I came up with it. They didn't. End of story.Likebox 01:26, 6 November 2007 (UTC)

Regarding the Goedel quote, the point is that he is giving a definition the effectiveness condition that he would require of a formal system. At the time, it was not quite clear what it should mean to say that a formal system is effective (or, if effectiveness is part of the definition, to say what a formal system is). — Carl (CBM · talk) 00:53, 6 November 2007 (UTC)

This quote is from 1963 from when after the dust settled. He is annoyed that people don't just use modern computing to define formal systems, instead sticking with the outdated recursive definitions which make code obscure. I agree with this quote, but not from authority. Just because in this case I think he's right. He was wrong on other things. Look, I'll probably lose this fight, but I will fight until the very end, because I believe in the cause.Likebox 01:26, 6 November 2007 (UTC)

There's no need to fight anything to the end; people are quite willing to compromise. I should point out that a proof that only the author can understand isn't really a ... proof. When you have enough experienced people who say your proof is either wrong, vague, or otherwise needs improvement, you should consider the possibility they're right. — Carl (CBM · talk) 01:33, 6 November 2007 (UTC)

Re: John Marshall image

Please reply to the message I left on my talk page. Thanks. :) --Setanta 23:00, 5 November 2007 (UTC)

Edit Warring

I know it is discouraged, but I really believe that you are obfuscating clear and correct proofs for no reason. You have reverted the clear quine proof of halting to the slightly less clear f(i,i) proof three times, with no reason.

There is no reason not to have both proofs, as I had in my rewrite. I would prefer to come to an agreement too, but the two proofs are slightly different. They are only equivalent if you understand the fixed-point theorem, which is not a given for a reader of this page. I can't stomach the idea that the halting problem will only be proved for programs with an input. That's ridiculous! In this day and age. When the proof for a program with no input just requires a quine.Likebox 01:21, 6 November 2007 (UTC)

We can talk about that. I have pointed out on the talk page why I would not call your program a quine. I would need to think about whether there is a way to do it with no inputs without the recursion theorem. — Carl (CBM · talk) 01:22, 6 November 2007 (UTC)

You need the fixed point theorem. But you're right. I was usin "quine" in the more general sense of a program with a subroutine that prints out all the code, and then goes on to do something else. That's why I called it a lemma. Please, I am sick of this fighting. I am sincere, and so are you. We should be able to agree. I'm going home.Likebox 01:29, 6 November 2007 (UTC)

I also think we should be able to agree on some compromise language for the articles. Nobody has said that the ideas you are advocating shouldn't be in the articles. The objections seem only to relate to the wording. There is a message somewhere that encourages you not to contribute unless you are willing to see your text mercilessly changed by others. You can't expect that just because you prefer a certain wording, everyone else will also like it. — Carl (CBM · talk) 04:52, 6 November 2007 (UTC)

List of basic mathematics topics

There is no style guideline, the project is basically a being driven by The Transhumanist. See a thread I've started at Misplaced Pages talk:WikiProject Lists of basic topics#Overlap with portals and other concerns for a few of the concerns that have been raised. --Quiddity 01:26, 6 November 2007 (UTC)

Edit Warring

If you keep replacing a correct proof with a vague sketch, I will continue to war. I don't want to war, but your rewrites are not acceptable in any way, and the current text, due to me, is complete and correct.

I can't believe this. I gave Misplaced Pages the gift of a book proof of Godel's theorem, and instead of thank you, I get edit warring! Do you understand how galling that is? Please bring in some neutral parties.Likebox 06:35, 6 November 2007 (UTC)