In constructive mathematics even very small sets can be quite a bit more interesting than in classical mathematics. Since you will not believe me that sets with at most one element are very interesting, let us look at the set of truth values, which has “two” elements.

A *truth value* is represented by a sentence, such as `2 + 3 = 5` or `forall x in R exists n in N . x < n`. (Recall that there are no free parameters in a sentence; when we do allow free parameters we speak of *propositions*, so `x^2 + y^2 = z^2` and `exists x in R . x^2 = y` are propositions, not sentences). Sentences `p` and `q` represent the same truth value if they are logically equivalent. The set of all truth values is usually denoted by `Omega`.

How many elements does `Omega` have? The constants `TT` and `_|_` which represent truth and falsehood, respectively, are truth values. So we have `TT in Omega` and `_|_ in Omega`. That’s two elements. In classical logic, these are the only two, by which we mean that every `p in Omega` is equal either to `TT` or to `_|_` (because either `p` or `not p`). In constructive logic, however, this is not the case. But this does not mean there is a third truth value, which is different from both `TT` and `_|_`! How can that be? In order to explain this properly, we must be careful about what it means for a set to have “two elements”: For a set `A`, say that:

*`A` has**two elements in the strong sense*if there are `x, y in A` such that `x != y` and, for all `z in A` either `z = x` or `z = y`.*`A` has**two elements in the weak sense*if there are `x, y in A` such that `x != y` and, for all `z in A` it is not the case that `z` is distinct from both `x` and `y`.

To a classically trained mind there is no difference between the two senses of having two elements. Computationally speaking, however, there is a difference:

- `A` has two elements in the strong sense if we can compute `x in A` and `y in A` such that `x != y`, and there is an algorithm for deciding, given any `z in A`, whether `z = x` or `z = y`.
- `A` has two elements in the weak sense if we can compute `x in A` and `y in A` such that `x != y`, and there is no `z in A` that is distinct from both `x` and `y` (but there may be no algorithm for deciding, given `z in A`, whether it equals `x` or `y`).

Clearly, having two elements in the strong sense requires more (a decision procedure) than having two elements in the weak sense. In classical logic `Omega` has two elements in the strong sense. In constructive logic it has two elements in the weak sense, which we can prove as follows. Take `x = TT` and `y = _|_`. Given any `z in Omega` we must prove `not (z != x and z != y)`, which is logically equivalent to `not (not z and not not z)`, which is true (exercise, someone post a solution please).

Does this mean that constructive logic denies that `Omega` has two elements in the strong sense? No, it leaves the question unanswered, because constructive logic is “backward compatible” with classical logic.

You may have been thinking all along that `Omega` is the same thing as the type `bool`

that many programming languages have. This is not the case. First of all, unless your programming language is very limited, `bool`

has* **three* elements: `true`

, `false`

and “undefined”, which is represented by a diverging expression such as `while true do done; true`

. But even if we discount the udefined value, `bool`

is only a subset of `Omega`, namely the set of *decidable* truth values, which is usually denoted by `2`:

`2 = {p in Omega ; p or not p}`.

What are the elements of `2`? Since `TT or not TT = TT or _|_ = TT` and `_|_ or not _|_ = _|_ or TT = TT` we have `TT in 2` and `_|_ in 2`. And given any `p in 2`, we know that `p or not p`. If `p` then `p = TT`, and if `not p` then `p = _|_`. We have proved that `2` has two elements in the strong sense.

To add to the confusion, there is also the set of classical truth values,

`Omega_c = {p in Omega ; p iff not not p}`.

It consists of those truth values that satisfy the rule Reductio ad Absurdum (proof by contradiction).

Since `not not TT = not _|_ = TT` and `not not _|_ = not TT = _|_` we see that `TT in Omega_c` and `_|_ in Omega_c`. We thus have a chain of inclusions

`2 sube Omega_c sube Omega`.

