FG1 Seminar talk
Which proofs can be computed by cut-elimination?
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.