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

Γ⊢J

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

∅⊢

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

J⊢J⊢J(id).

Cartesian contexts

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

Γ,I,I,Δ⊢JΓ,I,Δ⊢J(C),

and the weakening rule

Γ,Δ⊢JΓ,I,Δ⊢Γ,I,Δ⊢J(W),

and the 𝛿 rule

Γ,J,Δ⊢Γ,J,Δ⊢J(𝛿),

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 ↩