I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" with respect to a logic (or perhaps just specifically for sequent calculus?).

As far as I can tell, they don't directly provide a definition for the property of canonicity. I have heard this property discussed in other contexts, and so I think this is a general property about logical systems, but I can't figure out what the precise definition is.

I think the following is a good alternative phrasing of my question: if I have a set of rules for a sequent calculus, how can I decide if that system has the property of canonicity? also, how can I decide if that system does not have the property?

EDIT: also, I think that there is a difference between canonicity and proof normalization. Is this true? What is the difference?

  • $\begingroup$ This seems to be a somewhat informal notion. See Theorem 6. $\endgroup$ – Yuval Filmus Mar 13 '18 at 22:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.