A few questions about intuitionistic mathematics

I have to write a paper on Intuitionism for my Philosophy of Science class and I'm struggling with a few concepts I have encountered in my self-study.

The (intuitive) characterization of valid intuitionistic inferences I am familiar with is given by the BHK interpretation. Let $\neg$ denote the strong negation as defined in H4, and $\sim$ denote the weak negation (i.e. $\sim P$ means no proof of $P$ has been found). This is probably a lot to ask for in only one question, but I'll give it a shot:

1. In this book it says that Gödel proved that every theorem of PA which does not involve the symbols "$\vee$" or "$\exists$" is also a theorem of HA, and given that every statement in classical logic is classically equivalent to one that does not contain those two symbols, we have that every theorem of PA has a version which is acceptable to the intuitionist.

• Is this not true in general, for example when dealing whith real numbers?
• Isn't it true that, in general, if a statement $P$ is classically valid, then $\neg \neg P$ is intuitionistically valid?
2. I was also wondering about which formulations of the Axiom of Choice are acceptable in an intuitionistic framework. The main result in this context is Diaconescu's Theorem, which states that in constructive set theory the full version of AC cannot hold, as it would imply excluded middle.

• First of all I am not confortable with the proof of such theorem: how can the sets $U$ and $V$ (defined in the Wikipedia page) be intuitionistically well defined, if we cannot, in general, assert $P \vee \neg P$? In the same book I was referring to before it says that $$b_n = \begin{cases} 0 \ \forall n \quad \text{if Goldbach's conjecture is true} \\ 1 \ \forall n \quad \text{if Goldbach's conjecture is false} \end{cases}$$ "does not define a sequence at all, because it does not tell us how to computes its terms" (page 126). So how can the sets $U$ and $V$ be well defined if $P$ is a statement we cannot prove or refute, like the Goldbach Conjecture?
• It says here that, even though the full AC is not intuitionistically acceptable "there are, however, certain restricted axioms of choice that are acceptable for the intuitionist", like the Axiom of Countable Choice or of Dependent Choice. But the choice used in Diaconescu's reasoning isn't only countable, it's finite! So how can the cardinality of the family of sets we are chosing from have anything to do with the intuitionistic validity of our choice principle?

Unfortunately, I haven't got the background in Logic and Set Theory to delve into too much technical detail, so I'm getting my information from not-too-technical philosophy books and Wikipedia and Standford Encyclopedia entries. If someone could explain in simple terms what I'm getting wrong that would be great.

This question came out even longer than I had planned and, of course, partial answers are also very much appreciated. Thank you very much for any help.

21/05/12 I got two very helpful answrs and, although I'm going to accept Kaveh's one since it addresses both 1. and 2., Carl's one was crucial to my understanding 2. I hope these answers get the upvotes they deserve, thank you both!

-
Regarding (2), you must be very careful. Diaconescu's theorem is a result about the internal logic of a topos, but there are other formulations of the axiom of choice and other models of intuitionistic "set theory". For example, in Martin-Löf's intuitionistic type theory, the axiom of choice is a theorem. See this article by Martin-Löf himself: 100 years of Zermelo's axiom of choice: what was the problem with it? – Zhen Lin May 18 '12 at 10:14
@ZhenLin Thank you, I found the article and plan on reading it soon. – Emilio Ferrucci May 18 '12 at 10:24
@EmilioFerrucci This post on the irrationality of $\sqrt 2$ may be relevant to your interests. It covers, in a simple example, some differences between the classical and intuitionistic school of thought. – process91 May 18 '12 at 13:39
@MichaelBoratko Thanks for the link. I do ha some familiarity with intuitionistic mathematics; the book I referred to in the question has a full chapter on it, and it is very well done. Do you have any particular reason to belive the link answers any of my questions? – Emilio Ferrucci May 18 '12 at 14:35
@EmilioFerrucci No, nothing in particular, just the first thing I thought of when reading your post :) – process91 May 18 '12 at 19:27

