Each first-order arithmetic, like PA1 for example, has non-standard models. The order-type of an enumerable non-standard model is the following: N + QxZ (natural numbers are followed by a dense order of copies of integers). When you prove that some formula is a theorem of PA1, you prove something about all the models of PA1. When you go semantic way and you show the satisfaction in the standard model (called N), you constraint your result to N only. You cannot say: I have shown that some result is satisfied in the standard model, and hence it is a theorem of PA1. And Gödel's theorem says: there is a formula which you cannot prove nor disprove in the theory (PA1 in this example). Does it make sense for you?