From what I understand of one of Godel's incompleteness theorems, it involves coding wffs into numbers. Each wff corresponds to a Godel number and each Godel number gives rise to a wff. And then by using a kind of logical isomorphism between the set of wffs and N, incompleteness of any "adequate" theory is implied by the fact that computability implies definability. Is that basically right? Assuming it is... Here's my question. We use arithmetic to encode formulas. What if we used a nonstandard model of arithmetic or some other poset to encode wffs? What kind of results do we get, for instance, something about infinitary logic if our model of arithmetic has unlimited numbers that could correspond to an infinite string of OR or AND? Thanks.