Abstract
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 univeral 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. (A final version of this paper will appear later.)