2
$\begingroup$

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?

$\endgroup$

1 Answer 1

5
$\begingroup$

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)

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .