Been a while since I studied the first incompleteness theorem, but as I understand it:
A “formal language”, or “logical system” consists of:
– An algebra: i.e. operators with predefined meaning (addition, multiplication etc).
– A set of axiomatic statements which must be self consistent (i.e. no contradictions), and not derivable from the other axioms.
Statements are then made which are consistent with the algebra, and may be shown to be consistent with the axioms (true) or in contradiction (false). There are also statements which may be made that may not be proven or disproven (e.g., if one axiom is removed and treated as a statement, it cannot be proven or disproven).
Therefore if we find a statement which is true and cannot be proven, we can simply make it an axiom.
Goedel’s first incompleteness theorem states that there are true statements which cannot be proven in any system with a finite set of axioms.
The proof is one of the best, counterintuitive and horrifically complicated bits of maths I’ve ever come across. It involves metamathematics and Peano arithmetic and amazingly is published entirely on wikipedia here.