Gödel proved that every theorem of PA which does not involve the symbols "$\lor$" or "$\exists$" is also a theorem of HA

I think you are talking about Godel's negative translation

Is this not true in general, for example when dealing whith real numbers?

The theorem holds if the theory itself is closed under the translation and double negation of the atomic formulas are equivalent to them, then translation is identity over the part not containing "$\lor$" and "$\exists$".

Isn't it true that, in general, if a statement P is classically valid, then ¬¬P is intuitionistically valid?

No, we need to remove the constructive content from all internal parts, just doing at the outside will not suffice. (If you know Kripke models, then a double negation in the front means that the statement inside will be eventually forced i.e. constructively correct).

First of all I am not confortable with the proof of such theorem: how can the sets U and V (defined in the Wikipedia page) be intuitionistically well defined, if we cannot, in general, assert P∨¬P? [...] So how can the sets U and V be well defined if P is a statement we cannot prove or refute, like the Goldbach Conjecture?

I guess your question is "why we accept the axiom of specification as constructive?". These kind of confusions arise usually because people not familiar with constructive concepts try to interpret them classically. Different constructive theories use conceptually different but similar looking concepts and the difference is not visible when looking at them as classical objects. The best reference I know of that has a good treatment of these issues and explanation of what each of them means is Beeson's book "Foundations of Constructive Mathematics", 1980.

In this case you are using an argument about not-well-definedness of a number (not a sequence!, $n$ is not playing about role here) in constructive number theory to argue against about the well-definedness of a set in a particular set theory.

It can become even more confusing (for people not familiar with the fact that these theories might use conceptually different concepts), a constructive axiom about some concepts in a constructive theory may destroy the constructiveness of another theory. There is nothing wrong about each one, the problem is that the underlining concepts are different and each satisfy different constructive axioms. A good illustrative example is "functions" and "operations". If you want to know more about their difference check Beeson's book.

It says here that, even though the full AC is not intuitionistically acceptable "there are, however, certain restricted axioms of choice that are acceptable for the intuitionist", like the Axiom of Countable Choice or of Dependent Choice. But the choice used in Diaconescu's reasoning isn't only countable, it's finite! So how can the cardinality of the family of sets we are chosing from have anything to do with the intuitionistic validity of our choice principle?

Be careful about calling them finite, $U$ and $V$ are finite only if you have constructive proof of it, and here it would mean giving a natural number and a bijection between the set and that number. You are again mixing the classical views with constructive views and that can cause confusion.

Second thing is that you are not clear about the context. There quite a few axioms of choice, some of them may destroy the constructive content of a constructive theory if you are not careful about what are the real underlining objects they are talking about. The countable axiom of choice might be talking about countable "set" of subsets of natural numbers not general sets.

In summery,

• remember that there is not a constructive mathematics, there are a many constructive mathematics, and they disagree about the axioms,

• be careful when combining constructive axioms from different constructive theories, understand what kind of objects they are really taking about (what information is given when an object is given?) and understand what is the justification for constructiveness of the axiom about those objects, then check if that justification still applies to the objects in the theory you want to add the axiom to it.

