Timeline for How to construct a constructive proof from a non-constructive proof using prime ideals?
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| Apr 13, 2017 at 12:19 | history | edited | CommunityBot |
replaced http://math.stackexchange.com/ with https://math.stackexchange.com/
|
|
| Oct 30, 2016 at 21:07 | vote | accept | HeinrichD | ||
| Oct 13, 2016 at 6:48 | comment | added | HeinrichD | @IngoBlechschmidt: mathoverflow.net/questions/252009 :-) | |
| Oct 13, 2016 at 6:29 | comment | added | Ingo Blechschmidt | @HeinrichD: Just saw (part of) your deleted question on characterization of Zariski toposes in my mail feed. If you drop me a mail ([email protected]), I can try to give a (very partial) answer. Also I'd be interested in the full text of your question! | |
| Sep 29, 2016 at 22:19 | answer | added | HeinrichD | timeline score: 3 | |
| Sep 16, 2016 at 8:00 | comment | added | HeinrichD | @Ingo: The slides were very helpful. Thank you. | |
| Sep 15, 2016 at 9:31 | comment | added | Ingo Blechschmidt | A direct reference is cse.chalmers.se/~coquand/sitesur.pdf. Also the slides located at cse.chalmers.se/~coquand/FISCHBACHAU are very good. | |
| Sep 14, 2016 at 21:09 | comment | added | darij grinberg | I'll mark this thread for the future, but I won't have the time to expand this into an answer today. | |
| Sep 14, 2016 at 21:07 | comment | added | HeinrichD | @Darij Thank you for your comments. I would love to see these turned into an answer, perhaps including the application to the specific example I gave. I couldn't find this in the book by Lombardi and Quitte so far. | |
| Sep 14, 2016 at 21:06 | comment | added | darij grinberg | ... "Noetherian ring / Artinian ring / compactness" kinds of arguments. Sorry if I misrepresented anything! | |
| Sep 14, 2016 at 21:05 | comment | added | darij grinberg | ... every time the resulting extension ring reveals itself to have zero divisors, getting rid of them by quotienting it by an ideal". As I said, this is not a fully automatic rewriting of a proof (unless the proof is rather limited in its tooling), and some interpretation is required. It also seems to fail whenever some sort of Noetherian or Artinian properties are involved; this is why we constructivists tend to think that the real non-constructive arguments in mathematics are not the "maximal ideal / prime ideal / limit / algebraic closure" kinds of arguments, but the ... | |
| Sep 14, 2016 at 21:02 | comment | added | darij grinberg | ... grow to encompass either $f$ or $g$". The "dynamic counterpart" of "algebraic closure" would be "a field that, every time we have a polynomial over it, can grow by adjoining the roots of this polynomial". The latter example is actually a bit of an oversimplification, since "adjoining the roots" in itself isn't always constructive (it relies on the factorization of the polynomial into irreducibles, which cannot always be computed), so it too gets replaced by the dynamic concept of "adjoining the roots as if the polynomial had a symmetric Galois group and then, ... | |
| Sep 14, 2016 at 21:00 | comment | added | darij grinberg | The book arxiv.org/abs/1605.04832 by Lombardi and Quitte has its whole Chapter VII devoted to a (not fully formalized, but often rather straightforward-to-follow) method for obtaining a constructive proof from a non-constructive one. Roughly speaking, the idea is to replace the "too-perfect-to-be-true" notions like "prime ideal" or "maximal ideal" or "algebraic closure" by their "dynamic" counterparts. For instance, the "dynamic counterpart" of "maximal ideal" is something like "a prime ideal $I$ that, each time we find two elements $f$ and $g$ satisfying $fg \in I$, can ... | |
| Sep 14, 2016 at 19:43 | answer | added | Simon Henry | timeline score: 8 | |
| Sep 14, 2016 at 17:53 | comment | added | HeinrichD | @MattF. This is a very good point. Thank you. | |
| Sep 14, 2016 at 17:52 | history | edited | HeinrichD | CC BY-SA 3.0 |
added 452 characters in body; edited title
|
| Sep 14, 2016 at 17:48 | comment | added | user44143 | The word "otherwise" in proof b gives me pause. Even if "for all n (x+y)^n !=0" leads to a contradiction, that does not construct n such that(x+y)^n=0. So proof b may need more to work constructively. | |
| Sep 14, 2016 at 16:47 | answer | added | Henry Towsner | timeline score: 8 | |
| Sep 14, 2016 at 14:51 | comment | added | Emil Jeřábek | The keyword to search is “proof mining”, but I have no idea whether something relevant to prime ideals has been done. | |
| Sep 14, 2016 at 14:14 | comment | added | HeinrichD | It is not equivalent to AC; it is weaker. But I only use this for countable $A$ anyway, where can even give a proof in ZF ("just add elements until you are done"). References are included in the text. | |
| Sep 14, 2016 at 13:57 | comment | added | user40276 | I don't completely understand your question. But given a multiplicative set $S \subset A$, the existence of a prime ideal $\mathfrak{p}$ such that $\mathfrak{p} \subset A \setminus S$ is equivalent to AC, so for instance "the intersection of all prime ideals is the set of nilpotent elements" cannot be made into a proof without AC. | |
| Sep 14, 2016 at 13:27 | history | asked | HeinrichD | CC BY-SA 3.0 |