Free Variable Sequent Calculi

Roger Antonsen

Master Thesis, Language, Logic and Information, Department of Linguistics, University of Oslo, 2003.

@mastersthesis{Antonsen03,
  author =   {Roger Antonsen},
  title =    {Free {V}ariable {S}equent {C}alculi},
  year =     2003,
  month =    {May},
  address =  {Language, Logic and Information, Department of Linguistics},
  school =   {University of Oslo},
  publisher = {University of Oslo}
}

Sammendrag

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.