Timeline for Cardinal Arithmetic, foundations and constructive math
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5, 2012 at 15:51 | comment | added | Andrej Bauer | Yes, "constructive" mathematicians are concerned with practical computation, very much so. I happen to be concerned with practical computation. But I am not a constructive mathematician. | |
| Nov 5, 2012 at 15:50 | comment | added | Andrej Bauer | Any topos whose object of truth values has more than two truth values will contain freakish subsets of the singleton. Consider the Grothendieck topos $Sh(\mathbb{R})$ of sheaves over $\mathbb{R}$. The subsets of the singleton $\lbrace 0 \rbrace$ correspond to the open subsets of $\mathbb{R}$, but only two of those, $\emptyset$ and $\mathbb{R}$, are finite. There is also a computational reason why you should not expect subsets of a finite set to be finite. Consider the intersection of a c.e. set and a finite set. Why do you expect to be able to produce a finite list of its elements? | |
| Nov 5, 2012 at 15:09 | comment | added | Najdorf | Also above I said that my idea of constructivism is that it should be practically computable (I mentioned MP in addition to the law of excluded middle). I have no idea if this is even a topic of discussion in constructive/intuitionist circles but if you look at it from a programming point of view it is the most natural definition. | |
| Nov 5, 2012 at 15:07 | comment | added | Najdorf | Alright that example clarified things a bit. But I am fine with unprovabally finite subsets of a finite set. My initial thought after reading your statement was that, there is a freakish model where a finite set had a non-finite subset (that would is stupid but from my experience you can't just call something obviously stupid and move one hence my confusion). | |
| Nov 5, 2012 at 13:49 | comment | added | Andrej Bauer | @Najdorf: only you can know whether the thing you call "real subset" can be formalized. I suspect you means something like "decidable subset". That is insufficient to do mathematics. Let me give you an example which should worry you. Let $p : \mathbb{R} \to \mathbb{R}$ be a polynomial. Consider the set of its zeroes $Z = \lbrace x \mid p(x) = 0\rbrace$ and then the intersection $Z \cap \lbrace 0 \rbrace$. It is a subset of $\lbrace 0 \rbrace$. It is unprovable intuitionistically that $Z \cap \lbrace 0 \rbrace$ is finite. So, in your view that set must not be "real". But then what is left? | |
| Nov 5, 2012 at 9:18 | vote | accept | Najdorf | ||
| Nov 5, 2012 at 8:57 | comment | added | Najdorf | @Andrej: I am very sorry for the lack of clarity, I have not thought about these things and strangely enough I think I use constructive in a stronger form than anyone else here which just worsens the matters. The subset/Random Variable is not a real subset, so if the non-finite subsets of a finite set are only of that type then I am fine with the original statement. The next question is whether what I call real subset can be formalized in any sense or not ... | |
| Nov 4, 2012 at 23:57 | comment | added | Andrej Bauer | @Guillaume: see how people get confused by the Brouwerian counterexamples? It is best not to use them. It legitimizes funny talk about "future" and "random variables". | |
| Nov 4, 2012 at 23:44 | comment | added | Andrej Bauer | @Najdorf: the same criticism applies to classical mathematics. We are not forming any strange subsets, only ones that classical mathematicians do too. You keep changing the rules of the game every time we tell you something you do not like. It does not work that way, we are not cheating, that is how things are. Lastly, statements like "your subset is different things in the future, it is essentially a random variable" do not mean anything. You have to make them mathematically precise. I was not basing my arguments on a notion of time or randomness. My proof is water tight. | |
| Nov 4, 2012 at 23:01 | comment | added | Najdorf | @Andrej, @Guillaume: In those cases I would take issue with the way you define the subsets which depend on an odd black box. What you have is not a fixed subset, it can be different things in the future, it is essentially a random variable. | |
| Nov 4, 2012 at 22:45 | comment | added | Andrej Bauer | @Robert: you are welcome. If you are really combining ordinal numbers and constructive math, I definitely recommend reading Paul Taylor's JSL paper on the subject. | |
| Nov 4, 2012 at 22:12 | comment | added | David Roberts♦ | Thanks, Andrej. It's relevant for a possible constructive extension of a theorem I'm working on. | |
| Nov 4, 2012 at 20:58 | comment | added | Andrej Bauer | Exactly, and also it is misleading to offer specific statements whose status is yet unknown but could be resolved in the future. This makes it look like you are confusing the truth value of a statement with our knowledge of it. In fact, this is precisely the reason why I find Brouwerian counter-examples to be a really poor way of explaining intuitionistic mathematics. There is a difference between something being true and us knowing it is true, and Brouweian counter-examples ask you to forget about the difference. | |
| Nov 4, 2012 at 16:14 | comment | added | Guillaume Brunerie | @Andrej: I was assuming that if someone believe that GHC either holds or not then he probably also believe in excluded middle anyway. But I see your point, one can know that excluded middle is constructively problematic but not recognize a particular instance of it. | |
| Nov 4, 2012 at 14:58 | comment | added | Andrej Bauer | @Guillaume: in my experience the Brouwerian counterexamples do not help explain anything to classical mathematicians. You see, if you already believe that GCH either holds or not, then your reasoning is vacuous. It is better to provide a proof that some statement implies excluded middle. Here: a finite set is either empty or inhabited (it is bijective to a unique $[n]$, and so se just observe whether $n = 0$). Consider the subset $\lbrace 1 \mid p\rbrace$ where $p$ is any truth value. If this set is empty then $\lnot p$, if it is inhabited then $p$. Therefore $p$ or $\lnot p$, excluded middle. | |
| Nov 4, 2012 at 14:54 | comment | added | Andrej Bauer | @Najdorf: (3) I am not saying that all intuitionists accept all axioms I listed. Actually, the constructive mathematicians I know are mostly convervative -- they do not want to assume any extra axioms, except perhaps dependent choice. In any case, constructive mathematics is a base on top of which one can usefully explore other kinds of mathematics, so it is not unusual to consider various axioms out of sheer curiosity. You don't have to go all philosophical all the time. | |
| Nov 4, 2012 at 14:52 | comment | added | Guillaume Brunerie | @Najdorf What is unreasonable about the fact that a finite set might have non-finite subsets? A finite set is a set $A$ such that there exists (constructively!) a natural number $n$ and a bijection $[n]\simeq A$. Now consider the subset $X$ of the singleton $\{0\}$ such that $X$ contains $0$ if and only if GHC holds. Classically $X$ is either empty or equal to $\{0\}$, but constructively there is no way to find a bijection between $X$ and some standard finite set $[n]$. A set which is not finite does not need to be infinite either. | |
| Nov 4, 2012 at 14:52 | comment | added | Andrej Bauer | @Najdorf: (1) the base system does not matter so much, it could be higher-order intuitionistic logic (i.e., the internal language of a topos), or some variant of intuitionistic set theory. (2) I agree that having an embedding $\mathbb{R} \to \mathbb{N}$ is unreasonable, but it is unavodiable that a finite set should have non-finite subsets. In fact, the statement "every subset of a singleton is finite" implies excluded middle. | |
| Nov 4, 2012 at 14:50 | comment | added | Andreas Blass | @Najdorf: If you're going to arbitrarily declare some constructively possible phenomena "not reasonable", then you should give some hints about how much classical mathematics your notion of "reasonable" includes. We now know that it includes the non-constructive principles that $R$ can't embed in $N$ and that subsets of finite sets are finite, but we have no idea what else it might include. So people trying to answer your question are left to simply guess what you're willing to admit as "reasonable". | |
| Nov 4, 2012 at 14:49 | comment | added | Andrej Bauer | @David: a realizability topos validates "trichotomous ordinals form a set", see arxiv.org/abs/1201.0340 | |
| Nov 4, 2012 at 11:01 | comment | added | Najdorf | Alright that was helpful but I still have some issues: (1) When you say there are models for your first list of statements, what is the base system of constructive math you are working with? (2) Throughout the whole discussion I am assuming a degree of reasonableness, an axiom stating the fact that a finite set can have non-finite subsets or that we have an embedding $\mathbf{R} \to \mathbf{N}$ are not resonable (3) I might be mistaken but I thought that intuitionists did not like Church's thesis ... | |
| Nov 4, 2012 at 7:21 | comment | added | David Roberts♦ | Under what assumptions do the ordinals form a set? | |
| Nov 4, 2012 at 4:15 | history | answered | Andrej Bauer | CC BY-SA 3.0 |