Thanks, Elorch. I have been looking into constructive set theories for a little while and I will continue to. Your idea about the law of the excluded middle is also interesting.
As an aside, it is interesting to see solutions to set theoretic word paradoxes, such as the solution to the barber paradox (the barber is a woman, although that is sort of cheating), and the Cretan paradox (most liars do not lie consistently).
Following on from the thread concerning Godel's first incompleteness theorem, looking at the proof made me think about how the technique used to create a self-referential statement could be used to implement the classical "Cretan liar's paradox". [Incidentally, I suspect Paul misunderstood this 4th century work when he misrepresented it in Titus 1:12 ""One of themselves, even a prophet of their own, said, the Cretans are always liars, evil beasts, slow bellies." ]
Ironically, I would guess that Godel probably did this first and then later used an adaptation of the idea to prove the first incompleteness theorem.
Using some of the machinery of the incompleteness proof, it is easy to create a statement F(n) that says: "statement n is false" where n is the unique natural number for another statement. We can add a free variable to this statement to give a statement F(x, y) s.t. if y is substituted for x, it says "statement y is false". If the Godel number of F(x,y) is p, the statement F(p, p) is a self-referential statement saying "this statement is false".
So is the statement F(p,p) true or false? It is easy to see that if it is true then it is false, but if it is false then it is true, so if it has either value the theory is inconsistent. This would be bad news as this would mean number theory and the whole of mathematics would be inconsistent.
The solution is that the statement simply has no truth value - it is indeterminate. There is certainly no proof within the theory that it is true and no proof that it is false (otherwise the system would be inconsistent). Strangely, it can be proved that since the statement is indeterminate, we can formally extend the system to another (relatively consistent) system where this statement is chosen to be either true or false as an axiom (like with the axiom of choice or the continuum hypothesis), but I believe the statement could not be interpreted in the same way in this artificial system.
To me this example puts the law of the excluded middle on very shaky ground, as it means that in any system powerful enough to deal with number theory, there are statements that are indeterminate within the theory, but also have no valid truth value that makes sense (which seems more awkward than statements which are true but unprovable).
The solution to this discomfort may lie in constructivism, where self-reference may be avoided, in the same way as in axiomatic set theory, sets may never be members of themselves, or members of sets that are members of the original set, or so on. Maybe even more safe is constructive set theory. Constructivism may avoid awkward self-reference (or then again, it may not).