It seems to me that a tag for "arithmetic logic" is missing while it concerns a significant number ($\sim 500?$) of questions, which currently have no common tag other than the very broad lo.logic —3700 questions— (while the main specific tag in this direction, peano-arithmetic —206 questions— is much too restrictive). What should be a good name, good tag excerpt for such a tag? What should be the scope of such a tag?

Initial suggestion: "arithmetic-logic" (discarded as too broad after feedback).

**Edit:**Now created taking feedback into account theories-of-arithmetic.

As was suggested, current instances of peano-arithmetic should be replaced with theories-of-arithmetic: as this can only be performed by moderators, I added the feature-request metatag.

Concretely, the request to either

(a) make peano-arithmetic a synonym of theories-of-arithmetic

or (b) merge peano-arithmetic into theories-of-arithmetic

An advantage (noticed by Martin Sleziak in this Editor Lounge discussion) of (a) is that users typing "peano" when typing tags, will be proposed theories-of-arithmetic. In option (b), I understand that after merging, the tag peano-arithmetic can be recreated.

Here I just list (maybe not comprehensively) of possibly concerned questions that have a very high number of upvotes, just to have an idea of the scope of the tag, and I list the tags they currently have.

(1) Is (Z,+,0,1,P2,P3) decidable? nt.number-theory lo.logic decidability

(2) Gödel's Incompleteness Theorem and the complexity of arithmetic peano-arithmetic nt.number-theory lo.logic

(3) What can be proven in Peano arithmetic but not Heyting arithmetic? lo.logic

(4) Which recursively-defined predicates can be expressed in Presburger Arithmetic? lo.logic nt.number-theory computational-complexity

(5) Does Taranovsky's system of ordinal notations make sense? lo.logic proof-theory ordinal-numbers

(6) Proof as a Σ₁ approximation to truth: what about higher degrees? lo.logic metamathematics

~~maybe also~~ [edit: and **not** these ones although they ring the "logic" and "arithmetic" bells]:

(7) Is being rational decidable? lo.logic decidability irrational-numbers

(8) Independence of being an integer lo.logic

(9) Are surjectivity and injectivity of polynomial functions from $\mathbb{Q}^n$ to $\mathbb{Q}$ algorithmically decidable? nt.number-theory ac.commutative-algebra algorithms polynomials computability-theory

03C62Models of arithmetic and set theory;03F30First-order arithmetic and fragments;03F35Second- and higher-order arithmetic and fragments03H15Nonstandard models of arithmetic$\endgroup$ – YCor Oct 10 '20 at 12:49