Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: H. J. Sander Bruggink on 3 Oct 2006 14:47 Charlie-Boo wrote: > H. J. Sander Bruggink wrote: > >> your definition was wrong, because the last line >> of the proof is *not* the sought after theorem. Thanks for >> the clarification. > > WADR, I think you're still confused. ... [snip] > ... So the theorem can be at either the beginning or the end. No, *you* must be confused. Because now you admit that your definition that the theorem is at the end is wrong. >> you *claim* that the language is Turing complete. >> Care to give a proof of that? > > 1. For any program: > a. if it enumerates a set, then it is of the form: > FOR (loop code) WRITE(x) > b. if it decides a set, then it is of the form: > IF (decision code) WRITE(TRUE) > WRITE(FALSE) > c. if it computes a function, then it is of the form: > SET X=(function code) WRITE(X) > qed Congratulations. You replaced one unsubstantiated claim by four others. Do you think this constitutes a proof? LOL. > >>>> I have seen systems translate a proof to a program. > > Curry-Howard is not based on proofs and it is not automatic. Curry-Howard is not based on proofs??? You really don't understand it, do you? Don't you think it is a good idea to actually understand it before claiming it's rubbish? > They call > it proofs, but it is not generated. Not generated??? By a computer program, you mean? So now you imply that your "system" does generate its proofs? Now, can we see this "proof generator" of yours, then? (Oh no, wait, we've been there before. You can't substantiate your claims because this proof generator of yours doesn't exist. You admitted that already.) > They don't create programs from > specifications. They (claim to) create programs from pieces of code > that the user types in. You're typing nonsense, Charlie. > It isn't proving anything. It isn't > automatic. Right. Neither is proving in your system, is it? [snip] > Trying to compare a Computationally Based Logic to a Proposition Based > Logic shows that you don't understand one or the other (inclusive > or.) LOL. Everything you say shows that you don't have a clue what you're talking about. Propositional logic? Who's talking about that? > >> Did you already implement your system, btw? (No, I bet not.) > > Yes. Come on. Show it. Substantiate your claims. Do yourself what you're asking of others. [snip more lies from Charlie] > >> You are only making a fool of yourself. Just look at >> the example I pointed you to in the "Turing vs Godel" >> thread. > > Liar, you never gave me a pointer. (You didn't even sell me one.) "Turing vs Godel" thread. You can do your own homework from there. Use Google. But anyway. Show this program synthesis system of yours or just shut up and admit you're a liar. [snip] groente -- Sander
From: Charlie-Boo on 3 Oct 2006 18:00 Bill Hale wrote: > In article <1159899594.291222.133100(a)i3g2000cwc.googlegroups.com>, > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > > > http://www.arxiv.org/html/cs.lo/0003071 > > > > > In the section "IV. An example from Number Theory", you give the > > > following definition: > > > > > > 4. MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a) a * b > a > > > > > > This doesn't seem to be a definition of MUL(a,b,c). I find this > > > confusing and misleading. > > > > > > Bill Hale > > > > Thanks for the interest. DEF 4 states that MUL(a,b,c) is equivalent to > > MUL(a,b,c) ^ ~LT(c,a), but is not meant to capture enough information > > to completely define MUL. > > But, you are not saying that the two are equivalent. You are saying that > the two are equivalent *by definition*. > > This is confusing. You are misusing the word "definition". (I am actually calling them DEF, for what it's worth.) That is debatable in this case, but think of the reasons that we might know that two wffs (relations) are equivalent. The DEF in the paper show a number of scenarios, such as: 1. P , ~~P 2. P^Q , Q^P 3. P(a) , (eA)P(A)^EQ(A,a) 4. FAC(a,b) , (eA)MUL(A,a,b) 5. HALT(a,b) , YES(a,b)vNO(a,b) What would you call each of these? I think it is natural to say that these are true by definion of ^, EQ, FAC, MUL, HALT etc. What would you suggest as a better name? I think that DEF (definition) is the best single general concept for these. After all, doesn't everything boil down to the definitions? C-B > Bill Hale
From: Bill Hale on 3 Oct 2006 20:48 In article <1159912824.883725.67590(a)h48g2000cwc.googlegroups.com>, "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Bill Hale wrote: > > In article <1159899594.291222.133100(a)i3g2000cwc.googlegroups.com>, > > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > > > > > http://www.arxiv.org/html/cs.lo/0003071 > > > > > > > In the section "IV. An example from Number Theory", you give the > > > > following definition: > > > > > > > > 4. MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a) a * b > a > > > > > > > > This doesn't seem to be a definition of MUL(a,b,c). I find this > > > > confusing and misleading. > > > > > > > > Bill Hale > > > > > > Thanks for the interest. DEF 4 states that MUL(a,b,c) is equivalent to > > > MUL(a,b,c) ^ ~LT(c,a), but is not meant to capture enough information > > > to completely define MUL. > > > > But, you are not saying that the two are equivalent. You are saying that > > the two are equivalent *by definition*. > > > > This is confusing. You are misusing the word "definition". > > (I am actually calling them DEF, for what it's worth.) That is > debatable in this case, but think of the reasons that we might know > that two wffs (relations) are equivalent. Two wffs might be equivalent because the second wff is defined to be the first wff. Or, two wffs might be equivalent because the second wff is proved to be equivalent to the first wff. >The DEF in the paper show a > number of scenarios, such as: > > 1. P , ~~P This would be a theorem or an axiom. It would not be a definition. > 2. P^Q , Q^P This would be a theorem or an axiom. It would not be a definition. > 3. P(a) , (eA)P(A)^EQ(A,a) This would not be a definition. > 4. FAC(a,b) , (eA)MUL(A,a,b) This should be a definition. > 5. HALT(a,b) , YES(a,b)vNO(a,b) I haven't read what you mean by this yet. > What would you call each of these? I think it is natural to say that > these are true by definion of ^, EQ, FAC, MUL, HALT etc. You are now giving another meaning for "true by definition", or at least using it in a third meaning. "2. P^Q , Q^P" is true by definition does not mean the same as "2. P^Q , Q^P" is true by definition of "^". Is this what you are saying: 2. P^Q , Q^P since it is true by definition of ^ That is not a definition. I am confused. You need to explain more. I would say the following: "4. FAC(a,b) , (eA)MUL(A,a,b)" is not true by the definition of FAC and MUL. "4. FAC(a,b) , (eA)MUL(A,a,b)" is true because it is the definition of FAC. > What would you suggest as a better name? Fact. Basic fact. But, if it is not a definition, then you need to prove it or reference where it is proved. It seems like you are saying that it doesn't need a proof since it is a definition. This would require that CBL needs more than just 8 or so axioms that you are claiming. > I think that DEF (definition) > is the best single general concept for these. No. Definitions have certain requirements that you are not following. You can't define Q^P to mean P^Q for example. > After all, doesn't > everything boil down to the definitions? No. Definitions are not needed: they are just a convenience. Bill Hale
From: Steven Zenith on 4 Oct 2006 00:25 Charlie-Boo wrote: > Why do you think that Prof. Gio Wiederhold of Stanford invited me to > represent the United States as a Computer Scientist in a cultural > exchange with the People's Republic of China under the People to > People program? He knows about the coming war and figures you have destructive potential or he was trying to politely get rid of you? Just guessing. With respect, Steven
From: Steven Zenith on 4 Oct 2006 00:53
Charlie-Boo wrote: > ... And you claim that people want to give you awards but > you're too busy to accept them? What was the award for, Volunteer of > the Week? What on earth are you talking about? Your lack of sincerity and ad hominem attacks are transparent and unnecessary. With respect, Steven |