bio | website | dorais.org |
---|---|---|
location | Hanover, NH | |
age | ||
visits | member for | 5 years, 5 months |
seen | 7 hours ago | |
stats | profile views | 13,986 |
I like math and a few other things...
Apr 14 |
awarded | Good Answer |
Apr 13 |
awarded | Nice Answer |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
@GeraldEdgar: no, he did not believe that LLPO was true. |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
Since @PeterLeFanuLumsdaine mentioned the Cauchy/Dedekind issue, note that my answer specifically pertains to Cauchy reals as defined in the Bishop school of constructivism, for example. For (at least some common flavors of) Dedekind reals, dichotomy is constructively provable because $0$ can only lie in one of the two cuts of $\alpha$. In that case, the Bisection algorithm, for example, can be used to find a rapidly Cauchy sequence converging to a solution to the IVT but then it's not clear how to get a Dedekind real out of that. |
Apr 13 |
revised |
Does the Brouwer fixed point theorem admit a constructive proof?
added 2 characters in body |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
@AsafKaragila: I knew you were kidding, but it's still an interesting factoid about the argument. |
Apr 13 |
revised |
Does the Brouwer fixed point theorem admit a constructive proof?
A more convincing view of the Bouwerian counterexample |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
@coudy: We do have an algorithm to compute the $f$ I give and you can get a counterexample to BFPT using the usual trick that a fixed point of $f(x) + x$ is a root of $f(x)$. So it's easy to rescale and translate $f$ to show that BFPT is not constructive for the unit interval. |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
@AsafKaragila: No, the argument is constructive: its a proof of a negation, not a proof by contradiction! I show that it is impossible to have a constructive proof of IVT, which is the constructive way of proving a negative statement. |
Apr 13 |
comment |
Does the Brouwer fixed point theorem admit a constructive proof?
@Guntram: That's right: what I show is that IVT is actually equivalent to LLPO (assuming you believe LLPO can be repeated indefinitely in order to carry out the usual bisection argument). So if you believe LLPO is constructive or you have other ways to get around this issue, then everything is fine! |
Apr 13 |
answered | Does the Brouwer fixed point theorem admit a constructive proof? |
Apr 12 |
awarded | Nice Answer |
Apr 10 |
awarded | Nice Answer |
Apr 9 |
comment |
How do I apply the Boolean Prime Ideal Theorem?
@DavidSpeyer: If $P(x)$ is thought as a first-order predicate rather than a bunch of propositional variables things trivialize since the theory I wrote down becomes finite. (Moreover, first-order logic doesn't allow us to control the objects of our structure: a model of the theory of rings and the first-order versions of the axioms I wrote is some ring with a prime ideal rather than a prime ideal on the given ring $R$.) Using propositions as in my answer, your "$\exists_b P_{ab-1}$" is really a disjunction $\bigvee_{b \in R} P_{ab-1}$, which doesn't work unless $R$ is finite. |
Apr 9 |
comment |
How do I apply the Boolean Prime Ideal Theorem?
@QiaochuYuan: The key issue with maximality is that it can't be formulated using a bunch of finitary requirements. Formulas in the first-order language of rings are finitary requirements but this is not always the best way to formulate them. |
Apr 9 |
comment |
How do I apply the Boolean Prime Ideal Theorem?
@Goldstern: Yes, it's always fun when that happens! |
Apr 9 |
answered | How do I apply the Boolean Prime Ideal Theorem? |
Apr 3 |
comment |
Applications of set theory in physics
Replacement has tons of applications! From "having enough this-and-that" to the Reflection Principle which allows one to blindly work with proper classes in ZFC without resorting to Grothendieck universes and similar tools. The fact that replacement is invisible doesn't mean it's not used. This is a natural side effect that, while mathematicians conventionally work within the framework of set theory, most never work with bare axioms. In fact, that's the way set theory is intended to be used... |
Apr 3 |
revised |
Applications of set theory in physics
removed code block |
Apr 3 |
revised |
Necessary and sufficient condition for $can : A^X\otimes_A A^Y\rightarrow A^{X\times Y}$ to be an embedding
edited title |