Gentzen systems, with their introduction rules on the left and the right, have very special properties which are useful in studying logics. Since connectives are always introduced in a proof (read from top to bottom) proofs never lose structure. If a connective does not appear in the conclusion of a proof, it will not appear in the proof at all, since connectives cannot be eliminated.