FG1 Seminar talk

2014-10-31
Stefan Hetzl
Which proofs can be computed by cut-elimination?

Abstract:
This talk will be about the sequent calculus and cut-elimination in classical first-order logic.

Gentzen's proof of the cut-elimination theorem can be considered as a non-deterministic procedure based on local proof rewriting steps. I will speak about some recent results concerned with describing the set of cut-free proofs thus obtainable from a fixed proof with cuts.

I will not assume any prior knowledge in proof theory.