Classical first-order logic

• Classical first-order logic

• Author(s) / Creator(s)

  • Katalin Bimbó

• The first sequent calculus, LK is the example after which many other calculi have been fashioned. We describe this calculus, prove its equivalence to the axiom system K, and provide a sound and complete interpretation too. A major part of Section 2.3 is a presentation of the proof of the cut theorem using triple induction. We avoid the detour via the mix rule by using a suitable formulation of the single cut rule, by adding a new parameter to the induction, and by defining anew the rank of a cut. Although we do not go through all the details of this proof, we hope that sufficiently many cases are included so that the structure of the proof becomes completely clear. Later on, we will provide more condensed proofs of cut theorems or simply state cut theorems with reference to this proof, possibly, with modifications.

• Date created

  2020-06-01

• Subjects / Keywords

  • 2-valued logic, admissibility of the cut rule, axiomatic calculus for FOL, contraction measure, sequent calculus for FOL, single cut rule

• Type of Item

  Chapter

• DOI

  https://doi.org/10.7939/r3-1f3n-8288

• License

  Attribution-NonCommercial-NoDerivatives 4.0 International