Am i wrong or does 'Well here's what Godel proved: There's no way to really know whether or not any theory is consistent.' completely ignore Gödel's completeness theorem for first order logic.
The Completeness Theorem (in one of its equivalent forms) says that every consistent first-order theory has a model, linking syntax and semantics. It doesn't tell you any thing about how you would go about justifying that a theory is consistent.
People hoped that some logical system capable of formalizing real mathematics would be able to justify its own consistency. Godel's Incompleteness Theorem (and stronger, related results) imply that any system capable of formalizing real mathematics (or even a very weak subset of it) can not justify its own consistency, requiring an appeal to a stronger system. Obviously, that raises the obvious question of why that stronger system is consistent. There are constructive proofs (due to Godel himself, Gentzen, and others) of the consistency of Peano Arithmetic, but by the Incompleteness Theorem they must all be non-finitary in some fashion, no matter how slight.
However, there are some limits to this understanding of Godel's Incompleteness Theorem. There are theories that are strong enough to prove (and perhaps more importantly, state) their own consistency but not strong enough to formalize diagonalization. If PA is consistent, then there is a theory that can state and prove its own consistency as well as the consistency of PA. The trick is that provability can be formalized on the basis that subtraction and division are total functions, whereas diagonalization requires addition and multiplication to be total functions. These theories can prove that subtraction and division are total functions, but not addition and multiplication.
I don't think there is a contradiction, but someone please correct me if I'm wrong. Godel's theories are something I've recently begun trying to wrap my head around.
Godel's completeness theorem proves the equivalence of logical implication and deducibility. Logical implication being the formal definition of what it means for a collection of sentences (axioms) to logically imply another sentence (theorem); deducibility being the method with which a working mathematician would like to use to show logical implication (i.e. any proof you've ever read in a mathematical textbook).
Incompleteness, on the other hand, shows that there are some true sentences that cannot be deduced from any set of axioms (and therefore, by completeness, are not logically implied by any set of axioms).
This is my understanding after having spent a few weeks reading Enderton's "A Mathematical Introduction to Logic." If I am misunderstanding this, I would love input (so please comment). Godel's theorems are something I'm very anxious to wrap my head around.
Yeah. It should be something like "any sufficiently strong theory". But that's still a justifiable simplification. Other parts of the explanation are totally incomprehensible to someone who doesn't already know what's he talking about.