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

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?