Hacker News Reader

Comment by Reubend | Hacker News Reader

Thanks for posting this. As a beginner, do I need to already know what "sequent-calculus-style trees" are for this to be useful?

I didn't see any broad explanation of what the tree structure means here. I can see that disjunctions split a branch into 2 branches, but I'm still pretty confused overall.

View on HN

Sequent calculus trees [1] are straightforward. Essentially read them as: for each horizontal line, the judgment (assumptions ⊢ conclusion) below the line is valid if-and-only-if the judgments above the line are valid, by grace of the syntactic transformation rule named to the right of the line. These are stacked atop one another to form a tree, the leaves at the top (with nothing above the lines) being axioms of the system, the root at the bottom being the judgment whose proof is the tree.

Sometimes the trees are upside down from this, for reasons I haven't been able to divine. Some logics also permit multiple (alternative) conclusions in a judgment, which is then properly called a sequent.

Nearly the same notation is used for type judgements in type theory as well, with "assumptions ⊢ conclusion" being replaced by "environment ⊢ type assignments". [2]

[1] https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK (The preceding section introduces the notation but uses the upside-down variant, for unclear reasons -- I've rarely seen it elsewhere.)

[2] https://en.wikipedia.org/wiki/Type_theory#Technical_details

It isn't necessary to know theory for these visualisations to be useful, both Traf and Paperproof (and sequence calculus trees!) should, ideally, just reflect what's already happening in your mental image while you're writing a Lean/Coq/on-paper mathematical proof. But I agree it warrants a tutorial/explanation, got to write it. I think it might be particularly unclear what's happening if you're just looking at the full tree of the already-proved-theorem. As we're writing the proof, hypothesis nodes (green, what we have) move down; and goal nodes (red, what we want to have) move up. So it kind of goes from both sides to the center, and you should read it "from both sides to the center", takes getting used to. Here is a video of what's happening in Paperproof as we're writing the proof e.g.: https://www.youtube.com/watch?v=0dVj4ITAF1o.

Some searching found http://logitext.mit.edu/tutorial . It tries to explain sequent calculus with an interactive gui prover. Not sure how approachable it is... I've gotten too used to these things to know how to explain them properly.

Reply on news.ycombinator.com