> Things are not that simple, because you can often convert axioms to rules of inference or vice versa, without changing the set of derivable consequences.

Yes, but the derivations themselves will change.

> As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.

Yep. I'm aware of the phenomenon that a single mathematical object of type T (say, infinity-categories) may admit multiple presentations by objects of type T' (say, model categories). But, just because two objects of type T' present the same object of type T (e.g., two Quillen-equivalent categories), it doesn't mean that they are equal in all respects (e.g., the category of simplicial sets is much nicer than the category of topological spaces).

Exactly. What are axioms and what are rules of inference ends up being a distinction without a difference.

I'm not sure I would go that far.

There is a difference, but it's not clear quite what it is.

For example, it becomes progressively harder to get nice (with cut elimination and finite rule schemata) sequent calculi for richer axiomatic systems. For example I have not come across a nice (in the above sense) sequent style formalisation of ZFC set theory. Have you?

No, but why is that a problem?

It's an indication, a hint, that rules and axioms are not always completely exchangable.