The thrust of Godel's argument for our purposes is that it shows us how to go beyond any given set of computational rules that we believe to be sound, and obtain a further rule, not contained in those rules, that we must believe to be sound also, namely the rule asserting the consistency of the original rules. The essential point, for our purposes, is: belief in soundness implies belief in consistency. We have no right to use the rules of a formal system F, and to believe that the results that we derive from it are actually true, unless we also believe in the consistency of that formal system. (For example, if F were inconsistent, then we could deduce, as TRUE, the statement '1=2', which is certainly not true!) Thus, if we believe that we are actually doing mathematics when we use some formal system F, then we must also be prepared to accept reasoning that goes beyond the limitations of the system F, whatever that system F may be.