Does constructive dilemma hold in intuitionistic logic?

Question

I mean this law: $ (( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)) \Rightarrow r$

It seems to me that it does hold for INT. Is there any non-esoteric logic that excludes that law?

Answer 1

It seems that this is indeed an intuitionistic tautology. Let's assume that $ (( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)) \Rightarrow r$ is false, then, in another world $w$: $( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)$ is true and ($\star$) $r$ is false. It follows then that $p \vee q$ is true, $( p \Rightarrow r)$ is true and $(q\Rightarrow r)$ is true. If $( p \Rightarrow r)$ is true, then $p$ is false and $r$ is true, which contradicts ($\star$).

Alternatively:

1. $ (( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)) $ (premise)

2. $ p \vee q$ (simplification 1)

3. $ p \Rightarrow r$ (simplification 1)

4. $ q \Rightarrow r $ (simplification 1)

5. $ (p \Rightarrow r) \Rightarrow ((q \Rightarrow r) \Rightarrow (( p \vee q) \rightarrow r))$ (one of INT axioms)

6. $(q \Rightarrow r) \Rightarrow (( p \vee q) \rightarrow r)$ (MP 5,3)

7. $( p \vee q) \rightarrow r$ (MP 6,4)

8. $r$ (MP 7,2)