Given a foundation of first order logic how would you define inductive predicates like testing if a natural number is even?
From my background in type theory I am aware you can compile down pattern matching with recursion to use of induction principles (possibly also with axiom K.) So I think as an example for Peano arithmetic you would compile down inductive predicates to use of a recursor predicate axiomized as something like
$$\mu(P, \phi. Q, \text{O}) \iff P$$ $$\mu(P, \phi. Q, \text{S}(x)) \iff [\phi := \mu(P, \phi. Q, x)]Q$$
But this seems like a very constructive approach. Are there better or cleaner ways to do this sort of thing perhaps with classical first order logic?
I am also aware of impredicative encodings but those require higher order logic.