Timeline for Replacing logician-constructive with combinatorist-constructive?
Current License: CC BY-SA 2.5
7 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/
|
|
| Aug 25, 2010 at 5:34 | comment | added | Aaron Meyerowitz | Sometimes a constructive move simply involves more carefully stating what it is that a proof shows. In Hex there can be no draw and it is not the case that the second player has a winning strategy. Probably every digit appears equally often in Pi. Classically, at least one appears infinitely often (actually at least two). Constructively, they don't all appear finitely often. Sometime following that discipline actually guides on to stronger proofs (but that is a topic for another question). | |
| Jun 6, 2010 at 15:33 | comment | added | Neel Krishnaswami | Wow, that Goldwasser/Kilian algorithm is really amazing! It "almost always" quickly terminates, which is neat. Are there any fast "almost always" semi-algorithms? (Ie, you're allowed to not terminate at all on "not many" inputs.) Most semi-algorithms I know come from things like the completeness of first-order logic, so their worst case performance is unspeakable. Are there any algorithms which you know will finish quickly if they finish at all? (The reason I ask is that it would refute the idea that combinatorially constructive methods subset the intuitionistic methods.) | |
| Jun 5, 2010 at 23:01 | comment | added | Timothy Chow | Neel's point is that "ineffective proof" in the strong sense of providing no algorithm at all is nicely captured by intuitionistic logic. E.g., the finiteness theorem of Faltings gives no algorithm for finding the solutions, and an intuitionist expresses this by saying the solution set is "not infinite" (as opposed to "finite"). The question is, is there a similar way to capture formally the fact that (for example) the probabilistic existence proof of Ramsey graphs yields no polytime construction? The answer is yes: the proof is not formalizable in a certain system of bounded arithmetic. | |
| Jun 5, 2010 at 18:21 | comment | added | Gil Kalai | Interesting post, but I do not think the example, as an example of non effective or non explicit proof, is bogus. It is true that the term "non effective proof" is not always precise or formal. | |
| Jun 5, 2010 at 17:47 | comment | added | Andrej Bauer | The "irrational to irrational = rational" example is bogus, see math.andrej.com/2009/12/28/… | |
| Jun 5, 2010 at 13:02 | history | answered | Gil Kalai | CC BY-SA 2.5 |