tag:blogger.com,1999:blog-3722233.post1404266269380906120..comments2024-09-10T16:39:34.186-05:00Comments on Computational Complexity: What Makes a Constructive Proof?Lance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger15125tag:blogger.com,1999:blog-3722233.post-86384222385291618892024-03-01T15:05:21.427-06:002024-03-01T15:05:21.427-06:00I finally tracked down the result I was thinking o...I finally tracked down the result I was thinking of: Theorem 1 of "Why are Proof Complexity Lower Bounds Hard?" by Ján Pich and Rahul Santhanam, FOCS 2019.Timothy Chowhttp://alum.mit.edu/www/tchownoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-21109959343294839352023-11-15T09:38:54.066-06:002023-11-15T09:38:54.066-06:00You shouldn't use the excluded middle (P or no...You shouldn't use the excluded middle (P or not P) but it's really about constructive methods, like proving P implies Q but showing how to convert a proof of P into a proof of Q.Lance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-47217255803982324832023-11-15T01:12:21.560-06:002023-11-15T01:12:21.560-06:00Are we talking about proving results in a logical ...Are we talking about proving results in a logical system in which "P or not P" is neither an axiom nor a theorem of that system? How far would you be able to get in such a system? Or are we just talking about avoiding the use of "P or not P" in certain crucial points in the proof? Gabriel Nivaschnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-5604827659796449862023-09-17T05:42:30.663-05:002023-09-17T05:42:30.663-05:00It seems that Daniels's proof can be presented...It seems that Daniels's proof can be presented in a constructive way. He defined languages L_k for any k and the description of the \Sigma^p_2 machines that decide L_k are computable in polynomial time in k. So we can write the statement B:="for every k, L_k is not in size(n^k)" as a \Pi_2 sentence in the language of arithmetic as follows:<br /><br />B:=For every k and every c, there is a natural number n such that any circuit of size at most cn^k+c with input length n does not decide L_k correctly on inputs of length n. <br /><br />As the property "any circuit of size at most cn^k+c with input length n does not decide L_k correctly on inputs of length n" is a primitive recursive property (it is actually a bounded formula in the language of Buss's bounded arithmetic) B is a \Pi_2 sentence. Daniels's proof can be formalized in Peano arithmetic and as it is known that Peano arithmetic is \Pi_2 conservative over Heyting arithmetic we get that Heyting arithmetic can prove B which implies the existence of a constructive proof of Daniels's result. Here is the wiki link about \Pi_2 conservativity of Peano arithmetic over Heyting arithmetic:<br />https://en.wikipedia.org/wiki/Friedman_translationErfan Khanikinoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-10382548605275452492023-09-12T20:39:11.629-05:002023-09-12T20:39:11.629-05:00To some fuel to the fire, constructivist don't...To some fuel to the fire, constructivist don't agree on what it exactly means. See "Varieties of Constructive Mathematics".<br /><br />And you can always state classical theorems in a construction way using Godel's translation.<br /><br /> not (not A and not B)<br /><br />which indicates that essentially they are interpreting or as having a new meaning.<br /><br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-74777824156933777942023-09-12T10:45:07.328-05:002023-09-12T10:45:07.328-05:00This post reminds me of that great non-constructiv...This post reminds me of that great non-constructive joke.Mahdihttps://www.blogger.com/profile/12382401759237060260noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-75969021523806919442023-09-10T23:38:01.357-05:002023-09-10T23:38:01.357-05:00Haven't there been some more recent (last 5 ye...Haven't there been some more recent (last 5 years maybe?) circuit lower-bound results whose proofs are non-constructive in the sense of explicitly using the law of the excluded middle? I feel like I've seen at least one such paper, but unfortunately, I can't recall any more details.Timothy Chowhttp://alum.mit.edu/www/tchownoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-1292276683785670932023-09-06T06:31:55.486-05:002023-09-06T06:31:55.486-05:00I think the L in the non-constructive theorem by K...I think the L in the non-constructive theorem by Kannan refers to a language in sigma_4. As stated it can easily be misunderstood as the class L. The definition of L was given in the post "Sixteen Years in the Making " (August'14) but did not survive the copy+paste.<br /><br />In general, keep up the great work. This blog is awesome!Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-33574703516900103392023-09-01T04:05:36.772-05:002023-09-01T04:05:36.772-05:00In number theory, there are some examples of theor...In number theory, there are some examples of theorems proven by cases, giving a proof if the Riemann Hypothesis holds, and another if the Riemann Hypothesis fails. Some are mentioned in wikipedia like Nicolas' theorem. I've always wondered what constructive mathematicians thought of those.Lievenhttps://www.blogger.com/profile/01537820436390730307noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-66155925879259552402023-08-31T13:41:55.319-05:002023-08-31T13:41:55.319-05:00(sqrt(2)^sqrt(2)) ^ sqrt(2) = sqrt(2)^(sqrt(2) * s...(sqrt(2)^sqrt(2)) ^ sqrt(2) = sqrt(2)^(sqrt(2) * sqrt(2)) = sqrt(2)^2 = 2<br /><br />Repeated exponentiation means the exponents get multiplied.Robertnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-88339829398002509152023-08-31T09:32:58.447-05:002023-08-31T09:32:58.447-05:00Why is (sqrt(2)^sqrt(2))^sqrt(2) rational???Why is (sqrt(2)^sqrt(2))^sqrt(2) rational???Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-51982067425684174302023-08-31T08:29:34.527-05:002023-08-31T08:29:34.527-05:00No, the first proof is not constructive as it depe...No, the first proof is not constructive as it depends on assuming sqrt(2)^sqrt(2) is either rational or irrationalLance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-77060732714644834292023-08-31T08:28:30.624-05:002023-08-31T08:28:30.624-05:00I can't find the typo. Can you be more "c...I can't find the typo. Can you be more "constructive"?Lance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-46972131379041335042023-08-31T06:46:16.768-05:002023-08-31T06:46:16.768-05:00Are you saying that the first proof, the one with ...Are you saying that the first proof, the one with all of the sqrt(2)s in it, is constructive as a proof by cases?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-42880255541459672282023-08-30T17:11:19.958-05:002023-08-30T17:11:19.958-05:00Your root 2 example has at least one typo.Your root 2 example has at least one typo.Anonymousnoreply@blogger.com