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:
-
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?
-
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!
Best Answer
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.