# Proof in constructive mathematics using decidability.

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

• 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? – Henning Makholm Sep 28 '18 at 17:11
• 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. – Carl Mummert Sep 28 '18 at 17:18

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

• 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. – Carl Mummert Sep 28 '18 at 17:32

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.