Full Idea
A notion of formal provability can be articulated in Peano arithmetic. ..This is surprisingly 'linguistic' rather than mathematical, but the key is in the Gödel coding. ..Hence we use Peano arithmetic as a theory of syntax.
Gist of Idea
A theory of syntax can be based on Peano arithmetic, thanks to the translation by Gödel coding
Source
Leon Horsten (The Tarskian Turn [2011], 02.4)
Book Reference
Horsten,Leon: 'The Tarskian Turn' [MIT 2011], p.23
A Reaction
This is the explanation of why issues in formal semantics end up being studied in systems based on formal arithmetic. And I had thought it was just because they were geeks who dream in numbers, and can't speak language properly...