The main hurdle for constructive mathematics is embedding a system as strong as ZFC or ZFC+large cardinals in type theory. This is not so difficult as compared to formulating Type Theory, and when such a system comes, people will use it.
I have a concern regarding the proof that Choice implies EM (from 10:00 to 17:00). For Choice to imply that a definite choice function f exists from {A, B} (as defined) to {0, 1}, sets A and B must be well-defined but, as their contents depend on whether p or not p, whether p or not p must be definite for those sets to be well-defined, which in turn requires EM. That is to say, the proof assumes EM. So, it seems to me that all that is proven is that on the assumption of EM, Choice implies EM, which is trivial.
***** You don't have to know what the content is but it has to be definite even if unknown. I.e. in this case, you don't need to konw whether p or not p, it must be definite whether p or not p, which implies Contradiction and EM. More later.
Thanks. As I see it, if you define a set in such a way that it is one if p is the case and another if p is not the case, and it happens that p neither is the case nor fails to be, your definition fails. If one rejects EM for p in the video, sets A and B are not well-defined and Choice does not apply. So, when you assume Choice applies to {A, B} in order to infer EM for p, you have previously assumed what you infer.
@@LaureanoLuna The sets don't depend on whether or not p, their definitions just depend on disjunction. The reasoning then after assuming Choice is of the form (P or Q), not P, therefore Q. So that doesn't assume EM either. What I found a bit odd that nobody mentioned in the talk is that the third case involves proof by contradiction
@@hywelgriffiths5747 I don't think you get my point. p can be a disjunction, that is irrelevant. The point is that without EM sets can be fuzzy because their defining conditions may fail to be true/false for some objects, so that assuming them to be definite implies assuming EM.
@@LaureanoLuna @Laureano Luna I think I'm beginning to glimmer what you're saying. I wasn't talking about p being a disjunction, just that the sets A and B are defined in terms of disjunction: {x in 2| x=0 OR p}. The proof assumes, I think, that p is a boolean, i.e. a value that can be one of two values. Is this what you say is equivalent to assuming EM?
The top part of the whiteboard (maybe two or three lines of text?) is missing. Anyone know if there are notes available somewhere that correspond to this talk?
I’m not a constructivist about math, but doesn’t the proof by cases that LEM follows from AOC assume LEM, given that you assumed f(A)=f(B) or not-f(A)=f(B), I don’t see how this is a constructive proof that LEM follows from AOC without having to already assume it.
Continuity is another matter. Continuity just means an academic condition affecting pure mathematics. That is academically acceptable, but does not exist in Nature, code, nor constructive mathematics. The lack of coherence is what dooms continuity. Physics, here, is just indicative, but code (by the Curry-Howard correspondence) and constructive mathematics are also determining. Conventional mathematics cannot stand, not being even intersubjective.
Great talk Andrej! too many people on the "anger" level still.
The main hurdle for constructive mathematics is embedding a system as strong as ZFC or ZFC+large cardinals in type theory. This is not so difficult as compared to formulating Type Theory, and when such a system comes, people will use it.
Category: comedy? ;)
Great talk, thanks for sharing!
it is above my head , cheers
Thanks for a great lecture, I've learned so much!
I wish I could hear the audience
I have a concern regarding the proof that Choice implies EM (from 10:00 to 17:00). For Choice to imply that a definite choice function f exists from {A, B} (as defined) to {0, 1}, sets A and B must be well-defined but, as their contents depend on whether p or not p, whether p or not p must be definite for those sets to be well-defined, which in turn requires EM. That is to say, the proof assumes EM. So, it seems to me that all that is proven is that on the assumption of EM, Choice implies EM, which is trivial.
***** You don't have to know what the content is but it has to be definite even if unknown. I.e. in this case, you don't need to konw whether p or not p, it must be definite whether p or not p, which implies Contradiction and EM. More later.
Thanks. As I see it, if you define a set in such a way that it is one if p is the case and another if p is not the case, and it happens that p neither is the case nor fails to be, your definition fails. If one rejects EM for p in the video, sets A and B are not well-defined and Choice does not apply. So, when you assume Choice applies to {A, B} in order to infer EM for p, you have previously assumed what you infer.
@@LaureanoLuna The sets don't depend on whether or not p, their definitions just depend on disjunction. The reasoning then after assuming Choice is of the form (P or Q), not P, therefore Q. So that doesn't assume EM either. What I found a bit odd that nobody mentioned in the talk is that the third case involves proof by contradiction
@@hywelgriffiths5747 I don't think you get my point. p can be a disjunction, that is irrelevant. The point is that without EM sets can be fuzzy because their defining conditions may fail to be true/false for some objects, so that assuming them to be definite implies assuming EM.
@@LaureanoLuna @Laureano Luna I think I'm beginning to glimmer what you're saying. I wasn't talking about p being a disjunction, just that the sets A and B are defined in terms of disjunction: {x in 2| x=0 OR p}. The proof assumes, I think, that p is a boolean, i.e. a value that can be one of two values. Is this what you say is equivalent to assuming EM?
The top part of the whiteboard (maybe two or three lines of text?) is missing. Anyone know if there are notes available somewhere that correspond to this talk?
Nice lecture, thanks.
So U-Way was just a crazy turtle after all. Great talk!
I’m not a constructivist about math, but doesn’t the proof by cases that LEM follows from AOC assume LEM, given that you assumed f(A)=f(B) or not-f(A)=f(B), I don’t see how this is a constructive proof that LEM follows from AOC without having to already assume it.
He explained why that's okay to do: equality is decidable in the naturals. He noted that you can prove this by induction.
Continuity is another matter. Continuity just means an academic condition affecting pure mathematics. That is academically acceptable, but does not exist in Nature, code, nor constructive mathematics. The lack of coherence is what dooms continuity. Physics, here, is just indicative, but code (by the Curry-Howard correspondence) and constructive mathematics are also determining. Conventional mathematics cannot stand, not being even intersubjective.
This is strictly not true, continuity is equivalent to Computable with an oracle (this is a basic result of Computable analysis).
Mathematicians "work"?