Motivation for signed tableaux rules for propositional intuitionistic logic

Question

I've been studying a signed tableaux proof system for propositional intuitionistic logic, and I'm confused about two of the inference rules stipulated. Most of the inference rules are quite straightforward, and in fact coincide with the inference rules for signed tableaux. For example, here is the rule for $T\wedge$: $$ \frac{S,T(X\wedge Y)}{S,TX,TY}T\wedge$$ And here is the rule for $F\vee$: $$ \frac{S,F(X\vee Y)}{S,FX,FY}F\vee$$ However, the rules for $F\neg$ and $F\rightarrow$ are causing me some confusion: $$\frac{S,F(\neg X)}{S_T,TX}F\neg \qquad \frac{S,F(X\rightarrow Y)}{S_T,TX,FY}F\rightarrow$$ Where $S_T=\{TX:TX\in S\}$. So, for these two particular rules, why must we remove all the formulas with sign $F$? I'm lacking a motivating, intuitive reason to remove all the formulas with sign $F$ when applying either of these two rules. If you can, please avoid appealing to the soundness or completeness of this proof system for propositional intuitionistic logic.

Thanks in advance for your help!

Answer 1

Revised edition

We have to see :

• Saul Kripke, Semantical Analysis of Intuitionistic Logic I (1965), page 97-on,

and :

• Melvin Fitting, Intuitionistic logic, Model theory and Forcing (1969), page 28-on.

According to Kripke's explanation [page 99] :

To assert $\lnot A$ intuitionistically in the situation $H$, we need to know at $H$ not only that $A$ has not been verified [proved] at $H$, but that it cannot possibly be verified at any later time, no matter how much information is gained; to assert $A ⊃ B$ in a situation $H$, we need to know that in any later situation $H′$ where we get a proof of $A$, we also get a proof of $B$.

How this is related to tableaux ? See Fitting [page 29] :

The corresponding classical tableau system is like the above, but in rules $F \lnot$ and $F \supset$, $S_T$ is replaced by $S$. The interpretations of the classical and intuitionistic systems are different.

In the classical system $TX$ and $FX$ mean $X$ is true and $X$ is false respectively. The rules may be read: if the situation above the line is the case, the situation below the line is also (or one of them is, if the rule is disjunctive). Thus $TX$ means the same as $X$, and $FX$ means $\lnot X$.

Classically the signs $T$ and $F$ are dispensable. Proof is a refutation procedure. Suppose $X$ is not true (begin a tableau with $FX$). Conclude that some formula must be both true and not true (a closed configuration is reached). Since this can not happen, $X$ is true.

In the intuitionistic case $TX$ is to mean $X$ is known to be true ($X$ is proven). $FX$ is to mean $X$ is not known to be true ($X$ has not been proved). The rules are to be read: if the situation above the line is the case, then the situation below the line is possible, i.e. compatible with our present knowledge (if the rule is disjunctive, one of the situations below the line must be possible). For example consider rule $F \supset$ . If we have not proved $X \supset Y$, it is possible to prove $X$ without proving $Y$, for if this were not possible, a proof of $Y$ would be ‘inherent’ in a proof of $X$, and this fact would constitute a proof of $X \supset Y$. But we have $S_T$ below the line in this rule and not $S$ because in proving $X$ we might inadvertently verify some additional previously unproven formula (some $FZ \in S$ might become $TZ$). Similarly for $F \lnot$. The proof procedure is again by refutation. Suppose $X$ is not proven (begin a tableau with $FX$). Conclude that it is possible that some formula is both proven and not proven. Since this is impossible, $X$ is proven.

This explanation can be clarified considering the semantical clauses for :

$w \vDash \lnot X$ and $w \vDash (X \supset Y)$.

These two are the only one where the clause consider : for all $w' \in W$ such that $wRw'$.

The $F \lnot$ rule, e.g., must be derived considering the negation of the above clause, i.e. :

$w \nvDash \lnot X$ iff for some $w' \in W$ such that $wRw'$ : $w' \vDash X$.

Thus, removing from the tree the $F$ formulae, forces us to search for a contradiction in a "later situation".