Question

There are several methods for producing non-standard models. For example, via Henkin's method, via ultraproducts, or via cuts of other models. However, some of these methods would not work very well for a Π₁ statement like Goldbach's Conjecture. Indeed, these statements reflect to the standard model so if Goldbach's Conjecture is true in any model of arithmetic then it must be true in the standard model.

Nevertheless, one could try to produce a model where Goldbach's Conjecture is false in order to gather evidence against the conjecture. Henkin's method is closest to the one you describe. It proceeds by adding new constants c₀,c₁,... to the language each of which is assigned to witness an existential quantifier in an infinite process by which one decides the truth of all sentences of the language. To start the process, we might decide that c₀ is an even integer which is not the sum of two odd primes. To witness this, we might declare later on that c₀ = 2c₁₇ to make sure that c₀ is even. Then for every term t that arises along the way, we will add witnesses to the fact that either t > c₀, or one of t and c₀ - t has a nontrivial factor, whichever does not contradict the current state of affairs. And so on for all sentences, including those which are unrelated to Goldbach's Conjecture. With careful bookkeeping, if our axioms are not contradictory, this will succeed in producing a term model of our axioms. (At the end, you need to mod out by the equivalence relation of provable equality, but those details are best left to the standard logic textbooks.) Unfortunately, without extraordinary insight, we have basically no grasp of what the final structure will be like.

There are more direct methods that work for weaker subsystems of arithmetic. For example, Shepherdson's method is highly successful in producing models of open induction. I described this method in an earlier answer. In fact, Macintyre and Marker [Primes and their residue rings in models of open induction, MR1001418] have refined Shepherdson's method to produce some very curious non-standard models of open induction. In one such model, all non-standard primes are congruent to 3 mod 4, and in another every nonstandard even integer is the sum of two primes. Since open induction is very, very weak one cannot draw many conclusions from this, but the models in question are very concrete.