Prev: Simple permutation question
Next: INFINITE LIST OF PRIME NUMBERS BY PLACEMENT BY NEW -1TANGENT MATHEMATICS
From: Aatu Koskensilta on 25 May 2010 21:33 "|-|ercules" <radgray123(a)yahoo.com> writes: > Aren't you the logician who proved that there is a formal proof for > every informal proof.... errr... with an informal proof? You're thinking of someone else. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: |-|ercules on 25 May 2010 21:59 "Aatu Koskensilta" <aatu.koskensilta(a)uta.fi> wrote > "|-|ercules" <radgray123(a)yahoo.com> writes: > >> Aren't you the logician who proved that there is a formal proof for >> every informal proof.... errr... with an informal proof? > > You're thinking of someone else. Another Aatu Koskensilta? Aatu Koskensilta wrote: All mathematical proofs can be formalised, after all. Is that a statement of incontrovertible fact, or a statement of faith? Yes. Good. Yes. That all mathematical proofs can be formalised is in a sense a triviality these days -- we simply would regard an argument we don't see how to formalise as falling short of the standard of rigour in mathematics, thinking there must be something obscure in it, that some steps must be spelled out more fully, that some detail has eluded us, and so on. This we have learned from experience, a habit mathematicians acquire by osmosis during their formative years. But it can also backed up by various general considerations the sort of which I alluded to in the posts I referred you to. One must be skeptical when the proof that all informal proofs can be made into formal proofs, is itself just an informal proof. Herc
From: Aatu Koskensilta on 25 May 2010 22:01 "|-|ercules" <radgray123(a)yahoo.com> writes: > Aatu Koskensilta wrote: All mathematical proofs can be formalised, > after all. This is hardly something I've claimed to have a proof of. It's just an observation. > One must be skeptical when the proof that all informal proofs can be > made into formal proofs, is itself just an informal proof. Why? -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: LauLuna on 26 May 2010 18:25 On May 23, 1:22 am, Herc7 <ozd...(a)australia.edu> wrote: > BONUS POINTS ~ GODEL DISPROOF > > Roger Penrose's argument is that a computer can never be as smart as a > person because you can ask the computer a question, "IS 'THIS CANNOT > BE PROVEN BY COMPUTER123' TRUE?". Humans know it is true, but > COMPUTER123 can never prove it. > > But I can equally ask Roger Penrose "IS 'THIS CANNOT BE PROVEN BY > ROGER PENROSE' TRUE?". Everyone else can prove it, but Roger Penrose > can never prove it. You are overlooking the possibility that 'this cannot be proven by Roger Penrose' express no proposition, that it be paradoxical just like the Liar sentence. Penrose will surely know that if he proves it, then it is not true; so he must know he cannot prove it; in fact he has proved that the sentence cannot be proven by Roger Penrose; but if your sentence expressed a proposition, it would express exactly the same Penrose has proved, which is impossible. So here's the difference between a computer and a human: you could never produce a paradoxical sentence about a computer's ability to prove something (because it is a well-defined mathematical fact) while you can produce such a sentence about a human's ability to prove sentences. Best.
From: Marshall on 26 May 2010 20:33
On May 26, 3:25 pm, LauLuna <laureanol...(a)yahoo.es> wrote: > On May 23, 1:22 am, Herc7 <ozd...(a)australia.edu> wrote: > > > BONUS POINTS ~ GODEL DISPROOF > > > Roger Penrose's argument is that a computer can never be as smart as a > > person because you can ask the computer a question, "IS 'THIS CANNOT > > BE PROVEN BY COMPUTER123' TRUE?". Humans know it is true, but > > COMPUTER123 can never prove it. > > > But I can equally ask Roger Penrose "IS 'THIS CANNOT BE PROVEN BY > > ROGER PENROSE' TRUE?". Everyone else can prove it, but Roger Penrose > > can never prove it. > > You are overlooking the possibility that 'this cannot be proven by > Roger Penrose' express no proposition, that it be paradoxical just > like the Liar sentence. > > Penrose will surely know that if he proves it, then it is not true; so > he must know he cannot prove it; in fact he has proved that the > sentence cannot be proven by Roger Penrose; but if your sentence > expressed a proposition, it would express exactly the same Penrose has > proved, which is impossible. Right. > So here's the difference between a computer and a human: you could > never produce a paradoxical sentence about a computer's ability to > prove something (because it is a well-defined mathematical fact) while > you can produce such a sentence about a human's ability to prove > sentences. Wrong. Marshall |