One reason I wanted to give them a name is because there’s a further structure I call a “fupomula” (/fju.ˈpɔu.mju.lə/, fyoo-POH-myoo-luh), after FUsed POwer-MULtiply-Add. As the naming suggests, this is a structure with a specified element (intended as -1) and a tetrary operator (intended as (aᵇ • c) + d), along with a predicate that calls certain elements “purely negative” and an allowance that the tetrary operator is undefined when a = 0 and b is purely negative.
From here we construct a successor function similarly to a fumula, by filling in a = b = c = -1, and define 0 as the successor of -1 and 1 as the successor of 0 just as before.
We then need axioms that say -1 and 0 are purely negative and 1 isn’t, and some generalization of the fumula axioms to account for the additional power input, plus probably a few more axioms to handle pure negativity and the power input more generally.