To: EPS who wrote (394 ) 10/5/1998 9:52:00 PM From: ahhaha Read Replies (2) | Respond to
Moreover, we believe they are true intuitively, but no effective decision procedure exists to determine whether they are true. That is, machines can't be programmed to necessarily find proofs. It is a game we mathematicians play. We start with a sentence within a system that we believe is true. The game is to derive the sentence from axioms of the system. We may never find a proof, but we may always be convinced of its truth though it remains undecidable as to whether a proof exists. Godel showed that you could always create a sentence within an inherently undecidable theory that effectively asserted its own falsity, a sentence built from intuitively true axioms and derived consequences of arithmetic. Some theories are decidable, all truths are provable, and some aren't, there exist truths which are true but not provable. You never know whether a sentence in a undecidable theory is true until you find a proof, show its provability, and thus its truth within the system.
