Abstract

I introduce a schematic notation for formulating bilateral natural deduction systems, and I use this notation to formulate three distinct bilateral natural deduction systems for classical logic. I then propose a new criterion for bilateral harmony that I argue is superior to the existing criteria proposed in the literature. Finally, I show, at the schematic level, that all three bilateral systems meet this criterion of bilateral harmony.