Timeline for Constructive proof of a rational version of Perron-Frobenius?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 31, 2018 at 17:53 | vote | accept | darij grinberg | ||
| May 11, 2018 at 7:43 | answer | added | darij grinberg | timeline score: 5 | |
| May 11, 2018 at 7:17 | history | edited | darij grinberg | CC BY-SA 4.0 |
improve Theorem 1
|
| May 3, 2018 at 16:39 | answer | added | Franka Waaldijk | timeline score: 7 | |
| May 3, 2018 at 14:37 | comment | added | darij grinberg | By the way, now that I've asked the proverbial rubber duck, I have gotten a new idea: use one of the LP duality style theorems (Gordan, Stiemke, Motzkin). But it's grading week again, so I have no time to check... | |
| May 3, 2018 at 14:31 | comment | added | Simon Henry | Unfortunately no | |
| May 3, 2018 at 14:26 | comment | added | darij grinberg | @SimonHenry: What I mean is: does it yield an algorithm that translates classical proofs into constructive proofs? Maybe the algorithm cannot be constructively proven to terminate, but at least we could apply it to any given proof and wait until it terminates. | |
| May 3, 2018 at 13:52 | comment | added | Simon Henry | I'm not sure I understand your question: Barr's theorem (ncatlab.org/nlab/show/Barr%27s+theorem) tell us there is a constructive proof. But it does not tell us what the proof is. | |
| May 3, 2018 at 13:49 | comment | added | user44143 | Tarski's proof that the decision procedure works is also constructive. | |
| May 3, 2018 at 13:48 | comment | added | darij grinberg | @SimonHenry: Thanks. Is there an internal-logic version of this argument which lets me virtualize the classical proof in some topos? | |
| May 3, 2018 at 13:48 | comment | added | darij grinberg | @MattF: I don't know if this actually answers my question. I want a constructive proof, not just an algorithm which yields a valid answer by a classical proof (but I don't even see how that algorithm would work). | |
| May 3, 2018 at 13:45 | comment | added | Simon Henry | Quick remark which does not answer your question but is I think worth mentioning: both statement have "geometric" assumption and geometric conclusion. Hence the Barr covering theorem proves non-constructively that they have constructive proof. Which for the record is also how I know that the version of brouwer fix point theorem that you linked is constructive. | |
| May 3, 2018 at 13:42 | comment | added | user44143 | The decision procedure for the first-order theory of algebraic reals makes their constructive development trivial. Represent an algebraic real by a polynomial and an appropriate interval bound. Then you can easily test if it is 0. If it is non-zero, you can easily represent its additive and multiplicative inverses. Similarly you can take two such reals and get a representation for their sum or product, either by explicit formulas, or by searching through all representations and testing them with the decision procedure. | |
| May 3, 2018 at 13:20 | history | asked | darij grinberg | CC BY-SA 4.0 |