3 ms·

Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it

by mzl 14y ago

Is really sequent calculus (http://en.wikipedia.org/wiki/Sequent_calculus http://en.wikipedia.org/wiki/Sequent_calculus) that odd, that you never encountered it in your math studies? I personally find it quite easy to read, with nicely structured proofs.

auggierose 14y ago
Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!
- tikhonj 14y ago
  Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
  - auggierose 14y ago
    I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
- mzl 14y ago
  Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.

by mzl 14y ago

auggierose 14y ago

Of course what is "easy" to read is always up to the individual to a certain degree. But this notation is used nowhere in math outside of logic. That should tell you something :-) Also in modern logic that is actually used in interactive proof assistants, this notation actually is not present any more, but then reintroduced when you write a paper about what you did!

tikhonj 14y ago
Isn't this sort of notation used in Coq, at least when it displays your current goal? Admittedly, it's an ASCII bastardization of the notation, but it's the same idea.
- auggierose 14y ago
  I don't mind writing instead of A => B => C the following: A B ---- C I just hate pressing everything into this style.
mzl 14y ago
Well, of course the logic notation in question is used in mostly in logic contexts. In the same manner, as a student of logic I will not come across special notation from analysis. Although I am not working in that area any more, when I used interactive theorem provers the one I used mostly would present the proofs in Sequent calculus. It showcased a nice connection between the logical framework and a small step operational semantics reading of te formulas. In my view, it is important to understand the reasons for different fields choices of notation; it typically reveals interesting things about the fields in question. When starting out learning a new field, it often seems strange and un-intuitive, but after a while one starts to recognize that there are many valid reasons for why a certain style of notation is used. Of course, sometimes it is just an accident of history, and bad choices stick around :) I've hopped around quite a bit in my studies (semantics, formal methods, operations research, theoretical computer science, pure algebra, logic), and I always feel overwhelmed with new notations and concepts. Nowadays I tend to expect it when trying to learn something new.