This decommissioned ERA site remains active temporarily to support our final migration steps to https://ualberta.scholaris.ca, ERA's new home. All new collections and items, including Spring 2025 theses, are at that site. For assistance, please contact erahelp@ualberta.ca.
- 118 views
- 199 downloads
Classical first-order logic
-
Classical first-order logic
-
- Author(s) / Creator(s)
-
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
-
- Type of Item
- Chapter