balance between a connective's introduction and elimination potential. Thus, cut-elimination validates that the operational rules are in harmony, ensuring the logical system is both consistent and that its proofs possess good normalization properties.

Locality

Certain inference rules are local, which is a desired property. For example, consider the !-rule in linear logic:In order to check that the !-rule has been applied correctly to a certain sequent calculus step , it's not only

1.Previous
3.Next