[HN Gopher] Sequent Calculus and Notation - Par Part 1
       ___________________________________________________________________
        
       Sequent Calculus and Notation - Par Part 1
        
       Author : hoping1
       Score  : 29 points
       Date   : 2025-01-22 17:16 UTC (5 hours ago)
        
 (HTM) web link (ryanbrewer.dev)
 (TXT) w3m dump (ryanbrewer.dev)
        
       | hoping1 wrote:
       | Extensive and patiently-paced, with many examples, and therefore
       | unfortunately pretty long lol
        
       | groby_b wrote:
       | 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 wrote:
         | 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 wrote:
           | 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!!
        
       | cylinder714 wrote:
       | 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
        
       | btilly wrote:
       | 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 wrote:
         | Fair, I think of this as advanced logic, and those concepts
         | (and that notation) as prerequisite.
        
       | dunham wrote:
       | 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...
        
       ___________________________________________________________________
       (page generated 2025-01-22 23:02 UTC)