Subformula

From Girard Reading Group

In ludics, formulas are represented as loci ξ and subformulas by subloci ξ*i. Immediate subformulahood respects focusing: so P^⊥, Q^⊥, and R^⊥ are all immediate subformulas of ((P^⊥ ⊕ Q^⊥) ⊗ R^⊥), since ⊕ and ⊗ are both positive connectives.

One way to look at this is that the above formula could have been written as

• ((Q^⊥ ⊕ P^⊥) ⊗ R^⊥)
• (R^⊥ ⊗ (P^⊥ ⊕ Q^⊥))
• ((P^⊥ ⊗ R^⊥) ⊕ (R^⊥ ⊗ Q^⊥))
• etc... I believe there are 12 ways in all.

However, if you look at the leaves of the left-focusing step, they are exactly the same - two possibilities, one of which has "|- Δ₁,P" and "|- Δ₁,R" as leaves, and another which has "|- Δ₁,Q" and "|- Δ₁,R" as leaves. The idea behind loci is to observe that because the behavior of the focused rules is exactly the same, it is counter-productive to view all 12 formulas as 12 different things - the use of loci has the result that all 12 must be treated identically.

You can see how this turns out for a left-focus on ((P^⊥ ⊕ Q^⊥) ⊗ R^⊥) below:

    |- Δ1,P
   —————————
   P⊥ |- Δ1         |- Δ2,R
———————————————    —————————
P⊥ ⊕ Q⊥ |- Δ1     R⊥ |- Δ2
————————————————————————————
(P⊥ ⊕ Q⊥) ⊗ R⊥ |- Δ1,Δ2

    |- Δ1,Q
   —————————
   Q⊥ |- Δ1         |- Δ2,R
———————————————    —————————
P⊥ ⊕ Q⊥ |- Δ1     R⊥ |- Δ2
————————————————————————————
(P⊥ ⊕ Q⊥) ⊗ R⊥ |- Δ1,Δ2