Sequent Calculus and Notation – Par Part 1

(ryanbrewer.dev)

25 points | by hoping1 4 hours ago ago

7 comments

  • cylinder714 2 hours ago

    Support for sequent calculus is built into Mark Tarver's Shen language; here's the relevant chapter in his Book of Shen: https://shenlanguage.org/TBoS/tbos_228.html

  • hoping1 4 hours ago

    Extensive and patiently-paced, with many examples, and therefore unfortunately pretty long lol

  • btilly an hour ago

    What is the upside down v supposed to be? Yeah, I know that it is "and". But it isn't specified, and I do little enough logic that I had to look it up.

    • hoping1 29 minutes ago

      Fair, I think of this as advanced logic, and those concepts (and that notation) as prerequisite.

  • groby_b 3 hours ago

    Alas, not having had the time to fully read yet, but starting at the "Axiom rule" part, a strong feeling starts popping up that this is Lean, but with mathy symbols.

    I don't know if the intuition will hold on further reading, but there was a strong "I've seen you in a different trench coat" feeling.

    • rck 2 hours ago

      Yup! Lean is based on a variant of the Calculus of Constructions, which is in turn based on strong connections between (intuitionistic) natural deduction and type theory. The connection is incredibly beautiful:

      https://en.wikipedia.org/wiki/Calculus_of_constructions

      • hoping1 2 hours ago

        Ah heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!