I&#x27;m not sure I would go that far.<p>There is a difference, but it&#x27;s not clear quite what it is.<p>For example, it becomes progressively harder to get <i>nice</i> 
(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?