Relation between the "signature property", polarities and Sequent calculus in "The Blind Spot" book by J.-Y. Girard.

Question

I'm trying to understand one particular concept from the J.-Y. Girard's book "The Blind Spot" (pages 50-51) where he introduces positive and negative signatures to formulas. So now there are two types of the same formula $A$, i.e. $A^-$ and $A^+$. As I understood, when we use the formula $A$ as one of the formulas of $\Gamma$ from the sequent $\Gamma\vdash\Delta$, for example, it will appear there with a different signature.

Next, Girard states that there are now three possibilities of truth values taken by the pair $(A^-,A^+)$, i.e. (F,F), (F,T) and (T,T), where T stands for True and F for False. Later he states that they correspond to "three-valued" interpretation F, I, T (here I stands for "intermediate value"). The first question is why are there only three combinations of truth values instead of four?

Later, there is a statement that all "cut-free rules are validated by the interpretation « if all $\Gamma$ are true, then one $\Delta$ is not false »" (pp. 51). And later that the Cut rule is not validated by this interpretation. That's the main thing I would like to clarify for me and understand.

For example, I took the rule from sequent calculus (its simpler form to be more correct):

$$\frac{X\vdash A_1, B \quad X\vdash A_2, B}{X\vdash A_1\land A_2,B}$$

On this example, how this rule should be validated by that statement and values assignment? Assume they have the following polarities:

$$\frac{X^-\vdash A_1^+, B^+ \quad X^-\vdash A_2^+, B^+}{X^-\vdash A_1^+\land A_2^+,B^+}$$

Put $X^-$ to be T, $A_1^+$ and $A_2^+$ to be F and $B^+$ to be T. Does it mean that now if we read that interpretation statement this interpretation is conserved after the rule application? If yes, why do we need this polarities? And why the Cut rule does not fulfil the property?

P.S. There is almost no explanation in the book regarding this notion...

Answer 1

I. Consider a finite set of atomic formulae $\{ A_1, A_2, \dots, A_n \}$, and two lists of formulas $\Gamma, \Delta$ whose atomic subformulae all belong to $\{ A_1, A_2, \dots, A_n \}$.

If a sequent $\Gamma \vdash \Delta$ has no proof in the Sequent Calculus $\mathbf{LK}$, then you can assign classical truth values $f,t$ to the propositions $\{ A_1, A_2, \dots, A_n \}$ such that (under the usual truth table semantics for $\wedge, \neg, \vee, \rightarrow$) all the formulae in $\Gamma$ evaluate to $t$, but formulae in $\Delta$ evaluate to $f$.

This works because (as you might recall from page 43) the intuitive meaning of the sequent $\Gamma \vdash \Delta$ is that if all elements of $\Gamma$ are true, then it can't be that all elements of $\Delta$ are false. Quantifying over all assignments $q$, we get that $\Gamma \vdash \Delta$ has a proof precisely if $\forall q. (\forall \gamma \in \Gamma. q\gamma = t) \rightarrow (\exists \delta \in \Delta. q\delta \neq f).$

For example, $A \rightarrow B \vdash A \vee B$ has no proof in $\mathbf{LK}$. I know this because I can assign the value $f$ to $A$ and the value $f$ to $B$: under this assignment, $A \rightarrow B$ evaluates to $t$, but $A \vee B$ evaluates to $f$. This is classical truth-table semantics.

II. Having discovered the notion of polarity, and having observed that the left/right rules preserve polarity [3.3.3, 1st and 2nd paragraphs], we may wonder: can we put a twist on classical semantics, so that instead of assigning one fixed truth value to each atomic proposition in $\{ A_1, A_2, \dots, A_n \}$ as before, our new semantics will assign two, possibly different, truth values to each:

• the value of $A_i$ when $A_i$ occurs in a negative position (which we call the value of $A_i^-$),
• the value of $A_i$ when $A_i$ occurs in the positive position (which we call the value of $A_i^+$), while retaining the maxim that a sequent should have a proof precisely if whenever all elements of $\Gamma$ are true, then not all elements of $\Delta$ are false?

For example, I could consider the polarity-dependent assignment that

• always assigns $f$ to $A$,
• assigns $t$ to $B$ when $B$ occurs in a negative position (as $B^-$),
• assigns $f$ to $B$ when $B$ occurs in a positive position (as $B^+$).

What happens when we evaluate the sequent $A \rightarrow B \vdash A \vee B$ under this assignment? Well, that depends on which of the four possible polarizations we choose for our atomic formulae!

