This is a decommissioned version of ERA which is running to enable completion of migration processes. All new collections and items and all edits to existing items should go to our new ERA instance at https://ualberta.scholaris.ca - Please contact us at erahelp@ualberta.ca for assistance!
- 105 views
- 174 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