I wonder if a slightly higher level explanation might help. If any real mathemeticians are around, please correct me if I'm inaccurate. An alphabet is a set of

I wonder if a slightly higher level explanation might help. If any real mathemeticians are around, please correct me if I'm inaccurate. An alphabet is a set of symbols. Symbols can be combined by the operation of concatenation to form strings. Strings either satisfy a property of being a syntactically valid or not. Let those strings that satisfy the property of syntactic validity be called sentences. The set of all sentences that are syntactically valid is called a language. I think the trick to understanding this particular theorem of Gödel is to know that in such formal systems there is a difference between semantic consequence (which is about truth) and syntactic consequence (which is about proof). A sentence is provable if it is derivable from other sentences of the language by applying certain syntactic transformation rules (inference rules) to them. On the other hand, a sentence of the language is logically valid if it is true under all possible interpretations (sorting out what this means is what model theory does for you.) If every sentence that is provable is logically valid then the system has the property of soundness. If every sentence that is logically valid is provable then the system has the property of completeness. The systems are designed so that we only need to do this syntatic manipulation, much like algebra, to produce proofs, but we always have a map giving us the meaning of any given sentence. This is in fact what "formal" means in this context: that in proofs we're only looking at the form (syntax) of the sentences and not the interpretation/meaning (semantics) of any of the sentences. To re-iterate: Something can be true but not provable, i.e. in any incomplete system. Something can be provable but not true, i.e. in an unsound system. If everything that can be proven is true, then the system is sound. If everything that is true can be proven, then the system is complete. First-order logic is sound and complete. Now when a system is extended with artihmetic, then due to Gödel numbering, it is suddenly capable of a form self-reference. This allows a system to state metatheorems about itself. If it can do this, then it is necessarily incomplete. In particular, it cannot prove its own consistency.