paradoxes and intuitionist logic

[iepos@tunes.org]

> Epimenides Paradox, also known as the liar paradox or the paradox of 
> self-reference is attributed to Epimenides, a Cretan who made one immortal
> statement: "All Cretans are liars." A sharper version is simply "This
> statement is false."
> 
> This paradox is a result of self-reference. And the issue of self-reference
> within an axiomatic formal calculus and its consequences have been laid out
> neatly by Kurt Godel and are formalized by his infamous result: Godel's
> Theorem. And what Godel showed was that any formal system is a member of one
> of two groups: either less complex than number theory, or at least as
> complex as number theory. And here's the rub: if a formal system is less
> complex than number theory, then it won't be very useful, and if it is as
> complex as number theory, then it is incomplete because of the system's
> ability to refer to itself.
> 
> So it gets you coming and going; either way your formal system is incomplete
> because there are always statements, both true and false, that cannot be
> proven either way within any particular formal system.

yes. i've heard of godel's theorem, but i'll admit i don't really understand 
it. it is clear to me that if a system admits self-referential sentences
and provides a way for the system to talk about its own theorems, then
there will either be unprovable true sentences or provable untrue ones:
the sentence with the meaning "this sentence is unprovable" will be
such a sentence. however, i don't quite see how this problem can happen
in simple number theories, ones that don't even provide a way for
self-referential sentences much less a way to reference the system's own
theorems. sure, one could extend the system by assigning arbitrary
numbers to represent the system's theorems and proofs ("godel numbering"?)
but this seems to be quite an extension to me, and it results in a new
system that deserves to be incomplete. but anyway, i must be missing something,
because godel's result seems to be well-respected. i'd be interested
in seeing a simple victim number theory.

> 
> I definitely suggest you read _Godel, Escher, Bach_ for a lengthy discussion
> of essentially this issue.

hmm. well, i've heard of the book but never read it. from what i've heard,
it is entertaining but doesn't really give you much specific information...
but i might read it anyway someday ...

anyway. self-reference is an interesting thing. it seems to have the
surprising quality of popping out of nowhere when you least expect
it.... like the Y combinator, which can be built from simple innocent bases.

anyway, i'm still thinking on my original question (well, i guess it
was sort of a question): what are some good ways of formulating the
class of statements (propositions)? it seems that some things don't
have the property of the deductive theorem, and some don't have the
excluded middle... well, saying that they do not is not correct, i think;
perhaps it would be more correct merely to say that assuming the
properties for some things leads to problems. anyway, i'm sort of
interested in the relationship between the deductive theorem and the
excluded middle...

> 
> -Ken Evitt
> 

well... thanks for your reply.
i'm still interested in hearing from others.

i really should start working on that system i mentioned
a while ago. i'm horrible about starting projects and then
not doing anything at all with them (:-)). actually, i've
been doing some thinking about how I'll formalize the
notion of time. i can't admit a word such as "now" into the
system, because such a word would necessarily take on different
meanings in different contexts, which would ruin the purity
of the language; yet, doing things without such a word is
tricky. anyway, the world will be modeled as an ordered set of
states ("times", in a high-level sense, i'm not talking about a sequence
of machine states); this may not really be a good model, given discoveries
by Einstein (which i know quite little about), but i think it
will do. this is meant to be a practical system... that is,
i mean to actually implement it sometime, not just philosophize
about it forever.

- iepos