Why do you only need to show validity in one world when using trees in institutionist/constructivist logic?

Question

Depicted below, my prof used a tree to prove that an argument is valid according to intuitionist logic.

However, I can't find a contradiction in world 0. Why is invalidity ascertained when all branches in one world (in this case w1) close?

Answer 1

We can easily prove that :

$(\lnot p \lor q) \rightarrow (p \rightarrow q)$

holds intuitionistically with Natural Deduction.

---

I'm quite unfamiliar with the intuitionistical version of tableau method; I've seen :

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

where the usual tableau rules are modified as follows :

$$\frac{S, \ F(\lnot X)}{S_T, \ TX} \quad \text {(F $\lnot$)}$$

and :

$$\frac{S, \ F(X \rightarrow Y)}{S_T, \ TX, FY} \quad \text {(F $\rightarrow$)}$$

where $S_T$ means $\{TX \ | \ TX \in S \}$.

---

Thus :

$1) \ \{ T(\lnot p \lor q) , F(p \rightarrow q) \}$

then apply $(F \rightarrow)$ :

$2) \ \{ T(\lnot p \lor q) , Tp, Fq) \}$

then apply $(T \lor)$ to produce two branches :

$3_L) \ \{ T(\lnot p \lor q) , T\lnot p, Tp, Fq) \}$

and :

$3_R) \ \{ T(\lnot p \lor q) , Tq, Tp, Fq) \}$.

The right brach $3_R)$ closes by $\{ Tq, Fq) \}$; finally, we we have to apply $(T \lnot)$ to the left branch $3_L)$ producing :

$4) \ \{ T(\lnot p \lor q) , Fp, Tp, Fq) \}$;

now also this branch closes by $\{ Fp, Tp \}$, and the validity of the formula is proved.

---

---

Here is the proof with Natural Deduction :

1) $\lnot p \lor q$ --- assumed [a]

2) $p$ --- assumed [b]

3) $\lnot p$ --- assumed from 1) for $\lor$-elimination

4) $\bot$ --- from 2) and 3) by $\rightarrow$-elimination

5) $q$ --- from 4) by $\bot$-elimination

6) $q$ --- assumed from 1) for $\lor$-elimination

7) $q$ --- from 3)-5), 6) and 1) by $\lor$-elimination

8) $p \rightarrow q$ --- from 2) and 7) by $\rightarrow$-introduction, discharging [b]

9) $(\lnot p \lor q) \rightarrow (p \rightarrow q)$ --- from 1) and 8) by $\rightarrow$-introduction, discharging [a].

---

---

Comment

The left-branch of your tree, we have a contradiction in $w_1$ on $p$, labelled both $+1$ and $−1$, and also in the right-branch we have a contradiction in $w_1$ on $q$, labelled both $−1$ and $+1$.

Having shown that the the tableau trying to falsify the formula $(¬p∨q)→(p→q)$ closes without success (i.e. all finished branches are "crossed") we have shown that it is not falsifiable.

Being not falsifiable, the formula is valid, i.e. true in all models.