A Gentzen-style sequent calculus, GA4, for a first-order extension of Avron’s self-extensional paradefinite four-valued logic is introduced. Avron’s logic is known as a unique self-extensional extension of Belnap–Dunn logic. GA4 yields two new Gentzen-style sequent calculi, \(\hbox {GCL}_1\) and \(\hbox {GCL}_2\) , for first-order classical logic by introducing some new inference rules or initial sequents. \(\hbox {GCL}_1\) is obtained from GA4 by adding the rules of explosion and excluded middle, which correspond to the principle of explosion and the law of excluded middle. \(\hbox {GCL}_2\) is obtained from GA4 by adding initial sequents that correspond to the same principle and law. A theorem proving the equivalence among \(\hbox {GCL}_1\) , \(\hbox {GCL}_2\) , and Gentzen’s sequent calculus LK for first-order classical logic is established. The cut-elimination, contraposition-elimination, and completeness theorems for GA4, \(\hbox {GCL}_1\) , and \(\hbox {GCL}_2\) are proved. The self-extensional properties of GA4, \(\hbox {GCL}_1\) , and \(\hbox {GCL}_2\) are derived using the contraposition-elimination theorems.
