[colanderman]

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