Re: sinking feeling

[David Matuszek <dave@VFL.PARAMAX.COM>]

Philip Delaquess writes

> Y'know, friends, I've been reading the recent debate about 'any' with
> a mixture of amusement and confusion for what seems like weeks now,
> and this morning I got this kind of a sick, sinking feeling. It seems
> to me that y'all are trying to codify a system that is 1) complete,
> 2) consistant, and 3) capable of describing itself. Does the name
> Kurt Godel ring any bells? Can somebody convince me that you're not
> trying to do the impossible?

Not to worry.  What Goedel actually proved (serious oversimplification
alert) was that if you have a formal system that is sufficiently
expressive so that you can state, within the system, the proposition
that the system is consistent, then you will be able to prove this
proposition within the system if and only if the system is not in fact
consistent.

In other words, you cannot prove, within a consistent formal system,
that the system you are in is consistent.  Or, if you can prove it,
it's because it isn't true (the system is broken, so you can prove
all kinds of garbage in it, including consistency).

Russell and Whitehead set out to prove that mathematics is consistent.
They failed.  Mathematics includes arithmetic, of course.  Arithmetic,
it turns out, is sufficiently expressive to make the claim that
arithmetic is consistent.  (Figuring out how to use things like "add"
and "subtract" to say this is the really clever part, and constitutes
about half of Goedel's proof.)  Goedel basically said, hey, it's a
good thing you failed, guys!  Nowadays nobody much tries to prove
mathematics is consistent--but most of us still take it for granted
that arithmetic really is consistent.  (I have my doubts -- I'm quite
serious -- about calculus, but what the heck, it works.)

So even if Lojban is complete (whatever THAT means), consistent
(extremely unlikely, given its size and the difficulty of building
even small consistent systems--but still a very worthy goal), and
capable of describing itself (easy), we don't have to worry until some
Lojbanist claims to have used Lojban to prove Lojban is consistent.

  -- dave@vfl.paramax.com -- If my header says otherwise, it lies.

In memoriam:  The Space Age, 1969-1972.