I have rewritten this question, in hopes of conveying its content more clearly (I have adopted a quotation convention that is important to carefully follow):

Ideas I believe are correct (in classical logic):

$A: = \text{'A' is a true statement}$

$\neg A: = \text{ 'A' is a false statement}$

$A \rightarrow B := \text{ 'A} \rightarrow \text{B' is a true statement}$

$\neg ( A \rightarrow B):= \text{ 'A} \rightarrow \text{B' is a false statement}$

$A \land B := \text{'A} \land \text{B' is a true statement}$

$A \lor B := \text{'A } \lor \text{B' is a true statement}$

For the purposes of this discussion, let the object in single quotes denote a statement that has no initial truth evaluation unless explicitly stated. For example, $\text{'A'}$ is neither false nor true. (For example, $x \gt 2$). However, if I say $\text{'A' is true}$, then $\text{'A'}$ is assigned a truth value of $\text{true}$.

When one is asked to prove $A \rightarrow B$, the standard method is (typically) to assume $A$ and arrive at $B$. An equivalent way of asking for this proof is "Under what conditions do we have $A \rightarrow B$ ?"

One can demonstrate that:

$ \text{'A} \rightarrow \text{B'} \quad$ and $\quad '\Big[\neg \text{A} \land \big ( \text{B} \lor \neg \text{B} \big ) \Big ] \lor \Big [ \text{A} \land \text{B} \Big]'$

have the same truth tables. This means that $A \rightarrow B$ and $\Big[\neg A \land \big ( B \lor \neg B \big ) \Big ] \lor \Big [ A \land B \Big ]$ occur together.

From the Law of the Excluded Middle (a classical logic principle), we know that $\text{'B} \lor \neg \text{B'}$ is a tautology. For the same reason, so is $\text{'A} \lor \neg \text{A'}$. If we assume $\neg A$, we immediately prove $\Big[\neg A \land \big ( B \lor \neg B \big ) \Big ] \lor \Big [ A \land B \Big ]$, by virtue of the $\text{'B} \lor \neg \text{B'}$ tautology. Conversely, when we assume $A$, we need to demonstrate (prove) that we can arrive at $B$ in order to assert $A \land B$, which will give us $\Big[\neg A \land \big ( B \lor \neg B \big ) \Big ] \lor \Big [ A \land B \Big ]$.

My first question is why do I have to go to the trouble of proving $A \land B \quad$ if $\quad \neg \text{A} \land \big ( \text{B} \lor \neg \text{B} \big )$ just as well gives me $A \rightarrow B$ ?

My only guess is that exercises that ask "Prove $A \rightarrow B$" are actually saying "If $A$, prove $A \rightarrow B$." Where "If $A$" is interpreted as "Begin your argument with $A$ as an assertion."

My second question is: the entire above understanding of an "implication" relied on truth tables and the Law of the Excluded Middle. Intuitively, I would think that the entire notion of a truth table depends on the Law of the Excluded Middle (otherwise, we could not even create our traditional bivalent depictions of a truth table). As such, how does one interpret "prove $A \rightarrow B$" in a intuitionistic/constructive logic setting, where the Law of the Excluded Middle is elided.

  • 5
    $\begingroup$ What precisely is the distinction between $\implies$ and $\to$ that you are making? In any case, there is absolutely nothing wrong with having both $A\to \neg B$ and $A\to B$; that just means that $A$ has to be false. $\endgroup$ Apr 28, 2021 at 5:53
  • 1
    $\begingroup$ Comment to the beginning; YES, every time in the context of a mathematical proof we assert a statement $A$, we are judging it TRUE, either because it is an axiom or because we have a proof of it (it is a theorem). $\endgroup$ Apr 28, 2021 at 9:11
  • 1
    $\begingroup$ And YES, if we assume $A$ and prove $B$, this proof amounts to proving $A \to B$. If $A$ has been already proved (axiom or theorem), we have instead a proof of $B$. $\endgroup$ Apr 28, 2021 at 9:13
  • 1
    $\begingroup$ "My second question is...", more or less YES. The truth table holds in classical logic, with LEM. In Intuitionistic Logic LEM does not hold, which means not that every use of LEM is forbidden (for e.g. finite collections it is safe) but some use of it are forbidden. Tipically, Intuitionism rejects the proof of the existence of an object $a$ satisfying property $P$ on the ground that the assumption that all objects are $\lnot P$ produces a contradicition. This is (in a nutshell) the gist of "constructive": the proof must "produce" a witness of $P$. $\endgroup$ Apr 28, 2021 at 9:18
  • 2
    $\begingroup$ Disagree; a statment "if A, then B" is proved assuming $A$ and deriving (with some "logical correct move") $B$. Having done this, we are licensed to assert $A \to B$. If $A$ is not assumed but it has been already proved, we prove $B$, fullstop. Obviously, every proof needs some starting point; this is the reason to be explicit about the context, i.e. the theory (axioms) we are working with. Pythagoras theorem is a theorem of Euclidean geometry, i.e. it holds in every "environment" where Euclid's axioms hold. $\endgroup$ Apr 28, 2021 at 9:29

