Prove $(\lnot \lnot A \implies A) \implies (A \lor \lnot A)$ in propositional logic

Question

I'm working through the exercises of the first chapter of Thompson's Type Theory and Functional Programming and have gotten stuck on exercise 1.7 on page 28(marked as page 15):

1.7. Show that the three characterizations of classical logic (as an extension of the intuitionistic system above) are equivalent.

The three characterizations are roughly:

1. $\implies \lnot A \lor A$
2. $\lnot \lnot A \implies A$
3. Given a proof of $\lnot A \implies B$ and $\lnot A \implies \lnot B$, one can infer $A$

To go about this, I am attempting $\#1 \implies \#2$, $\#2 \implies \#1$, $\#1 \implies \#3$ and so forth. I was able to prove $\#1 \implies \#2$ but I'm stuck on proving that $\#2 \implies \#1$.

Edit: Originally I wrote #1 as $\lnot A \lor A$, changed to the correct value: $\implies \lnot A \lor A$

Answer 1

Using this proof wiki as a reference, it seems an indirect approach to $\#2 \implies \#1$ is to inutitionistically establish

$$ \vdash \lnot \lnot (A \lor \lnot A)$$

without using $\#2$ or $\#3$, then use that to establish $\#2 \implies \#1$. In detail:

$$\begin{array} {rll} 1 & \quad \quad \lnot (A \lor \lnot A) & \text{New Premise} \\ 2 & \quad \quad \quad \quad A & \text{New Premise} \\ 3 & \quad \quad \quad \quad A \lor \lnot A & \text{Or Intro of 2} \\ 4 & \quad \quad \quad \quad \bot & \text{Contradiction of 1 and 3} \\ 5 & \quad \quad \lnot A & \text{Not Intro of 2 through 4} \\ 6 & \quad \quad A \lor \lnot A & \text{Or Intro of 5} \\ 7 & \quad \quad \bot & \text{Contradiction of 1 and 6} \\ 8 & \lnot \lnot (A \lor \lnot A) & \text{Not Intro of 1 through 7} \\ \end{array}$$

There is a bit of a problem with this approach is that you are really establishing

$$\lnot \lnot A_1 \implies A_1 \vdash A_2 \lor \lnot A_2$$

where $A_1$ and $A_2$ are different propositional variables, which does answer the question being asked, to establish the equivalence of the axioms, but it leaves behind the more interesting question of whether

$$\lnot \lnot A \implies A \vdash A \lor \lnot A$$

can be established. All of the pairings $\#M \implies \#N$ for $N \ne 1$ can be established without resorting to separate propositional variables.

Edit: Nevermind, Mauro Allegranza writes in another answer that it is not possible to establish $\lnot \lnot A \implies A \vdash A \lor \lnot A$.

---

Edit: Reponse to question in comments :

First, there is a difference between an inference an a theorem. An inference is procedural concept, it is an algorithm. It has inputs (possibly zero) and outputs.

When the book writes $A \lor \lnot A$, they are describing an inference, not a theorem. It has 1 input: a true/false expression for $A$, such as $X \land Y$. It has 1 output: a disjunction, such as $(X \land Y) \lor \lnot (X \land Y)$. Even though it is written $A \lor \lnot A$, that is a just a mnemonic, a bit of a lie, a complete description of an inference requires a programming language.

Let $C$ be the set of inferences of constructive logic, $E$ is the inference of the excluded middle, and $D$ is the inference of double negation. Let $E_T$ be the theorem $A \lor \lnot A$ and let $D_T$ be the theorem $\lnot \lnot A \implies A$ (for simplicity we'll ignore #3). Let $[A := V]$ be use to denote replacing the propositional variable $A$ with propositional expression $V$.

The book is asking you to establish that the theorems of $C \cup E$ equal to the theorems of $C \cup D$. We can prove $\vdash_{C} E_T \implies D_T$. Therefore $\vdash_{C \cup E} D_T$. Therefore any proof $\vdash_{C \cup D} Z$ can be converted to a proof $\vdash_{C \cup E} Z$ by replacing every use of $D[A := V]$ with $(\vdash_{C + E} D_T)[A := V]$. Therefore, if a thereom is in $C \cup D$, it is also in $C \cup E$.

However, we cannot prove $\vdash_C D_T \implies E_T$ because it isn't a theorem of constructive logic. But we can still prove $\vdash_{C \cup D} E_T$. From which it follows that any proof $\vdash_{C \cup E} Z$ can be converted into a proof $\vdash_{C \cup D} Z$ by replacing every use of $E[A := V]$ with $(\vdash_{C \cup D} E_T)[A := V]$. Therefore every theorem in $C \cup E$ is also in $C \cup D$.

In short, #1 and #2 are equivalent inferences (they produce the same theorems when added to constructive logic), but they are not equivalent theorems (they do not imply each other in constructive logic).

Answer 2

You're trying to prove something too strong. Letting $B$ be $A \vee \neg A$, it suffices to show that $\neg \neg B$ holds intuitionistically (whence if 2 holds for any $A$, then $B$ holds).

Answer 3

Applying the definition ($\alpha$$\implies$$\bot$) to $\lnot$A in ($\lnot$$\lnot$A$\implies$A) we obtain:

1. ($\lnot$(A$\implies$$\bot$)$\implies$A).

And applying the definition ($\alpha$$\implies$$\bot$) to 1. we obtain

2. (((A $\implies$ $\bot$) $\implies$ $\bot$) $\implies$ A).

Which I find a bit strange for an axiom, but I digress. Actually, your text talks about a rule of inference, not an axiom, but I still find such a rule a bit strange to lie at the basis of a system, but I have digressed again.

The rule, which I'll call Wajsb., would go:

(($\alpha$ $\implies$ $\bot$) $\implies$ $\bot$)

---

$\alpha$

End of rule.

The following doesn't follow the same style as your book, but perhaps might help you construct a proof in that style.

hypothe. 1 | (((A$\implies$$\bot$) $\lor$ A)$\implies$ $\bot$)

hypothe. 2 || (A $\implies$ $\bot$)

2 A-intro 3 || ((A$\implies$$\bot$) $\lor$ A)

3, 1 mo.p 4 || $\bot$

2-4 ar. in 5 | ((A$\implies$$\bot$)$\implies$$\bot$)

5, Wajsb. 6 | A

6 A-intro 7 | ((A$\implies$$\bot$) $\lor$ A)

7, 1. mo.p 8 | $\bot$

1-8 ar. in 9 ((((A$\implies$$\bot$)$\lor$A)$\implies$$\bot$)$\implies$$\bot$)

9, Wajsb. ((A$\implies$$\bot$)$\lor$A)