Introduction to Proof Theory I: Sequent Calculus

Speaker: Tim Lyon

Abstract: Proof theory is an important branch of mathematical logic that is primarily concerned with the study and application of mathematical proofs. One of the preferred formalisms in proof theory for building deductive systems is Gerhard Gentzen's sequent calculus formalism. This talk is intended as an introduction to proof theory and will introduce a variant of Gentzen's sequent calculus for classical propositional logic. Moreover, the sequent calculus will be used to demonstrate and define fundamental proof theoretic notions such as sequents, types of inference rules, methods of soundness and completeness, and properties of calculi.

[vaibhavkhobragade]

Great very helpful. Actually, proof theory has very limited resouces on YouTube. This is a really valuable. Thank you so much Tim. :)

[jucom]

I haven't really had proof theory since i just started college a month ago but i get curious and this really helps me understand the basics of what i pick up around me so i don't have to wonder, thank you.

[knogger]

Awesome presentation, thanks a lot!
You've mentioned that eliminability implies admissibility, but are there admissible rules that aren't eliminable?
And if so, how would one go about proving admissibility without implicitly giving a transformation algorithm?

[oversoon]

Amazing video. Do you have any recommendations of resources for going deeper into topics in proof theory?

[booguy]

Thanks for this great presentation. It's very informative. I'm curious though;—why is it that A→(B→A) is an axiom even if it is shown to be derivable? Does this have to do with meta-logical analysis?

[maxpercer]

what happens in the corresponding formula when gamma is empty?

[encapsulatio]

For those like me who want to self study but have extremely weak mathematical background, how can I make sure I am truly ready and have all the prerequisites covered for learning formal logic, sequent calculus, natural deduction, etc?

[与我无关-zk]

How the Hilbert system is invented?
I mean how does Hilbert know that the three axioms can actually get other theorems with the help of MP?