Recent searches
Search options
Is there something like a framework for cut elimination?
As far as I know, to design a system that admits cut you need (1) deep intuition, and (2) to write some of the worst proofs ever conceived
Is there some kind of metatheory for designing proof systems that have "cut elimination by construction"?
@julesh imo the metatheory is category theory
@JadeMasterMath This is not specific enough... I can totally believe it's true but there are many many details to work out
@julesh yeah...I am working on it haha
@JadeMasterMath @julesh Glaive intensifies :D