Introduction to Proof Theory I: Sequent Calculus
Вставка
- Опубліковано 12 чер 2024
- Speaker: Tim Lyon
Webpage: sites.google.com/view/timlyon
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.
Great very helpful. Actually, proof theory has very limited resouces on UA-cam. This is a really valuable. Thank you so much Tim. :)
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.
Very helpful, thank you
Glad to hear it and thanks for watching! There's also a follow up video that dives into invertible rules, cut-elimination, and proof-search in case you are interested: ua-cam.com/video/hUO2D0Smh0w/v-deo.html
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?
Hello @knogger7756, glad you liked the video and great question!
So, first off, in the literature the notion of “eliminability” typically means one of two things: (1) some folks say a rule is “eliminable” if it occurs in a proof system, but can be removed from the system without affecting completeness, or (2) as in the video, a rule is “eliminable” if a 'permutation algorithm' exists that lets one permute/shift the rule upward in any proof until it is removed entirely from the proof.
Usually, if one has a proof system for a logic, then the proofs are recursively enumerable, meaning, if a rule is admissible, then technically an algorithm exists for finding a proof without the rule. Specially, if one has a proof that uses an admissible rule, then one can recursively enumerate all proofs of the system until one finds a proof without rule, which is guaranteed to exist since the rule is admissible. However, this still doesn’t imply eliminability in the sense of definition (2) above since this algorithm is not an algorithm that permutes/shifts the admissible rule upward in a proof until it is removed entirely from the proof.
Still, I am not aware of a case where admissible rules are not eliminable. That being said (and in answer to your second question), one can prove a rule R admissible without providing an ‘upward permutation elimination algorithm’ as follows: If you (1) prove your proof system S sound and complete and (2) prove a rule R not in the system sound, then (3) the system S+R (which is S extended with the rule R) is sound since both S and R are sound, and is also complete since S is complete and S+R extends S. This means that anything provable in S+R is provable in just S, confirming that R is admissible. However, this admissibility argument is not proven by means of an ‘upward permutation elimination algorithm’.
To summarize: (i) I am not aware of a situation where admissible rules are not eliminable in the sense of definition (2) above, though this doesn’t imply that such a situation doesn’t exist (this would need to be mathematically proven), but (ii) despite this, one can prove a rule admissible without providing an ‘upward permutation elimination algorithm’.
Great introduction!
Thank you!
Amazing video. Do you have any recommendations of resources for going deeper into topics in proof theory?
We are glad you liked the video! For resources on proof theory, the following are good introductory texts: (1) "An Introduction to Proof Theory" by Samuel Buss, which can be found for free online, and (2) "Basic Proof Theory" by Troelstra and Schwichtenberg. If you would like recommendations on more advanced topics in proof theory, feel free to ask 😉
I'd also recommend to take look at Kleene "Mathematical logic", awesome dense book, it starts with very beggining (propositional logic and model theory), proceeds with proof theory in propositional logic and goes further to more and more advanced topics (predicate calculus, etc).
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?
Hello Booguy! To answer your question, we first need to recognize that there are two proof systems presented here: (1) the Hilbert system Hcp (i.e. an axiomatization) for classical propositional logic, and (2) the sequent calculus Lcp for classical propositional logic. The formula A -> (B -> A) is an axiom in system (1), but not system (2).
Second, we want to argue that the sequent calculus Lcp is complete. We can argue this as follows: (I) It is known that Hcp is complete, i.e. every classical propositional validity can be derived by Hcp. (II) As shown on slide 17, every axiom of Hcp (which includes A -> (B -> A)) can be derived in Lcp, and also Lcp can simulate modus ponens (MP). (III) Therefore, if A is a classical propositional validity, it can be derived in Hcp by (I) above, meaning A can be derived in Lcp by (II) above. (IV) Hence, Lcp is complete with respect to classical propositional logic as it can derive every classical propositional validity.
what happens in the corresponding formula when gamma is empty?
Thank you for your question Max. When gamma is empty, we have the empty conjunction, which is taken to be top (also called "verum"), denoted ⊤, and when delta is empty, we have the empty disjunction, which is taken to be bottom (also called "falsum"), denoted ⊥. So, for example, the empty sequent "\emptyset |- \emptyset" would be interpreted as the formula ⊤ -> ⊥ (i.e. "top implies bottom"). If you have further questions, please feel free to comment/ask 🙂
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?
Thank you for your question. If you are interested, the following blog post/link gives a completeness proof of the Hilbert axiomatization discussed in the video: risingentropy.com/proving-the-completeness-of-propositional-logic/. The proof shows/establishes how the three axioms and MP can be used to derive any valid classical propositional formula. If you have further questions about completeness, about specific aspects of the proof, etc. please feel free to ask 🙂
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?
For self study, I would recommend Herbert B. Enderton's book "A Mathematical Introduction to Logic." In fact, I used this book for self study when I was first learning logic. Regardless of what book you choose, I would recommend using a book that (1) has a reputation of being introductory enough for self study (which can usually be determined by reading reviews, looking at comments on stack exchange, etc.) and (2) has solutions to exercises so you can check your work. Not only is reading the book and taking the time to think about the material important for understanding and memorization, but working through a few exercises at the end of every section/chapter in the book is also crucial in my opinion. Enderton's book will teach you propositional and first-order logic, some model theory, and related computational concepts such as (un)decidability. Also, I believe there is a solution manual to Enderton's exercises which can be found online.
For proof theory, I would recommend reading "An Introduction to Proof Theory" by Samuel Buss, which can be found for free online. Personally, when I first read this text, I would spend time trying to prove the lemmas, theorems, etc. prior to reading their proofs, treating the results in the text as exercises.
If the material contained within these books is too far outside the scope of your current mathematical skill, it might be good to first learn mathematical proof techniques to get accustomed with writing proofs, problem solving, etc. Some good books in this area are "An Introduction to Mathematical Proofs" by Loehr and "How to Prove It: A Structured Approach" by Velleman. Additionally, if you want to learn via online videos, Khan Academy has a large number of videos on mathematical topics.
Last, I would say that learning a new mathematical discipline takes time as one must digest the material and practice solving problems to get a good idea of how the mathematical objects behave. Therefore, in the beginning, you may never feel truly ready when you pick up a book on a new subject, but through effort and reflection you can certainly increase your skill and knowledge.
@@computationallogicgrouptud9652 Thank you so much for your in depth reply.
So if I successfully finish in the order you listed them all the books you recommended will I be ready and have no gaps in knowledge to learn type theory, linear logic(the part that has to do with type theory), linear lambda calculus, natural deduction, sequent calculus?
I also want to be able to read and successfully understand papers on combinatory logic and combinatory calculus variants, session types, refinement types, set theoretic types, separation logic, bunched logic.
What books/papers do you recommend for every one I listed?
Thank you again for being so helpful with your time and knowledge.
@@encapsulatio You are very welcome! If you read Buss's "An Introduction to Proof Theory," then you should acquire an understanding of natural deduction, the sequent calculus, and linear logic. However, this text assumes familiarity with propositional and first-order logic, so if you have not yet studied these topics, then it would be good to first read the two starting chapters of Enderton's book.
Regarding the other topics you wish to study, I am not too familiar with the literature, though for separation/bunched logic you might want to read David Pym's book "The Semantics and Proof Theory of the Logic of Bunched Implications." That being said, the topics you mentioned are quite advanced, so I would suggest you wait until you have finished learning about fundamentals notions (e.g. those I mentioned above) before moving onto studying these topics.
Last, if you are truly interested in learning all of the topics you mentioned, you might want to consider applying for a program at a university. For example, the MSc program in Logic and Computation at TU Wien offers courses in many of the subjects you mentioned: informatics.tuwien.ac.at/master/logic-and-computation-de/
@@computationallogicgrouptud9652 I can't even properly reply to you here in crappy youtube, everything is so censored. I always have my comment deleted.
@@computationallogicgrouptud9652 thank you for the reply, a question regarding the admission to the MSc in Logic&Computation, will a background(MSc in physics) suffice to apply? or is there a hard prerequisite ? thanks again!
Who is the instructor in this video?
The speaker is Tim Lyon ( sites.google.com/view/timlyon ). If you have any further questions, please let us know 🙂
@@computationallogicgrouptud9652 thank you. Love the channel!