Free Variable Sequent Calculi
Master Thesis, Language, Logic and Information, Department of Linguistics, University of Oslo, 2003.
This is a thesis about free variable sequent calculi for first-order languages without equality. A brief summary: Chapter 1 and 2 are mainly background material. Chapter 3 introduces a way of representing and reasoning about relations between inferences and sketches a method for syntactical soundness proofs; more precisely, soundness results from one calculus can be transferred to another calculus by means of proof transformations. Chapter 4 investigates a new free variable sequent calculus with 'uniform variable splitting'. This calculus is an attempt to generalize and sharpen the idea of universal variables and the 'splitting by need'-method. There is also an appendix containing a draft of the paper 'A free variable sequent calculus with uniform variable splitting' written by Arild Waaler and Roger Antonsen.