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?
$\begingroup$
$\endgroup$
1
-
1$\begingroup$ Yes; both $A \to A$ and $A \to (B \to A)$ are valid propositional formulas and thus they are provable with every proof system that is complete. $\endgroup$– Mauro ALLEGRANZAOct 26, 2021 at 8:47
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
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
answered Oct 18, 2021 at 19:27
-
$\begingroup$ is there technically an infinite numbers of proofs for A→A or is there just one? $\endgroup$ Oct 18, 2021 at 20:35
-
$\begingroup$ @ryanjones in mathematical logic except for some language with ground terms only such as Herbrand logic an entailed sentence may have infinite proofs, usually we require finite proofs for most propositional and first order logics you encounter. Clearly here you can have finite proof with only 2 steps needed (axiom of identity + implication right rule) in sequent calculus, similar in ND systems. $\endgroup$ Oct 19, 2021 at 17:45