Terms for Classical Sequents: Proof Invariants and Strong Normalisation

from blog Home on consequently.org, | ↗ original
I’m giving a talk entitled “Terms for Classical Sequents: Proof Invariants and Strong Normalisation” at the Melbourne Logic Seminar. Abstract: A proof for a sequent \(\Sigma\vdash\Delta\) shows you how to get from the premises \(\Sigma\) to the conclusion \(\Delta\). It seems very plausible that some valid sequents have different proofs. It also...