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.
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.
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:
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...
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
Extensive and patiently-paced, with many examples, and therefore unfortunately pretty long lol
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.
Fair, I think of this as advanced logic, and those concepts (and that notation) as prerequisite.
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.
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
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!!