Having three possibly distinct sets, all of which have “two elements”, arranged like this seems useless and unnecessarily complicated. But this is really quite useful, actually. The smallest one, `2`, is the datatype `bool`

that we all know from programming. The middle one, `Omega_c`, is “classical logic sitting inside constructive logic”. So even though we might not accept classical logic, we still have it at our disposal. The largest one, `Omega`, is useful because, well, because it is the set of truth values.

Your brain may still object to all of this. In classical mathematics, `2 = Omega_c = Omega`, end of story. While you were taught in school that this is the case, it is not what you personally believe, at least not if you are a programmer. Remembering that `2` is the datatype `bool`

, the assumption `2 = Omega` means “we can compute with truth values”. If this is really so, we should be able to write programs that compute the basic logical operations on `Omega`, yes? And so indeed logical disjunction, conjunction and negation are usually easily available as operations in typical programming languages. But let us not forget that `forall` and `exists` are also logical operations. Why are they not available in typical programming languages? If you are correct in your belief that `2 = Omega`, you should be able to write a program that takes as input a boolean function `f : NN -> 2` and outputs the truth value `forall n in N. f(n)`. Can you do it?

This was definitely the most striking fact I remember from my class on constructive set theory that I took as an undergrad (when Michael Rathjen was visiting Stanford). All I remembered in particular was that if the instance of the powerset axiom for a set of one element was true, then the entire powerset element would be. Thanks for explaining just what’s going on in more detail!

What easwaran is referring to is this. Let `1` be a one-element set. If the powerset `P(1)` exists then all powersets `P(X)` exist. Actually, this statement depends a bit on the details of the other axioms that you might have. I suspect Michael Rathjen taught CZF or something similar, which had the (strong) collection axiom and enough separatation to prove “for every sets `X` and `Y` the set of functions `X -> Y` exists”. From this yoou get arbitrary powersets by noticing that `P(X)` is in bijective correspondence with `X -> P(1)`.

But can you write a program that takes as input a boolean function `f : NN -> 2` and outputs the truth value `forall n in NN. f(n)` for some `Omega` where `2 != Omega`?

Hi Andrej (long time no see)…being a “classically trained” (sort of) mathematician who is living in a two dimensional world, here is how I have interpreted (over time) constructive logic, especially as relates to this very insightful discussion of 2, as well as PeterMcB’s comments on LEM. I’m going to intentionally state this to be difficult, but I’m truly curious what a constructivist would say:

“Constructive logic is classical logic + decidability. Basically, take good old classical logic, and throw out any part that, if implemented on a computer, might be undecidable.”

If this is true, then I don’t really see the point….why mess with logic when we can just discuss things in terms of TMs. If this is false, then please explain the difference. And if this is something other than true or false, then I’m totally lost :).

Two-valued propositional logic is fairly easy to implement. It seems to me that the logical operations “forall” and “there_exists” belong to predicate logic. This is more complex but still manageable with well-defined, finite domains. The difficulties seem to lie in infinite domains, such as the natural numbers.

But if for whatever reason, two logical values aren’t enough, it would seem only natural to try the next step…three.

Let me first answer to lukeb. Can we write a program that takes `f:NN->2` as input and outputs the truth value of `forall n in N. f(n)`, but we do not require that the output value is in `2`, but rather in `Omega`? The problem with this is that it is far from clear in what way `Omega` is a datatype in a programming language. In Martin-Löf type theory, which is a kind of super programming language, `Omega` is not a datatype but rather the kind of all datatypes! In a “real” programming language, `Omega` does not exist.

However, lukeb’s question still stands, and is a good one. Can we write `forall` if we change the underlying type of booleans? The answer is interesting and requires an entire post to the blog :-)

Next, Hal (hello!) asks whether he is correctly interpreting constructive mathematics to mean “those things that can be computed” within the realm of classical mathematics. The answer is essentially “yes”, with the caveat that this is not the only possible way of

