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$

  • 1
    $\begingroup$ It suffices to prove $\#1\vdash \#2$, $\#2\vdash \#3$, $\#3\vdash \#1$, or any other cyclic triad, $\endgroup$ Oct 12, 2016 at 4:19
  • 1
    $\begingroup$ @GrahamKemp $(\#3 \vdash \#1)$ is not provable, neither is $(\#2 \vdash \#1)$. You have to prove something like $(\vdash \#2) \implies (\vdash \#1)$. (where $\vdash$ refers to a constructive proof, and $\implies$ refers to any kind of proof that you trust). See math.stackexchange.com/a/913019/97045 $\endgroup$
    – DanielV
    Oct 12, 2016 at 22:55

3 Answers 3


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

  • $\begingroup$ so basically, 4 and 7 establish 1 from p and $\lnot$ p, respectively. $\endgroup$
    – RJM
    Oct 12, 2016 at 3:53
  • $\begingroup$ @RobertJMcGinness No, that's not a correct summary. (1) is never being established, and (4)/(7) never establish anything. You may be used to a view of logic where you only infer new theorems from previously established theorems. But in actuality, most logics allow you to infer theorems from previously established proofs as well, not just the theorem. For example, a rule of inference is "From $(X \vdash Y)$ infer $X \implies Y$", another is "From $(X \vdash \bot)$ infer $\lnot X$". Note that the $\bot$ isn't the input to the inference, but the entire $(X \vdash \bot)$ is. $\endgroup$
    – DanielV
    Oct 12, 2016 at 4:02
  • $\begingroup$ That is pretty cool. Is it correct, then, to look at it as you are building the theorem of "classical logic" with the theorems of intuitional? Does that make it equivalent to the theorem in classical in terms of how it functions? $\endgroup$
    – RJM
    Oct 12, 2016 at 4:13
  • $\begingroup$ @RobertJMcGinness Is English your native language? $\endgroup$
    – DanielV
    Oct 12, 2016 at 4:31
  • $\begingroup$ Ganz klar, nicht? $\endgroup$
    – RJM
    Oct 12, 2016 at 4:32

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

  • $\begingroup$ How do you establish $\lnot \lnot B$ from #3, even given $B = A \lor \lnot A$ ? $\endgroup$
    – DanielV
    Oct 12, 2016 at 3:30
  • 1
    $\begingroup$ I was just looking at characterization #2 implying characterization #1. Substituting $\bot$ for $B$ would work when trying to show #2 from #3. $\endgroup$ Oct 12, 2016 at 4:14
  • $\begingroup$ Actually, I mistyped #1. I just fixed it. In this light, I don't see how showing that given #2, and ~~(A \/ ~A) == (A \/ ~A) given #2 proves #1. $\endgroup$
    – redfish64
    Oct 12, 2016 at 6:57

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

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


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)

  • 1
    $\begingroup$ It is a strange thing for an axiom schema, but the reason it is considered is because it constructive plus any of the equivalent formulations in the question makes the propositional part of constructive logic equivalent to 2 valued propositional logic (aka truth tables); $\endgroup$
    – DanielV
    Oct 12, 2016 at 22:00
  • $\begingroup$ @DanielV I might have a different reason for considering it strange as an axiom schema than you. And, of course, you are correct about how joining it to constructive logic yields 2 valued propositional logic. Why do you find it strange? $\endgroup$ Oct 12, 2016 at 22:42
  • 1
    $\begingroup$ I have 2 reasons for disliking this as an axiom. The first is that I'm from the old style of philosophy that believes built in axioms/inferences should be self evident, or at least vacuous. The second is that I take the position that true means provable wrt a logic, always, no exceptions. So on matters of falseness, I take it to mean "provable that no proof exists" (or at least "if it's provable" that no proof exists), consequently, that inference $A \lor \lnot A$ means is that assumption that for every statement, it must either be provable or there must be a proof that it isn't provable... $\endgroup$
    – DanielV
    Oct 13, 2016 at 1:00
  • 1
    $\begingroup$ ...and that's a pretty absurd thing to assume to me, I'd even go far enough to call that kind of axiom "arrogant". $\endgroup$
    – DanielV
    Oct 13, 2016 at 1:01
  • $\begingroup$ @DanielV Interesting. I find 0. (((A $\implies$ $\bot$) $\implies$ $\bot$) $\implies$ A) strange, because from what I've seen most axioms used for classical logic and intuitionistic logic aren't particular in that if we can only change the variables, we will not find anything more general which is also a tautology. But, with just one substitution, from the tautology 1. (((A $\implies$ B) $\implies$ $\bot$) $\implies$ A) we can get the above axiom. The set of all four substitutions using $\top$ and $\bot$ of 1. contain the two subset of similar substitutions of 0. $\endgroup$ Oct 13, 2016 at 2:12

You must log in to answer this question.

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