Sequent Calculus and Notation – Par Part 1 (opens in new tab)

(ryanbrewer.dev)

38 pointshoping11y ago10 comments

10 comments

There is a interactive web toy for sequent calculus proofs here: http://logitext.mit.edu/main

For natural deduction and other topics, Bob Atkey's interactive course is fun: https://personal.cis.strath.ac.uk/robert.atkey/cs208/index.h...

cylinder7141y 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

groby_b1y 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.

rck1y 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

hoping1OP1y 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!!

Tainnor1y ago

Sequent calculus is way older than Lean or any similar such language. It's a bit like saying "this looks like Haskell" when reading about the Lambda Calculus.

hoping1OP1y ago

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

btilly1y 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.

Tainnor1y ago

It may help, if you're familiar with set notation, to remember that x ∈ A ∩ B iff x ∈ A ∧ x ∈ B - the symbols mirror each other.

hoping1OP1y ago

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

j / k navigate · click thread line to collapse

10 comments

dunham1y ago

There is a interactive web toy for sequent calculus proofs here: http://logitext.mit.edu/main

For natural deduction and other topics, Bob Atkey's interactive course is fun: https://personal.cis.strath.ac.uk/robert.atkey/cs208/index.h...

cylinder7141y 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

groby_b1y 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.

rck1y ago

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

hoping1OP1y 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!!

Tainnor1y ago

Sequent calculus is way older than Lean or any similar such language. It's a bit like saying "this looks like Haskell" when reading about the Lambda Calculus.

hoping1OP1y ago

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

btilly1y 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.

Tainnor1y ago

It may help, if you're familiar with set notation, to remember that x ∈ A ∩ B iff x ∈ A ∧ x ∈ B - the symbols mirror each other.

hoping1OP1y ago

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

j / k navigate · click thread line to collapse