29,949 reputation
380170
bio website dorais.org
location Hanover, NH
age
visits member for 5 years, 5 months
seen 7 hours ago

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