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?


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$.


$$\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)

  • $\begingroup$ Thanks. That's a handy tool to have in my toolbox. $\endgroup$
    – J126
    Sep 22 '16 at 22:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.