Add the type ℚ, ℚ[≠0] = { x : x∈ℝ ∧ x≠0 }, reuse the symbols and operations of PA and the operations of ℤ (ℝ is an ordered field).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℝ (x+y∈ℝ).
[closure] ∀x,y∈ℝ (x⋅y∈ℝ).
[closure] ∀x,y∈ℝ (x-y∈ℝ).
[closure] ∀x∈ℝ ∀y∈ℝ[≠0] (x/y∈ℝ).