interpretingconstructive math (for this is what Hal is doing, he is translating back into classical mathematics). Even more subtly, which things turn out to be valid in your interpretation depends on what exactly you mean by “implemented on a computer”. With which programming language? (It matters!) This also requires an entire post to the blog.Thad suggests that maybe we can have three-valued logic and get `forall n in NN` that way. An important point I wanted to make was that it is a bad idea to think of constructive logic as being “three”-valued, since `Omega` has two elements in the weak sense (i.e., has no more than two elements). A better way of doing what Thad is suggesting would be not to try to get a third truth-value in, but to find a suitable subset `S sube Omega` which does the job. Such a subset, which will have to be larger than `2`, will have two elements in the weak sense.

Actually, I don’t think having three logical values has much to do with getting `forall n in NN`. Rather, it has to do with the need to distinguish “two in a weak sense” and “Two in a strong sense”. This, it seems to me, is an elaborate cirumlocution needed to keep some form of the law of the excluded middle while making a distincion between “True” and “provably true”.

But this same kind of distinction can be made far more easily by rejecting the Law of the Excluded Middle as a universal law applying to all propositions and instead treating it as a contingent “principle” which applies to some propositions but not others. But this may not be the best place for this discussion.

I disagree with the premis of this post. It clearly the case that the cardinality of the set of equivalence classes of logically equivalent sentences is greater than two. Even after you mod out by the axioms of ZFC, you still have sentences such as CH and Con(ZFC) which sit strictly between âŠ¤ and âŠ¥. In fact this set forms a rich boolean algebra in classical logic.

The proof that ¬(¬A ∧ ¬¬A) is straight-forward. Assume that both ¬A and ¬¬A are provable. Then applying the first to the second we get a proof of âŠ¥ as required. The proof in Coq is:

I am not going to reply to every comment here, but please do not take that as a sign of my agreeing or disagreeing with you. This blog is not intended to be a tutorial in logic. I shall also write more specialist topics.

Reply to Thad: you cannot have three logical values. There is a proof of this. And if you read my post again, you will discover that I do reject the Law of Excluded Middle, and I do tell you how you can regain it by considering only the decidable propositions.

Reply to roconnor: you are confusing syntax and semantics. I was very careful to say that a truth value is represented by a sentence, but did not claim that

everytruth value can be represented by a sentence, which is an assumption implicit in your post. The Lindenbaum algebras you mention are made up of only those truth values that are definable, i.e., represented by some expression in the logic. Also, truth is not the same thing as provability. One last remark: what makes you think that in constructive mathematics every set has a cardinality?I have understood the law of the excluded middle as having two classically equivalent formulations: bivalence (p v ~P) and noncontradition ~(p & ~p). It appears to me that you are rejecting bivalence but accepting noncontradiction.

I’m astonished to learn that I cannot have three logical values, since Lukasieiwicz invented his 3-valued logic in 1920, and I’ve been working with it for some 20 years myself. Could you reference the proof?

If you’re talking about the proof in coq, I believe this is likely to include some implicit assumptions that I might not accept.

You are correct. Bivalence is not valid in intuitionistic logic, whereas noncontradiction is.

There is a lot of confusion about what it means to have two-valued logic (which is why I wrote this post). Lukasiewicz’s three-valued logic is not a model of intuitionistic logic, because some rules of inference are not valid in it. I was not talking about just any arbitrary thing that anyone might call logic, but rather specifically about intuitionistic logic. But that does not matter since we can find models of intuitionistic logic which seemingly have “three values”, for example the topos of presheaves on the category consistig of two objects and an arrow between them. In fact, given any Heyting algebra `H` with as many points as you like, you can find a model of intuitionistic logic, namely the `H`-valued sets, such that `Omega` is the set `H` (with a suitably defined `H`-valued equality predicate). But now it is important not to confuse the question “How many points does `H` have?” with the question “

