Algebra 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.