Proof theory

Herman Ruge Jervell

Product information

Author: Herman Ruge Jervell
ISBN: 9783832589998
Publisher: Logos Verlag
Publishing date: 2013-01-16
Related year (electronic): 2013
Pages: 131
Package: Mathematik/Informatik 2019 [1990]

P-ISBN: 9783832533038

Cite this publication as

Herman Ruge Jervell, Proof theory (2013), Logos Verlag, Berlin, ISBN: 9783832589998

52
accesses
2
quotes

Description / Abstract

In proof theory we investigate the objects used for computations and arguments in computer science and mathematics. Our starting point is the classical analysis given by Gerhard Gentzen in the 1930s. We develop this further using a new theory of ordinal notation and connecting this with combinatorics on finite trees.

Table of content

  • BEGINN
  • 1 Direct arguments
  • 1.1 Auxiliary constructions . . . . . . . . . . . . . .
  • 1.2 Sequent calculus . . . . . . . . . . . . . . . . . .
  • 1.3 Cut elimination . . . . . . . . . . . . . . . . . . .
  • 1.4 epsilon-calculus . . . . . . . . . . . . . . . . . . . . . .
  • 1.5 Other systems . . . . . . . . . . . . . . . . . . . .
  • 1.6 Infinitary proofs . . . . . . . . . . . . . . . . . .
  • 2 Gentzen games
  • 2.1 Gentzen trees . . . . . . . . . . . . . . . . . . . .
  • 2.2 Syntactic moves . . . . . . . . . . . . . . . . . . .
  • 2.3 Strong termination . . . . . . . . . . . . . . . . .
  • 3 Ordinals
  • 3.1 Well Orderings . . . . . . . . . . . . . . . . . . .
  • 3.2 Arithmetical operations . . . . . . . . . . . . . .
  • 3.3 Delayed decisions . . . . . . . . . . . . . . . . . .
  • 4 Transfinite induction
  • 4.1 Transfinite induction . . . . . . . . . . . . . . . .
  • 4.2 Ordinal bounds . . . . . . . . . . . . . . . . . . .
  • 4.3 Bounds for provable transfinite induction . . . .
  • 4.4 Arithmetical systems . . . . . . . . . . . . . . . .
  • 5 Quantifiers
  • 5.1 Skolem and quantifiers . . . . . . . . . . . . . . .
  • 5.2 G¨odels interpretation . . . . . . . . . . . . . . . .
  • 5.3 The proof . . . . . . . . . . . . . . . . . . . . . .
  • 5.4 Discussion . . . . . . . . . . . . . . . . . . . . . .
  • 5.5 Spectors interpretation . . . . . . . . . . . . . . .
  • 5.6 epsilon-calculus . . . . . . . . . . . . . . . . . . . . . .
  • 6 Finite trees
  • 6.1 Ordering trees . . . . . . . . . . . . . . . . . . . .
  • 6.2 Deciding the ordering . . . . . . . . . . . . . . .
  • 6.3 Embeddings . . . . . . . . . . . . . . . . . . . . .
  • 6.4 Some calculations . . . . . . . . . . . . . . . . . .
  • 7 Constructing trees
  • 7.1 Building up from below . . . . . . . . . . . . . .
  • 7.2 Normal functions and ordinal notations . . . . .
  • 7.3 Further calculations . . . . . . . . . . . . . . . .
  • 7.4 Proof of wellordering . . . . . . . . . . . . . . . .
  • 8 Combinatorics
  • 8.1 Ramseys theorem . . . . . . . . . . . . . . . . . .
  • 8.2 Kruskals theorem . . . . . . . . . . . . . . . . . .
  • 8.3 Linearization . . . . . . . . . . . . . . . . . . . .
  • 8.4 Transfinite induction . . . . . . . . . . . . . . . .
  • 9 Labeled trees
  • 9.1 Extending finite trees . . . . . . . . . . . . . . .
  • 9.2 Well ordering of finite labeled trees . . . . . . . .

Related titles

    More of this author(s)