30,138 reputation
380170
bio website dorais.org
location Hanover, NH
age
visits member for 5 years, 6 months
seen 2 hours ago

I like math and a few other things...


May
22
comment Induction and nonstandard halting times of standard machines
@JoelDavidHamkins: You're right that $SH(\mathcal N)$ depends on how one clocks Turing machines. If $0 \notin SH(\mathcal N)$ then $SH(\mathcal N)$ isn't a semiring nor does it contain all parameter-free $\Sigma_1$-definable elements of $\mathcal N$ and the answer breaks down.
May
22
revised Induction and nonstandard halting times of standard machines
clarification
May
22
answered Induction and nonstandard halting times of standard machines
May
22
comment Induction and nonstandard halting times of standard machines
Is there any reason to believe $SH(\mathcal N)$ is different from the parameter-free $\Sigma_1$-definable elements on $\mathcal N$?
May
19
comment A basic minimization problem over finite fields
This amounts to finding a short vector in the lattice in $\mathbb Z^n$ generated by the $n+1$ vectors $(a_1,\ldots,a_n),(p,0,\ldots,0),(0,p,\ldots,0),\ldots,(0,0,\ldots,p)$. The LLL algorithm might help.
May
1
comment A question about finitely additive extensions of Lebesgue measure
@Mirko: No such $X$ can be Lebesgue measurable because of Lebesgue Density Theorem: en.wikipedia.org/wiki/Lebesgue%27s_density_theorem
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.