There's quite a large literature on understanding inductive definitions. The nLab article has some entry points.
One approach is simply to define these in terms of structural induction over the (Peano) natural numbers. Indeed, in ZFC, say, the only "primitive" forms of induction are the Axiom of Infinity and the Axiom of Foundation. Most day-to-day math doesn't rely on the Axiom of Foundation. Indeed, we can create W-types in a topos given just a natural number object. The upshot of this approach is the only form of "recursion" is recursion on naturals, any other form is derived. Showing some inductive-looking definition is meaningful or formulating admissible rules for patterns of induction more complicated than structural induction on naturals is (usually) the mathematical equivalent of what programmers call (in its only semi-ironic form) A Simple Matter of Programming. Bash enough natural number inductions and powersets at it, and it will eventually crack. In particular, induction over more structured types (e.g. W-types) can be formulated as least fixed points of some function $F$ and you can then then do natural number induction on $F^n(\emptyset)$.
In practice, it's often cleaner, clearer, and easier to use inductive types rather than some encoding of them. So some systems simply build an expressive form of inductive definition into the language itself, e.g. the Calculus of Inductive Constructions. These primitive forms of induction can sometimes go beyond the power of encodings which can call into question their justification. (Though, personally, I find it easier to philosophically justify the ability to introduce new forms of induction than to justify their encodings in typical "foundational" systems.)
Regardless of the approach, I find it much easier to find a "good" notion of induction, by using richer data types in the first place instead of just sets and natural numbers (or just being clear on the types). For reasons the earlier paragraph touched on and others, natural numbers are over-used, sometimes to absurd extents. For example, what is the type of $P$? Well, it needs a non-zero natural number, $n$, and then a sequence of exactly $n$ elements of $S$. In type theory notation, we might start to write this as: $P : (\Sigma n:\mathbb{N}_{>0}.\mathsf{Vec}\ n) \to {\dots}$ where $\mathsf{Vec}\ n$ stands for an $n$-tuple (a "vector of length $n$"). But $\Sigma n:\mathbb{N}_{>0}.\mathsf{Vec}\ n$ is just a round-about way of talking about non-empty lists or free semigroups! While the free semigroup bit may not be immediately obvious (though note also that the non-zero natural numbers are the free semigroup on one generator), the non-empty list part should be pretty clear. Describing $P$ as taking a non-empty list is a bit more humane than the presentation given. Further, non-empty lists are an inductive type with their own induction rule. In Agda, we might define non-empty lists as follows:
data NonEmptyList (S : Set) : Set where
Single : S -> NonEmptyList S
Append : S -> NonEmptyList S -> NonEmptyList S
which warrants recursive definitions of the form:
f (Single x) = g x
f (Append x xs) = h x (f xs)
for arbitrary functions g and h. In particular, something like $P$ can be defined as:
P : {S : Set} -> (S -> S -> S) -> NonEmptyList S -> S
P op (Single x) = x
P op (Append x xs) = op x (P op xs)
Though really what the quoted section is trying to do is show that given an associative operation on a set, all ways of bracketing an expression lead to the same value. To do this, it would be more natural not to start from a representation that has already quotiented away different bracketings. In other words, instead of a free semigroup, we want a free magma, better known as a non-empty full binary tree. The tree lets us explicitly represent different bracketings. (You don't need to be familiar with a bunch of esoteric algebraic structures. We're basically considering different tiny formal languages and doing induction over their syntax. Most notably, many examples are or can be factored through a term algebra.) Non-empty full binary trees are easily formulated in Agda as an inductive type:
data NonEmptyBinaryTree (S : Set) : Set where
Leaf : S -> NonEmptyBinaryTree S
Branch : NonEmptyBinaryTree S -> NonEmptyBinaryTree S -> NonEmptyBinaryTree S
with its own rule for recursive definitions:
f (Leaf x) = g x
f (Branch l r) = h (f l) (f r)
With this, we can then formulate a theorem that for all non-empty full binary trees which have the same non-empty list of leaves (in some fixed traversal) the same value is produced for any of them when we replace branches with the associative operation. I've taken exactly this approach to exactly this problem before here with a complete formalization along the lines above here. It's interesting to note that while my informal proof has a subproof that utilizes induction on naturals, my formalization doesn't even define natural numbers.
In summary, using more structured types from the get-go makes these kinds of questions easier to answer (and usually makes the problems easier to state and understand). Many cases can be viewed as structural induction over the syntax of a (very simple) formal language. More complicated cases, which I didn't discuss, are often of them form of induction over derivations of inductively-defined relations (sometimes called "rule induction", though not to be confused with the machine learning technique). There's a rich (and lively!) literature on various forms of induction including new ones like higher-inductive types. This literature will cover encodings in terms of other forms of induction or other constructs.