1. If we polarize as $A^+ \rightarrow B^- \vdash A^+ \vee B^+$, then the left hand side reduces to $f \rightarrow t$, which is $t$. The right hand side reduces to $f \vee f$, which is $f$.
2. If we polarize as $A^+ \rightarrow B^+ \vdash A^+ \vee B^-$, then the left hand side reduces to $f \rightarrow f$, which is $t$. The right hand side reduces to $f \vee t$, which is $t$.
3. For $A^- \rightarrow B^- \vdash A^- \vee B^+$ we get left $t$, right $f$.
4. For $A^- \rightarrow B^+ \vdash A^- \vee B^-$ we get left $t$, right $t$.

Notice that the left-hand side always evaluates to $t$, no matter how we polarize the atomic formulae. However, the right hand side is indeterminate until we fix a polarization of the atomic formulae. We could say that the formula $A \rightarrow B$ evaluates to $\mathbf{t}$ under the assignment, while formula $A \vee B$ evaluates to $\mathbf{i}$ (for indeterminate) and to the truth value $\mathbf{i}$ (for indeterminate). Notice that the truth values are assigned to the formula, not to any specific polarization!

A polarity-dependent (as Girard calls it, schizophrenic) assignment $q$ can behave in four possible ways on an atomic formula $A$:

1. $q$ assigns the same value $f$ to both positive and negative occurrences of $A$;
2. $q$ assigns the same value $t$ to both positive and negative occurrences of $A$;
3. $q$ assigns $f$ to positive occurrences of $A$, and assigns $t$ to negative occurrences of $A$; or
4. $q$ assigns $t$ to positive occurrences of $A$, and assigns $f$ to negative occurrences of $A$.

However, the polarity-dependent assignment $q$ can evaluate to only three different truth values on a (not necessarily atomic) formula $\varphi$:

1. $q$ evaluates to $\mathbf{v}$ on $\varphi$ (iff $q$ evaluates to $t$ on all possible polarizations of $\varphi$);
2. $q$ evaluates to $\mathbf{f}$ on $\varphi$ (iff $q$ evaluates to $f$ on all possible polarizations of $\varphi$); or
3. $q$ evaluates to $\mathbf{i}$ on $\varphi$ (iff $q$ evaluates to $t$ on some possible polarizations of $\varphi$, and $f$ on other possible polarizations of $\varphi$).

You can verify that behaviors 3 and 4 above do not need to be distinguished: the truth value of $q(A)$ is $\mathbf{i}$ in either case. This answers your question regarding the odd number of truth values.

III. At this point, we can write down truth tables for our three truth values $\mathbf{v}, \mathbf{f}, \mathbf{t}$ [p51 top], and for a moment it looks like we might succeed in writing down a 3-valued semantics with the property that $\Gamma \vdash \Delta$ has a proof precisely if $\forall q. (\forall \gamma \in \Gamma. q\gamma = t) \rightarrow (\exists \delta \in \Delta. q\delta \neq f)$, where $q$ ranges over polarity-aware (3-valued) assignments.

Indeed, we have already observed that the left/right rules of the sequent calculus preserve polarity. However, to make our new, polarity-aware semantics work, we need to handle the identity rules (axiom and cut) as well! Alas, the identity rules don't preserve polarity: instead, they relate positive and negative occurrences of the same formula [3.3.3, 3rd p].

In particular, consider the following instance of the cut rule:

$$ \frac{A \vdash B ~~~ B \vdash C}{A \vdash C} $$

Our 3-valued semantics validates this instance of the cut rule precisely if $\forall q. qA = t \rightarrow qB \neq f$ and $\forall q. qB = t \rightarrow qC \neq f$ together imply that $\forall q. qA = t \rightarrow qC \neq f$. But this is not the case: consider e.g. an assignment that sets $A$ to $\mathbf{t}$, $B$ to $\mathbf{i}$ and $C$ to $\mathbf{f}$. This answers your question regarding the cut rule.

IV. General advice: In the summer of 2013, as preparation for a linear logic summer school, I worked through the Blind Spot in its entirety (well, a slightly shorter version than the published one, the coursang.pdf that was available on JYG's website at the time). I came to the conclusion that it's a textbook meant as a vehicle for teaching deconstructive textual analysis. Coming up with your own readings (rejecting most of the bad ones you came up with, then formalizing the better ones and using them to prove non-trivial theorems) is not easy, but it is the entire point of the book, and by far the most useful skill you can get out of it (well, you'll learn plenty of proof theory along the way too). Basically, you're supposed to read it as Derrida taught. I'm sure you'll have fun working through it, but be aware: Math.SE, where the rules dictate that questions cannot be opinion-based and have to be answered by formalizing and explaining a specific meaning, goes against the book's spirit, at least a little bit, and might mean that you get less out of it than you otherwise would.