# What is the definition of the property of Canonicity for a logic?

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?

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