Yes, check out the Paris-Harrington theorem's use of indicators as one way to do this for a specific kind of Ramsey theorish combinatorial claim. It's kinda a tough slog but it's a really explicit construction of a model of PA which makes a true (in N) combinatorial claim false.

Generally speaking, however, there is no general constructive method to produce such models

Yes, check out the Paris-Harrington theorem's use of indicators as one way to do this for a specific kind of Ramsey theorish combinatorial claim. It's kinda a tough slog but it's a really explicit construction of a model of PA which makes a true (in N) combinatorial claim false.

Generally speaking, however, there is no general constructive method to produce such models. However, I believe the indicator method from the Paris-Harrington theorem can be extended to work for cases where the issue is the provable totality of functions with a certain rate of growth.

Yes, check out the Paris-Harrington theorem's use of indicators as one way to do this. Generally speaking, however, there is no general constructive method for all types of true but unprovable formulas that I'm aware of.

Yes, check out the Paris-Harrington theorem's use of indicators as one way to do this for a specific kind of Ramsey theorish combinatorial claim. It's kinda a tough slog but it's a really explicit construction of a model of PA which makes a true (in N) combinatorial claim false.

Generally speaking, however, there is no general constructive method to produce such models