Van Plato's book seems interesting! I see that it has a chapter on natural deduction and sequent calculus. I found the focus on introduction and elimination rul

Van Plato's book seems interesting! I see that it has a chapter on natural deduction and sequent calculus. I found the focus on introduction and elimination rules in natural deduction always somewhat mystifying, and wondered about what exactly natural deduction is. As I discovered just in the last few weeks, even if, like me, you don't know anything about the proof theoretic foundations of natural deduction and sequent calculus, they pop up naturally as proof systems for abstraction logic (AL): natural deduction is the proof system if your truth values form a complete lattice, and sequent calculus is the proof system if your truth values form even a complete bi-Heyting algebra. Note that in AL, there are no a-priori constants (such as ∧ or ⇒), so there are also no a-priori rules for elimination and introduction, but just the essence of natural deduction and sequent calculus. See http://abstractionlogic.com http://abstractionlogic.com for the least klunky presentation of AL to date.