If you taboo one-predicate 'matter', please specialize the two-place predicate (X matters to Y) to Y = "the OP's subsequent use of this article", and use the resulting one-place predicate.

I am not worried about apparent circularity. Once I internalized the Lowenheim-Skolem argument that first-order theories have countable "non-standard" models, then model theory dissolved for me. The syntactical / formalist view of semantics, that what mathematicians are doing is manipulating finite strings of symbols, is always a perfectly good model, in the model theoretic sense. If you want to understand what the mathematician is doing, you may look at what they're doing, rather than taking them at their word and trying to boggle your imagination with images of bigness. Does dissolving model theory matter?

There's plenty of encodings in mathematics - for example, using first-order predicate logic and the ZFC axioms to talk about second-order logic, or putting classical logic inside of intuitionistic logic with the double negation translation. Does the prevalence of encodings (analogous to the Turing Tarpit) matter?

Formal arguments, to be used in the real world, occur as the middle of an informal sandwich - first there's an informal argument that the premises are appropriate or reasonable, and third there's an informal argument interpreting the conclusion. I understand the formal part of this post, but I don't understand the informal parts at all. Nonstandard (particularly countable) models are everywhere and unavoidable (analogously Godel showed that true but unprovable statements are everywhere and unavoidable). Against that background, the formal success of second-order logic in exiling nonstandard models of arithmetic doesn't seem (to me) a good starting point for any third argument.