Sequent Calculus vs Natural Deduction

Question

Can I prove all implication proofs like $A \to A$ or $A \to B \to A$ in both Sequent Calculus and Natural Deduction or just in one of them? So for $A \to A$ can I use the right implication rule in sequent calculus to prove it?

Answer 1

Of course this depends on the proof rules in the two systems. But the usual formulations of sequent calculus and natural deduction for classical propositional logic are equivalent: $\varphi$ is provable with a natural deduction proof with hypotheses $\Gamma$ iff the sequent $\Gamma \vdash \varphi$ is provable.

Proving $\vdash A \to A$ in sequent calculus is almost trivial. We have $A \vdash A$, and now use implication introduction.

See e.g. Relationship between sequent calculus and Hilbert systems, natural deduction, etc