Proving "Or Statements" in Type Theory

Question

Oftentimes in math we see statements of the form $P \to (Q \vee R)$. To prove them we can assume $P$ is true and $R$ is false, and then demonstrate that $Q$ is true. This method of proof has the form: $$ [ (P \wedge \neg R) \to Q ] \to [ P \to ( Q \vee R ) ]. $$ It seems to me this would be valid in a constructive type theory. I would have a function type, $H$, that takes $(p,f):P \wedge \neg R$ and gives $H(p,f):Q$. To prove the above proof method, I would have to obtain from such a function another function, $g$, such that $g(p):Q \vee R$ when $p:P$. This seems impossible, since the data that $H$ requires is both $p:P$ and $f:\neg R$.

Is this form of argument not valid in constructive type theory?

Answer 1

For intuitionistic logic, a proposition is a tautology iff it is identically true in the logic of open sets in the plane. (similar to how, in classical logic, it's valid iff its truth table in two-valued logic is identically true)

In this logic,

• $\top$ (or "true") is the whole plane
• $\bot$ (or "false") is the empty set
• $\vee$ is union
• $\wedge$ is intersection
• $\neg$ is exterior (not complement)
• $X \to Y$ is the interior of $X^c \cup Y$ ($X^c$ being the complement)

And we can construct a counterexample:

• Let $P$ be the whole plane
• Let $R$ be the whole plane minus the origin
• Let $Q \subseteq R$.

Then,

$$\begin{align} [ (P \wedge \neg R) \to Q ] \to [ P \to ( Q \vee R ) ] &= [ (\mathbb{R}^2 \cap \varnothing) \to Q ] \to [ \mathbb{R}^2 \to R ] \\&= [\varnothing \to Q] \to R \\&= \mathbb{R}^2 \to R \\&= R \end{align}$$

but $R \neq \mathbb{R}^2$, so this proposition is not a tautology in intuitionistic logic. (or in any system weaker than intuitionistic logic)