1 Answer 1


Regarding your first question: Yes, we have the equivalence $$ A \rightarrow B ~\Leftrightarrow~ [¬A∧(B∨¬B)]∨[A∧B] $$ So in order to show $A \rightarrow B$ you can instead try to prove that either $¬A∧(B∨¬B)$ or $A \land B$ is true. In some concrete cases however $¬A∧(B∨¬B)$ (which is equivalent to $\neg A$) will simply be false and so the only remaining chance to show that the $\lor$ is true, is to show that $A \land B$ is true.

Maybe I can also illuminate the intuition behind $\rightarrow$ in a constructive logic.

Let's say you are in a functional programming class and one of the exercises of your assignment sheet reads

Let A and B be types.

(1) Assuming there is one element b of type B, write a function with type A -> B.

(2) Write a function with type ((A -> A) -> A) -> A). $~$

For (1), since B has at least one element b, we can just write a function* λ (a : A) => b sending anything to b : B.

In (2) you assume that you are handed a function (A -> A) -> A and you need to produce a value of A. Luckily it is easy to program the identity function id := λ (a : A) => a giving you the solution λ (g : (A -> A) -> A) => g(id) or written out: λ (g : (A -> A) -> A) => g ( λ (a : A) => a )

Thus far pretty ok stuff. However the exercise continues with

(3) Write a function ((A -> B) -> A) -> A

(4) Write a function ((((A -> B) -> A) -> A) -> B) -> B

and you can consider (3) as a joke by whoever made the exercise. You can try for yourself that it is not possible to write down any expression which would produce a function like this. However (4) can be done! (Try it! It's quite a challenge)

Now what am I trying to convey with the above?

I am trying to say that in constructive logic you can consider any proposition $A$ that you know nothing about as a type A that you know nothing about. And trying to prove $A \rightarrow B$ should then be considered as trying to write/program a function f : A -> B.

Really, this is properly known as "propositions as types" and is an instance of the Curry-Howard–de Bruijn Correspondence; which in the above case is saying that

There is a function with type ((A -> B) -> A) -> A if and only if there is a proof of $((A \rightarrow B) \rightarrow A) \rightarrow A$ in intuitionistic logic.

However $((A \rightarrow B) \rightarrow A) \rightarrow A$ is known as Peirce's law and can be shown (in intuitionistic logic) to be equivalent to the law of excluded middle and is therefore not provable in intuitionistic logic.

Regarding your second question: Your intuition about the law of excluded middle being responsible for the two valued nature of classical logic is quite on point. At least in some proof assistants with an underlying constructive logic, adding LEM turns all propositions either true or false.

*Two things to note:

  • λ (x : X) => e is to be read as a function taking one argument of type X and putting it into some expression e possibly containing x. (For a proper explanation of what is meant, see here for more)
  • It is important that we know nothing about A. Once you have some element of A, everything is trivial. Just as $C \rightarrow A$ is easy to prove if you already know that $A$ holds.

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