How to understand Sequent Calculus
ฝัง
- เผยแพร่เมื่อ 23 ก.ค. 2024
- What's the best proof system for formal logic? Many logicians will say it's the sequent calculus. But it can be hard to understand at first. In this video, I'll show you how I finally got my head around its difficult-looking rules.
You can support the channel and help it grow by contributing on my Ko-fi page: Ko-fi.com/atticphilosophy
The ideas in the video draw on Greg Restall's work in understanding proof systems, for example, his paper Multiple Conclusions:
consequently.org/papers/multi...
00:00 - Intro
00:40 - Sequents
01:25 - Multiple conclusions
01:42 - My method
03:03 - Accepting or rejecting sentences
03:49 - Understanding sequents
04:46 - Sequent proofs
05:56 - Sequent rules
07:23 - Proving LEM
09:08 - Intuitionistic proofs
10:33 - The key to understanding sequents
If there’s a topic you’d like to see covered, leave me a comment below.
Links:
My academic philosophy page: markjago.net
My book What Truth Is: bit.ly/JagoTruth
Most of my publications are available freely here: philpapers.org/s/Mark%20Jago
Get in touch on Social media!
Twitter: / philosophyattic
#philosophy # logic #proof
Thanks to your videos I finally understood natural deduction for quantifiers and now im excitedly trying to learn sequent calculus, thank you so much for making these videos mate!
You’re welcome!
Thank you so much, this really opened my eyes
This is great, thanks! I was wondering, could you please do a video on the Gentzen tree-style natural deduction system (like that used in Halbach's 'Logic Manual')? That would be SO helpful!
Ok, I’ll give it a go
Thank you very much for making this video. Just to clarify, in your proof of the law of excluded middle in the natural deduction system are you implicitly using the law of double negation?
Show us more Sequent Calculus ❤
Ok! What would you like to know?
@@AtticPhilosophy I don't speak for everyone, but I'd definitely like to see some worked examples and an overview of all the different logical & structural rules.
@@AtticPhilosophy video about LJ and LJ', please! Also double-negation LK embedding into LJ. And evaluation model of LJ (and continuation-style passing as an evaluation model for LK into LJ embedding). Also it would be super interesting to learn about the Category Theory behind the Sequent Calculus semantic, could it be generalized even more? Comparison of semantic of Sequent Calculus as a formal language with semantic of logics as a formal languages.
Thanks for the video Mark :)
You’re welcome!
Can you do a video on linear logic? It's not quite clicking for me
I am new to the system and would probably have not found it so easy to get without this introduction. Always assuming, of course, that I did get it. I read that LHS implies RHS when LHS is taken as a conjunction of statements, while RHS is a disjunction. In these terms I guess that, for a proof to work, at least one statement must be accepted on the LHS, and any additional statement is always accepted there, while everything on the RHS is provisionally reject-able, with the proviso that at least one statement must ultimately be accepted.
That's it - conjunction on the left, disjunction on the right.
Ooooh, I hadn't met Sequent Calculus before
so this indeed wetted my appetite for more
Do you have any book recommendations
on learning the Sequent Calculus?
or even better software
to help explore the ideas
This handbook article is very good (and free): mathweb.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf For a book, this one is very good: Proofs and Models in Philosophical Logic, Greg Restall, www.cambridge.org/core/elements/abs/proofs-and-models-in-philosophical-logic/A1907B05C24E1000270CC5B684FA7AAB
@@AtticPhilosophy
Thank you for your prompt response.
Interestingly the book is cheaper as a paperback than as an eBook.
@@AtticPhilosophy Thanks for these links I am digging through today Saturday.
Would another way to express the ideas on the LHS and the RHS as this: it is (or would be) set of propositions would be deemed inconsistent. That is to say to the term inconsistent means I accept the LHS and at the same time reject the RHS? Also I am wondering how close is this to the principle of Identity? That is to say if I have two identical portraits of ME on wall [where one is on the left and the other is to the right] that the right portrait is ugly while the left portrait is handsome. If both portraits are identical they must be described in the same way: one can not be ugly unless both are ugly. I hope I expressed that well. Another example, is X+2 = 2 + X but the X on the right hand side is 7 but the X on the left is 2. How can that be if it is the same X (otherwise we need two different variables)? It is inconsistent!
It’s not the propositions themselves that are inconsistent, for A |- A is a proof with nothing inconsistent. Rather, it would be bad to accept the LHS but reject the RHS.
What book would you recommend for an in-depth study of logic?
There are loads of good intro & more advanced textbooks, none covers it all, so it very much depends on what you want to cover. Some good choices:
Intro:
Logic, by Wilfrid Hodges
Logic, by Greg Restall
Logic: The Laws of Truth, Nick JJ Smith
Logic, its Scope & Limits, by Richard Jeffrey
More advanced:
Computability & Logic, Boolos & Jeffrey (a standard grad-level reference)
Logic For Philosophers, Ted Sider (aimed at philosophers)
Graham Priest, 2001: An Introduction to Non-Classical Logic (Good for propositional modal, intuitionistic and 3-valued logics and proof trees)
@@AtticPhilosophy Thanks You!
Though I can get my head around it, I can’t get used to interpreting sequents in terms of acceptance/rejection. Isn’t the left of a sequent just your assumptions and the right of a sequent just the possible conclusions, given whatever’s on the left?
Not quite as simple as “possible conclusions” on the right. Take, for example: |- p,~p. A valid sequent, but neither p nor ~p are possible conclusions, since neither is derivable from zero premises. What you can infer is their disjunction, so you could say: the disjunction of the stuff on the right is the conclusion.
@@AtticPhilosophy I guess the word “conclusion” is too proofy, but clearly the right of the sequent is saying that at least one of the formulas separated by a comma holds.
@@patrickwithee7625 That's right, but no saying which, and difficult to out this in proof-theoretic-acceptable terms (many proof theorists will want to avoid 'is true' altogether). Hence the disjunctive 'either-or' reading.
@@AtticPhilosophy So if the stuff on the right makes up a conclusion, how exactly are we "rejecting" the stuff on the right then?
@@Nicoder6884 The idea is to think of X |- Y as saying: its bad to accept the Xs and reject the Ys.
Can you make a video talking about free logic? 🙏
Good call! I'll add it to the list.
Personally, to me this interpretation makes less sense than the one I learned: A ⊢ B can be interpreted as "Knowing A, prove B." Thus the rule "..., A ⊢ A" is interpreted as, "knowing A, I have proved A." To me the advantage of this is that you can avoid thinking about this excluded middle-like "accept and reject."