-
Thank you very much for your lengthy answer. I understood most of it, but I still would like to ask you a couple of things: (1) Could you expand a little bit on what you mean by "we need to remove the constructive content from all internal parts"? When does Glivenko's Theorem hold? (I was under the impression it held for all propositions) (2) By "finite choice" I didn't mean $U$ and $V$ are finite, I meant $\{U,V \}$ was finite (it has two elements). If $U$ and $V$ are sets, I really can't see why countable choice shouldn't be... – Emilio Ferrucci May 20 '12 at 20:26
...applicable to the family of sets $\{U, V \}$. Everything else was was very clear :) – Emilio Ferrucci May 20 '12 at 20:27
@Emilio, 1) Glivenko doesn't work for first-orde (btw, the wikipedia article you linked to states this). 2) depends on what we mean by "sets", intuitively the sets should have enough structure so you can find an element of them from the information given to you about them. This might be a good example (and may not work really) but I think it can help with the point: assume I give you a very complicated set and only give you a non-constructive proof that it is not empty, how can you find an element of the set? – Kaveh May 20 '12 at 20:55
You can do it if it is a subset of natural numbers and the set membership is decidable by going over elements till you find one (this may need Markov Principle but let's not bother with it). Now if it is a set of real numbers and you are provided only with a nonconstructive proof of non-emptiness how can you find a real number in the set? (even here I should be careful about what we mean by real numbers, are we talking about recursive reals or general Cauchy reals or general Dedekind reals? What information is given by each real number? etc.) – Kaveh May 20 '12 at 20:56
The key point for handling quantifiers is just to use the right translation. For example see en.wikipedia.org/wiki/… . For propositional logic you can just put two negations in front but for first-order logic you have to be more thorough in double negating. – Carl Mummert May 21 '12 at 1:39

This is an answer to some of the questions from the OP.

• The set $\{U,V\}$ constructed in the proof of Diaconescu's theorem looks finite from a classical perspective. But the definition of "finite" is that there is a bijection with some natural number (this is true in both classical and constructive settings). Because the sets $U$ and $V$ are constructed in such a way that it is not known whether $U = V$ or $U \not = V$, there cannot be any constructive proof that such a bijection exists, because the bijection would let you tell whether the sets are equal. In fact the set $\{U,V\}$ is not finite (constructively).

• Diaconescu's theorem is particular to constructive set theory. In that theory, they allow comprehension axioms even when membership in the constructed set is not decidable. So for example they would accept $$W = \{ x \in \{1\} : \text{the Riemann hypothesis holds}\}$$ as a valid definition of a set. Of course they have no idea whether this set is empty, or whether it is $\{1\}$, because the Riemann hypothesis is an open question. There are other settings for constructive mathematics in which the set membership relation is always decidable; in those settings it is not possible to form sets like $W$ in the first place.

-
Thank you for your answer, I was missing the argument that explains why $\{U,V \}$ isn't constructively finite, which nicely clears up my doubts about the applicability of countable choice. It still seems strange that the axiom of comprehension isn't viewed constructively in constructive set theory, philosophically this seems to be equivalent to embraacing of set-theoretical realism.. I guess it's a compromise that had to be made. – Emilio Ferrucci May 21 '12 at 11:31
In the past I asked some experts in constructivism about this, and they indicated that a motivation for constructive set theory (IZF and CZF) was to resemble ordinary set theory as much as it could. Perhaps that helps explain the comprehension axioms. These theories do have the usual disjunction and numerical existence properties, which helps justify calling them "constructive"; see plato.stanford.edu/entries/set-theory-constructive – Carl Mummert May 21 '12 at 11:59
@Carl, Troelstra and van Dalen argue in their book that DP and EP are not sufficient to call a theory constructive. – Kaveh May 21 '12 at 13:52
@Kaveh: of course there are different concepts of what it means for a theory to be constructive. All that I said (intentionally) is that the presence of these properties helps justify calling IZF and CZF constructive. Different people can come to different conclusions about whether these systems are "really" constructive. – Carl Mummert May 21 '12 at 13:57
I also believe I remember that, although I don't have a copy of the book here. However, if any theory has those properties then it is, in a certain sense, "constructive". Another argument for the constructiveness of CZF is Aczel's interpretation of it into intuitionistic type theory. On the other hand, since IZF and CZF fail to validate the axiom of choice, they are in a certain sense "nonconstructive". Both Bishop and Martin-Lof argue that constructive systems will satisfy the axiom of choice (choice follows from the "very meaning of existence" as Bishop puts it). – Carl Mummert May 21 '12 at 14:09