Pitchfork

From Girard Reading Group

A pitchfork is the ludic analogue of "sequent". There are two kinds of pitchforks:

• positive: ⊢ Λ
• negative: ξ ⊢ Λ

where ξ is a locus, and Λ is a finite set of loci.

Although not explicitly endorsed in Locus Solum, we can adopt the following heterodox readings of pitchforks:

• "⊢ Λ" asserts that all of the the loci in Λ can't be false, i.e. that if all the loci in Λ are false we have a contradiction.
• "ξ ⊢ Λ" asserts that if all the loci in Λ are false, then ξ is also false.

This is essentially dual to the usual reading of intuitionistic sequents Γ ⊢ A and Γ ⊢∙. However, the first step in proving a positive pitchfork is usually to focus on some particular locus. This suggests we could explicitly represent this intermediate stage as a phantom pitchfork ⊢ Λ; ξ. We can read this pitchfork as asserting that if all the loci in Λ are false, then ξ is true. We call these "phantom" pitchforks, since they do not actually appear in Locus Solum, but only lurk in the background.