1
$\begingroup$

I am working in constructive mathematics that means without the law of excluded middle. One may also interpret this as working in inuitionistic logic.

Lets assume I have some set $A$ such that I know that $0 \in A$ is decidable. I have another statement $B$. I want to prove that $B \Rightarrow (0 \in A)$. Is the following proof strategy justified in constructive mathematics:

I make a case distinction:

Case 1: $0 \in A$, hence nothing to show.

Case 2: $ 0 \notin A$. Then bla bla bla bla bla $\rightarrow$ contradiction. Hence we must have $0 \in A$.

To be more precise: The contradiction I get in Case 2 is $\neg B$. (this is a contradiction since I assumed $B$).

I am not sure which of the following logical expressions is used in this proof. Either

$B \rightarrow \neg A \rightarrow \neg B \rightarrow A$

or

$\neg \neg A \rightarrow A$

($\neg A$ is short for $0 \notin A$).

$\endgroup$
  • $\begingroup$ What does it mean for one of those formulas to be "used in" the proof? And how did you select exactly those formulas to ask about? $\endgroup$ – Henning Makholm Sep 28 '18 at 17:11
  • $\begingroup$ The main issue is whether you work in intuitionistic logic with the axiom scheme $\bot \to\phi$, or in a weaker logic without that scheme. $\endgroup$ – Carl Mummert Sep 28 '18 at 17:18
0
$\begingroup$

By "$0 \in A$" is decidable, we just mean $0 \in A \lor 0 \not \in A$.

Given that assumption, if you can prove $\lnot \lnot (0 \in A)$, you can prove $0 \in A$. As you know $\lnot \lnot (0 \in A)$ is $\lnot (0 \in A) \to \bot$.

The proof of $0 \in A$ is as follows.

Case 1: $0 \in A$. Done.

Case 2: $0 \not \in A$, i.e. $\lnot (0 \in A)$. Then, from $\lnot (0 \in A) \to \bot$, we obtain $\bot$. Then, from the contradiction rule $\bot \to 0 \in A$, we have $0 \in A$.

$\endgroup$
  • $\begingroup$ Thanks for accepting this answer. Henning Makholm posted essentially the same answer simultaneously, and as far as I can tell his answer is equally valid with mine. $\endgroup$ – Carl Mummert Sep 28 '18 at 17:32
1
$\begingroup$

You know $A\lor\neg A$ and $\neg A\to\neg B$, and you want to prove $B\to A$:

Assume $B$, and we then seek to prove $A$.

Do case analysis on $A\lor\neg A$ (which we already know holds).

In the case $A$ we're done.

In the case $\neg A$, apply $\neg A\to\neg B$ to get $\neg B$. Together with the assumption $B$, this is a contradiction, and by the principle of explosion we're allowed to conclude $A$.

In both cases we could conclude $A$, so $A$, and therefore (discharging the hypothesis) $B\to A$.

All of this is perfectly valid intuitionistcally.

$\endgroup$

Your Answer

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