Proof system

Context in a proof system

A context is an idiom in the design of proof systems à la Gentzen for a collection of assumptions underlying a given judgement. Usually we add a judgement for “ is a context” which is written

A judgement in the context is written

which informally means “under the assumptions , the judgement thesis holds.” Typically there is an empty context or initial context

and we write as a shorthand for . We also have the identity rule

Cartesian contexts

A proof system with contexts is said to have cartesian contexts1 iff it has some variant contraction rule

and the weakening rule

and the rule

although the exact form of these vary depending on the proof system.2 Note that from the rule one can derive the identity rule.

#state/tidy | #lang/en | #SemBr

Footnotes

  1. This is my own term, arising from the need to distinguish contexts in intuitionistic (or classical) logic from contexts in linear logic. The term intuitionistic context might be deemed appropriate, but seems loaded, so I have opted for cartesian, which reflects categorical semantics. ↩

  2. see e.g. 2025. Introduction to Homotopy Type Theory, p. 17 ↩