This post is really about logic, but I use the stock market to motivate what I have found to be a challenging topic.

The law of excluded middle (sometimes shortened to simply: “Excluded middle”) is a tautology in classical logic. A tautology is a statement that is always logically true. I give examples to show excluded middle in action:

“Either it is raining now, or it is not raining now.” “I drove here or I did not drive here” “I need dental work or I do not need dental work”

I can go on forever, but we may generalize this by simply saying that if \( P \) is a *proposition* then either \( P \) is true, or it is not true.

It may seem like such a basic and foundational rule of logic, but there are systems of logic which actually do not allow excluded middle in this generality. One such system is intuitionistic logic. Intuitionism does not *deny* excluded middle, it simply does not admit it as a tautology - thus it’s entirely possible that one could prove special cases of excluded middle in intuitionstic logic, a fact I will revisit later.

It took me a long time of struggling to understand why we would ever avoid excluded middle. It seems so blatantly obvious, and what’s more it is extremely useful in mathematical arguments. After working with an intuitionistic proof system I have developed some intuition for this (pun not intended!). I would like to share my insights here. My basic insight is that intuitionism allows excluded middle when it is *informative and productive information* and doesn’t allow it otherwise. I will clarify what I mean by this now.

But I promised stock market applications, so I give first an algorithm to make infinite money using the law of excluded middle.

On the stock market we may purchase a stock with our own money or by way of loan (using the stock as collateral). The former situation is called going *long* on a stock and the latter situation is called going *short* on a stock. When we go long on a stock we hope its value goes up, so that when we sell it we make a profit. When we go short on a stock we hope its value goes down so that when we exchange it back for its original value as collateral, we again profit.

With that terminology in mind, let’s define an algorithm that we run every day for a year to either go long or short on a company’s stock - let’s call the company X. Define the proposition \( P \) to be the statement “X’s stock value will be lower than today’s value in one year.” In standard logic we have the law of excluded middle, so we know that either \( P \) is true or it is not true. Thus we proceed by two cases

- Case \( P \) is true: Go short on stock X today, sell in one year.
- Case \( P \) is false: Go long on stock X today, sell in one year.

Ok I stretched the truth a little bit here. This only guarantees that we don’t lose money, but that situation only occurs if the stock never changes in value. Otherwise this generates positive revenue.

Note: you probably already realized this algorithm is silly, but arguments like this actually do appear in classical logic with excluded middle. The intermediate value theorem is often proved using a very similar argument to the above “stock picking” algorithm, and for that reason it has the same outcome of being “true, but not useful.” This situation can be rectified, see my previous post on how to make it constructive.

Algorithm 1 is optimistic about what we can reasonably know about the future value of a stock. The problem is that we assert the truth of a statement without providing any evidence for it. Excluded middle is a way to construct “true” statements for which we have no evidence. That is fine, but the statements which come out of it tend to be unuseful and uninformative - and we can’t use them in algorithms (as above example illustrates).

To make logic maximally useful for computation, intuitionistic logic does not allow the general law of excluded middle.

If you have a proposition \( P \) you only know its truth if it is accompanied by a proof (often called a “witness” in logic circles). Thus the above “algorithm” does not work when we restrict ourselves to intuitionistic logic, because there is no way to prove the future value of a stock (we may estimate it and provide strong evidence for our *belief* that it will be a particular value, but we can’t guarantee it will realize that value).

More generally we can not prove the law of excluded middle using intuitionistic logic, becuase propositions can potentially be very degenerate like the example of \( P \) I gave above.

That said, we can prove *special cases* of excluded middle. Generally speaking this is possible when the contents of the proposition involve things we may easily compute over. Integers are a good example: “For every integer \( m \) either \( m=1 \) or \( m \neq 1 \)” is true in intuitionsitc logic, because computation over integers gives us a concrete proof procedure to follow that can take any \( m \) as input and decide whether it is \( 1 \) or not.

My background in math is very classical. I used and abused the law of excluded middle to prove many important theorems for my graduate studies, some of which ended up foundational both to my masters thesis and my PhD thesis. I started learning intuitionstic logic in order to utilize programming languages like Coq, which allow me to write mathematical algorithms and prove rigorously that they do the right thing (but Coq very strictly requires you to use Intuitionstic arguments). I will continue to post as I learn more.

I don’t mean this as an attack on classical logic, but just to clarify some of my thoughts on intuitionism.