Insidethe model, how many points does `Omega` have?”. Inside the model you can prove the validity of the statement `not exists p in Omega . (p != TT and p != _|_)`, but in the metatheory you can easily find a Heyting algebra `H` with more than two points. Please do not confuse a theory with meta-theory.The failure of many rules of inference does appear to be of the strongest arguments against Lukasiewicz 3-valued logic. But apparently no one has noticed that it’s possible to develop his logic in a way that does establish these rules of inference given certain reasonable conditions. My results have some features that are much like intuitionism. Since I’m an amateur with radically unorthodox ideas and not an expert on intuitionistic logic, I’m interested in comparing them. Please bear with me.

1. You said “If you are correct in your belief that `2 = Omega`, you should be able to write a program that takes as input a boolean function `f : NN -> 2` and outputs the truth value `forall n in N. f(n)`. Can you do it?” I can, if the theory is decidable, like ‘Presburger Arithmetic’ and the ‘Tarski’s axioms of Euclidian Geometry’

2. Another option of existing more than two truth values on `Omega` is when there are independent sentences on the theory, like the ‘Goodstein’s theorem’ on ‘Peano axioms’

Dear Yoav, the options you are mentioning are not valid within the context of this discussion.

1. Preburger arithmetic is a very limited subset of Peano arithmetic which does not even contain multiplication. When we speak of

naturalnumbers we mean Peano arithmetic. So, you have to consider all functions `f : NN -> 2` definable in Peano arithmetic, and it is impossible to decide whether such a function in general will always output `1` (actually, this already cannot be done for primitive recursive functions, which are a small subfamily of all number-theoretic functions). To put it in another way, of course by changing the assumptions you can draw a different conclusion.2. Tarski’s axioms are for real closed fields, not natural numbers. The set of natural numbers is not definable in Tarski’s theory. So your second remarks is not relevant because I was talking about function `NN -> 2`, not reals.

I’m a little late to the party, Andrej, but I wanted to ask….

In an intuitionistic type theory (say, HTT), Bool is clearly the strongly 2-elemented type.

Does this mean that Prop (the universe containing the unit type and the empty type) would be the weakly 2-elemented type? Wouldn’t Prop also be the subobject classifier?

Yes, in type theory $\mathtt{Bool}$ is the type with two elements that can be discerned, i.e., $\mathtt{True} \neq \mathtt{False}$ and for all $p : \mathtt{Bool}$ either $p = \mathtt{True}$ or $p = \mathtt{False}$.

But you got $\mathtt{Prop}$ wrong. First of all, it is not clear what you mean when you say that “$\mathtt{Prop}$ is the universe containing the unit and the empty type”. It is crucial to write down a precise definition. For example, if by this you mean $\mathtt{Prop} = \Sigma (t : \mathtt{Type}), (t = \mathtt{unit}) + (t = \mathtt{empty})$ then you have just defined something equivalent to $\mathtt{Bool}$. But that is not what $\mathtt{Prop}$ is in type theory. Instead, it has to be defined as those type which have at most one element: $$\mathtt{Prop} = \Sigma (t : \mathtt{Type}), \Pi (x y : t), x = y.$$

Now you cannot show that $\mathtt{Prop}$ is equivalent to $\mathtt{Bool}$, and indeed there are models where it is not. Lastly, you ask whether $\mathtt{Prop}$ is the subobject classifier ($\mathtt{Bool}$ of course is not, unless excluded middle holds). That depends on what you mean by “subobject” in type theory. There is a notion of subobject for which $\mathtt{Prop}$ is indeed a subobject classifier, namely $f : A \to B$ is a subobject if the homotopy fibers of $f$ are propositions in the above sense. In contrast, a pure propositions-as-types way of doing things would be to take every dependent sum as a subobject, in which case $\mathtt{Type}$ will be the subobject classifier.

A last word of warning: $\mathtt{Prop}$ is not a small type, i.e., it need not be contained in any universe. So it is a “large” classifier, and we have to keep this in mind when working with it.