From: Aatu Koskensilta on
"|-|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
"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
"|-|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
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
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