I'm not an expert in mathematical logic by far. But I understand that Godel's incompleteness theorem states that there can be some statements in an arithmatical system that are true but cannot be proven by that system. But that sounds like an implication. For part of the definition of an implication is that a true conclusion can proceed from a false premise. In other words a true statement can proceed from a false premise, or no true premise... or a true statement without something to prove it is true. So it sounds like Godel's proof might start out with things being equivalent, but there might be implication introduced somewhere so that the conclusion (about a true statement) might also precede without something to prove it, as well as might procede from something that does prove it. That would only prove that Godel intoduced implication in his proof, right?