David, Goedel showed that there are infinitely many undecidable propositions in first-order logic. The example you cited, “this statement cannot be proved”, cannot be stated in FOL because it requires metalanguage -- a method for talking about statements. FOL, as it is usually defined, does not contain any operator or method that would enable any statement to talk about any statement of any kind, not even about itself. Therefore, that is not one of the statements that Goedel was proving theorems about. Puzzles that contain metalanguage were debated by the Greeks thousands of years ago. A famous example is "All Cretans are liars." That statement was uttered by a Cretan. If that statement is false because it was uttered by a Cretan, it would imply that the Cretan who said it was not a liar. But that would imply that the statement is true. John ---------------------------------------- From: "poole" <poole(a)cs.ubc.ca> Goedel’s theorem does not “show that certain very complex propositions stated in first-order logic are undecidable”. The proposition is “this statement cannot be proved” If it is true, the logic is incomplete. If it is false the logic is unsound. (It doesn’t look very complex to me. I doubt that "no logician had ever written or encountered" this proposition, as other similar “paradoxes" were common). The only way to get around Goedel’s theorem is to make the logic too weak to state this. What Goedel proved was that any logic that can represent arithmetic can represent this. His proof was complicated because he had to invent programming and therem proving. Now the proof should be straightforward as we can assume that computers and theorem provers, and a computer is just a big arithmetic operation (the memory of a computer is just a large integer). I agree with the comment on OWL. Restricting a logic to be decidable, does not make it efficient, it just means you can state less. There are things you just cannot state. David