Definition 9.2 (ACF with characteristic). For n≥1, let χn be the sentence

1+⋯+1⏟n times=0.

Set

ACF⁡0=ACF⁡∪{¬⁡χn:n∈ℕ}ACF⁡p=ACF⁡∪{χp}(for p a prime)