Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Rupert on 10 Sep 2006 19:58

Charlie-Boo wrote:
> Do we all agree that Computer Science definitely should be formalized?
>

What's the merit in being completely formal, for any branch of
mathematics? Surely it's enough to convince ourselves that we could
formalize it.

From: Chris Menzel on 10 Sep 2006 23:11
On 10 Sep 2006 14:29:13 -0700, Peter_Smith <ps218(a)cam.ac.uk> said:
>
> Chris Menzel wrote:
>
>> Can that proof be found in their Grundlagen der Mathematik? If so, do
>> you happen to know which volume?
>
> Vol2, pp. 283-340.

Thanks.

From: Charlie-Boo on 12 Sep 2006 15:14
Alec McKenzie wrote:

> In which case you must have meant to say "A formal proof that in
> every programming language there is a program that outputs
> itself".
>
> It seems clear to me that that cannot be true

Why?

> Alec McKenzie
> usenet@<surname>.me.uk

From: george on 12 Sep 2006 15:51

Rupert wrote:
> What's the merit in being completely formal, for any branch of
> mathematics? Surely it's enough to convince ourselves that we could
> formalize it.

The question is surely not so much about the merits
of that approach as the POSSIBLITY. People are not
computers. People in general just don't communicate
in a "completely formal" way. But that does NOT change
the fact that MATH *is* BY DEFINITION *completely* formal;
that is what MAKES it math.

From: george on 12 Sep 2006 15:56

Peter_Smith wrote:
> george wrote:
>
> > Godel's original proof was a formal derivation.
>
> No it wasn't. Gödel's original proof was a bit of informal
> mathematics.

The overall outline may have been informal
but this informal shell housed a huge formal
kernel. There is nothing whatsoever informal
about defining a whole bunch of predicates to
construct a Godel sentence. There is nothing
informal about an explicit Godel numbering.

First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5 6 7 8 9 10 11 12 13
Prev: Simple yet Profound Metatheorem
Next: Modal Logic