Applications of nonconstructive mathematics - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-26T02:15:09Z http://mathoverflow.net/feeds/question/96914 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics Applications of nonconstructive mathematics Ruud Koot 2012-05-14T15:49:53Z 2012-05-20T21:21:38Z <p>What are good/interesting examples of theorems than can be proven classically, but not constructively, and have applications in e.g. physics?</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96917#96917 Answer by Felix Goldberg for Applications of nonconstructive mathematics Felix Goldberg 2012-05-14T16:04:34Z 2012-05-14T16:04:34Z <p>Well, the Brouwer Fixed Point Theorem comes to mind. An example of an application: <a href="http://physicsoffinance.blogspot.com/2011/09/brouwers-fixed-point-theoremwhy.html" rel="nofollow">http://physicsoffinance.blogspot.com/2011/09/brouwers-fixed-point-theoremwhy.html</a></p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96918#96918 Answer by Henry Towsner for Applications of nonconstructive mathematics Henry Towsner 2012-05-14T16:07:26Z 2012-05-14T16:07:26Z <p>The mean and pointwise ergodic theorems are non-constructive, and I understand they were originally developed for applications to thermodynamics.</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96921#96921 Answer by Igor Rivin for Applications of nonconstructive mathematics Igor Rivin 2012-05-14T16:20:37Z 2012-05-14T16:20:37Z <p>I would assume that the Hahn-Banach theorem would have to be close to the top of any list.</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96928#96928 Answer by none for Applications of nonconstructive mathematics none 2012-05-14T17:24:06Z 2012-05-14T17:24:06Z <p>The Knuth-Bendix completion algorithm is used in computer algebra. Its proof of correctness relies on Kruskal's tree theorem, if I understand correctly. The proof of Kruskal's tree theorem is very nonconstructive: <a href="http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem" rel="nofollow">http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem</a></p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96934#96934 Answer by Jason Rute for Applications of nonconstructive mathematics Jason Rute 2012-05-14T18:39:43Z 2012-05-14T18:39:43Z <p>One of the simplest is the monotone convergence principle, that every bounded increasing sequence of rationals is convergent.</p> <p>Along with Henry Towsner's example of the Ergodic theorem there is Doob's martingale convergence theorem and Lebesgue's theorem that every function of bounded variation is differentiable a.e.</p> <p>However, if more information is known then this non-constructivity can be overcome. For example, with a martingale, if the limit is computable in the $L^1$ norm and the $L^1$-bound is computable, then the rate of convergence is computable (both convergence in measure and a.e. convergence). (I assume the proof is constructive, but I haven't worked that out. However, computable rates of convergence are one of the most important consequences of constructive proofs.)</p> <p>Similarly, the Lebesgue differentiation theorem has computable rates of convergence ($L^1$ convergence and a.e. convergence) since the limit is known (it is the function itself) and the Hardy-Littlewood maximal lemma controls the maximal amount of deviation from the limit.</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/96947#96947 Answer by Andrej Bauer for Applications of nonconstructive mathematics Andrej Bauer 2012-05-14T20:55:01Z 2012-05-14T21:03:52Z <p>In general it is very difficult to be sure that a theorem cannot be constructivised in some form that preserves its applicability. As you will notice most of the answers offered have comments attesting this fact.</p> <p>One reason for this is that many non-constructive theorems in analysis become constructive when they are relaxed a little bit. A typical example is the mean value theorem. It does not hold constructively as usually stated, but it its $\epsilon$ version does: if $f$ is continuous and $f(0) &lt; 0 &lt; f(1)$ then for every $\epsilon > 0$ there is $x \in [0,1]$ such that $|f(x)| &lt; \epsilon$. Many other theorems can be relaxed in this way: Hahn-Banach, Brouwer fixed-point, etc. Moreover, such relaxed versions often make <em>more sense</em> in applications than their exact versions, for example because we need to take into account noise, errors, or bounded numerical precision.</p> <p>Another reason is that for applications we typically do not need a theorem in its full generality because we have extra information, which allows for a specialized constructive version. For example, while the general mean value theorem fails constructively, it holds for locally non-constant maps. Special versions of Hahn-Banach holds constructively, and they will typically suffice in concrete situations.</p> <p>There is a third reason why it is difficult to find classical theorems with applications that cannot be constructivized. Most applications belong to the fields of physics and computer science, which are both very naturally constructive. Physics is constructive by its very nature because "everything is continuous" in the real world, while in computer science "everything is computable". These are two main motivations for intuitionistic mathematics (namely Brouwerian continuity principles or sheaf-theoretic models, and computable interpretations of intuitionistic mathematics).</p> <p>Lastly, there remains the simple fact that one has to perform an exhaustive literature search to be sure that a theorem has not been constructivized. A lot more has been constructivized than one would think, and the only obstacle seems to be lack of man power.</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/97072#97072 Answer by Daniel Moskovich for Applications of nonconstructive mathematics Daniel Moskovich 2012-05-16T00:23:45Z 2012-05-16T00:29:04Z <p>Sard's Theorem, which is foundational, may be an example of a theorem of the sort you are looking for when the differentiability class of the function is low. Let's recall its classical statement:</p> <blockquote> <b>Sard's Theorem</b>: Let $f\colon\, \mathbb{R}^n\to\mathbb{R}^m$ be a $k$ times continuously differentiable function, where $k\geq \text{max}(n-m+1,1)$. Let $X$ be the critical set of $f$. Then $f(X)$ has Lebesgue measure $0$ in $\mathbb{R}^m$. </blockquote> <p>A constructivist version was proven by Yuen-Kwok Chan in 1971:</p> <blockquote> Chan, Yuen-kwok, <i>A constructive proof of Sard's theorem.</i> Pacific J. Math. <b>36</b>, 291–301 (1971; MR0276988). </blockquote> <p>The constructivist version relaxes the statement of Sard's theorem in a benign way ("critical points" are replaced by "almost critical points") and in at least one less benign way:</p> <blockquote> The function $f$ is taken to be a $k$ times continuously differentiable function, where $k\geq 2+\frac{1}{2}(n-m)(n-m+1)$. </blockquote> <p>I can imagine this being a real issue, because the function actually given to you might be $C^k$ only for $\text{max}(n-m+1,1)\leq k&lt; 2+\frac{1}{2}(n-m)(n-m+1)$. John Milnor on <a href="http://www.ams.org.ezlibproxy1.ntu.edu.sg/mathscinet/search/publdoc.html?arg3=&amp;co4=AND&amp;co5=AND&amp;co6=AND&amp;co7=AND&amp;dr=all&amp;pg4=AUCN&amp;pg5=TI&amp;pg6=PC&amp;pg7=ALLF&amp;pg8=ET&amp;r=1&amp;review_format=html&amp;s4=Chan&amp;s5=sard%27s&amp;s6=&amp;s7=&amp;s8=All&amp;vfpref=html&amp;yearRangeFirst=&amp;yearRangeSecond=&amp;yrop=eq" rel="nofollow">Mathematical Reviews</a> asks whether the bound on $k$ can be tightened, and so does the author at the end of the paper. If not, then Sard's Theorem for small $k$ seems to me to be a genuinely important result which can be proved classically, but not constructively.</p> http://mathoverflow.net/questions/96914/applications-of-nonconstructive-mathematics/97507#97507 Answer by none for Applications of nonconstructive mathematics none 2012-05-20T21:21:38Z 2012-05-20T21:21:38Z <p>A famous Martin Gardner mathematical games column had a number of April Fool items, one of which was about a guy getting rich by duplicating gold spheres using the Banach-Tarski theorem. I guess that doesn't count as a real application, but it's surely nonconstructive and I can't resist mentioning it.</p>