84:
74:
53:
204:
diagonalization to construct a decimal expansion of a real number where each digit is different from the respective digit of the respective algebraic number in the enumerating sequence. This procedure produces a transitive number and it is well-defined: it can produce any digit of the decimal expansion upon request. That allows us to compare the number to any rational number and to create a
Dedekind section out of it. What is nonconstructive here?
341:
to a particular logic. I.e. in a consistent logic you cannot derive a contradiction (e.g. 0 = 1). Should it instead say that adding a classical principe (say excluded middle) is a 'conservative extension' of intuitionistic logic? Meaning that by adding excluded middle we would only get a system in which all classical theorems hold but nothing more, i.e. we don't end up with something inconsistent. Please correct me if I am wrong.
22:
903:"Some non-constructive proofs show that if a certain proposition is false, a contradiction ensues; consequently the proposition must be true (proof by contradiction). However, the principle of explosion (ex falso quodlibet) has been accepted in some varieties of constructive mathematics, including intuitionism."
491:(Of cource, I don't expect a Goldbach proof to be found this simplistic way; this is just a thought experiment.) I wonder what Brouwer and/or Troelstra originally said about this, but I can't get access to Troelstra's book and don't even have a reference for Brouwer (the article should provide one). The
516:
I'm sure
Brouwer had this template in mind. Although he predates Church's thesis and the terms "co-c.e." or "Pi_1", he knew (and the article misses this point) that there is an effective procedure which terminates if and only if Goldbach's conjecture is false. (I seem to remember also "999999999 does
203:
The statement that the set of algebraic numbers is countable is equivalent to the statement that there exists an algorithm that enumerates them all with increasing precision, i.e. it outputs the decimal approximation of each consecutive number with precision growing by 1 in each turn. We can now use
725:
Is it? I think usually this sort of example is given by something like f(n)=0 if 2n is the sum of two primes or n is 0 or 1 and f(n)=1 otherwise. This second definition by cases uses a decidable criterion and so demonstrably yields a computable function. If definitions by cases are generally allowed
340:
I don't understand the sentence "Since intuitionistic logic is consistent with classical logic, it is impossible to disprove non-constructive statements that are classically valid." What does it mean for for some logic to be 'consistent with' another? I have only heard consistency used with respect
729:
I suppose we could, in a constructive theory, postulate the existence of a function such that f(x)=0 for all x if
Golbach's conjecture is false and f(x)=1 for all x if it is true and reason about such a function's properties, but it's not even obvious to me that most constructive theories would be
212:
We may distinguish three different problems. The first is that of proving the existence of transcendental numbers (without necessarily providing a specimen). The second is that of giving an example of a transcendental number by a construction specially designed for the purpose. The third, which is
219:
So "algebraics are countable, reals are uncountable, therefore transcendentals exist" is a (non-constructive) solution to the first, your proof is a solution to the second (we could include it in the article as such), and a proof that pi is transcendental is a solution to the third. On the other
717:
249:
To be sure, you could sabotage Cantor's proof of the uncountability of the reals to produce a weaker result: the mere fact that the set of real numbers cannot be countable. In that case, the proof that there exists a transcendental number is not constructive; it only proves that there
257:
This sort of example is commonly used by nonconstructive mathematicians that (in my opinion) don't really understand costructivism (and so can't appreciate the finer points of the nonconstructivity of proofs). Constructive mathematicians themselves often use the example in
362:
However, there are problems with the wording of that section. Some constructive systems do assume principles that are false in classical mathematics. For example, these systems may assume that every function from Ď to Ď is computable, or assume every function from
726:
to take the form the article suggests, however, that would seem to imply the existence of noncomputable functions (at least if there are no restrictions on what sorts of cases we can use), which at least some constructive theories outright deny.
288:
The article should be rewritten completely because the approach used in this article is academic. The concept of non-constructive proof is different from constructive proof and it (non constructive proof) should have a separate article.
356:
We say that a theory S extending a theory T is a conservative extension of T if everything that is in the language of T and provable in S is already provable in T. So classical logic is not a conservative extension of intuitionistic
262:, a proof that the irrational numbers aren't closed under exponentiation. But that example is less satisfying (especially since even the example in the nonconstructive proof can easily be decided: (â2) is irrational by the
770:
I'm glad to have helped. I also edited your definition to include the condition that the counterexample is even in the second case, which I believe is necessary unless I'm having a really bad day for thinking clearly.
246:; this is what Cantor's diagonal argument naturally shows. In that case, once you've proved the countability of the algebraic numbers (which has no surprises), then it's obvious that a transcendental number exists.
162:
Alan Kay and other computer scientists use the term "Existence Proof" to mean proof by example, e.g. demonstrating a red car is proof that some cars are red. I think this article should add this second connotation.
647:
230:
The anon has a good point here. While you might argue that the countability proof is nonconstructive as it stands, if it can trivially be made constructive, then there is not much to its nonconstructivity.
467:". On second thought, I don't understand either version of the sentence: A mathematical proof cannot yield a result about the current state of knowledge of the human scientific community, can it?
140:
430:
495:
seems to suggest that
Brouwer considered mathematical truth to be changing in time (and from person to person), according to current knowledge, but doesn't elaborate on that. -
186:
A good section on Boyer-Moore theory and the Boyer-Moore theorem prover would help here. There's a whole area of sucessful constructive mathematics that needs to be covered.
906:
These two statements are not related to each other. This appears to be an act of vandalism or a mistaken edit, removing some important context relating the two sentences.
845:
841:
827:
436:, but this fact is irrelevant to the correctness of the non-constructive proof". Does anyone know whether the theorem is valid in a constructive framework?
189:
One big problem with constructive proofs is that they tend to require case analysis and become bulky. With machine assistance, this is less of a problem.
524:, and substitute the halting problem for Goldbach's conjecture, then you've actually disproved the law of the excluded middle. Church's Thesis is a (Pi_2)
521:
934:
130:
745:
That example was indeed unclear - thank you for pointing it out. Although something was defined, it would not be possible to prove constructively that
929:
520:
As for mathematical truth changing in time and all that, Brouwer and others take that view. But it is not necessary for constructivism. If you assume
238:(like that by Errett Bishop) will prove (constructively) that the set of real numbers is uncountable in a strong sense: that given any countable set
254:
be a transcendental number. But to a constructivist, this interpretation is perverse; the word "uncountable" naturally takes the stronger meaning.
572:
The statement holds as written. However, I fail to see why this proof is inconstructive, given that you can take the smallest factor as before.
749:
was even a function. I changed the example to a more classical one involving the limit of a Cauchy sequence, with a reference to the SEP. â Carl
712:{\displaystyle f(x)={\begin{cases}0&{\mbox{if Goldbach's conjecture is false}}\\1&{\mbox{if Goldbach's conjecture is true}}\end{cases}}}
557:
I think the part 'all of its prime factors are greater than n' should instead be 'some of its prime factors are greater than n'. Am I mistaken?
106:
772:
731:
342:
813:
538:
371:
is continuous. Not every constructive system assumes such things; some constructive systems are consistent with classical mathematics.
823:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
97:
58:
461:
Such counterexamples do not disprove a statement, however; they only show that, at present, the statement has no constructive proof
602:, these subpages are now deprecated. The comments may be irrelevant or outdated; if so, please feel free to remove this section.
208:
Well, sure, but that's a diagonal argument, and it is not the same as the proof based on uncountability. As the article says:
318:
I disagree, unless if there is an evidence that a non-constructive proof is not the same as a proof thatis not constructive.
433:
263:
888:
33:
608:
Why doesn't someone write a history of constructive proofs to show how the field has grown and evolved? Robert
Hoffman
500:
844:
to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
528:
of arithmetic, and even of set theory (while the law of the excluded middle is conservative over arithmetic but
776:
735:
513:
Of course such things are templates, if one problem is solved one simply substitutes the next unsolved problem.
294:
613:
21:
346:
251:
879:
805:
730:
able to prove that two such functions are equal (without either proving or disproving
Goldbach's conjecture)
542:
402:
376:
In any case, I reworded the section to avoid this issue and avoid the "consistent with" terminology. â Carl
235:
177:
all cover the same ground. It would be better to merge all three, I think, and get one substantive article.
722:
Although this is a definition by cases, it is still an admissible definition in constructive mathematics."
525:
309:
274:
609:
863:
If you have discovered URLs which were erroneously considered dead by the bot, you can report them with
851:
496:
259:
221:
180:
174:
39:
804:. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit
83:
911:
907:
305:
192:
814:
https://web.archive.org/web/20141023060917/http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf
671:
290:
213:
much more difficult, is that of proving that some number given independently ... is transcendental.
558:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
797:
456:
323:
89:
848:
before doing mass systematic removals. This message is updated dynamically through the template
73:
52:
864:
510:
Yeah, this article could be clearer. I may fix it myself, but don't hold your breath. Briefly:
492:
562:
270:
170:
817:
577:
470:
In the
Goldbach example, it could be possible that the thinking along the lines of defining
441:
871:
830:, "External links modified" talk page sections are no longer generated or monitored by
870:
If you found an error with any archives or the URLs themselves, you can fix them with
474:
etc. just leads to the proof (or disproof) of
Goldbach's conjecture. So the sentence "
923:
756:
625:
Last edited at 19:11, 7 September 2009 (UTC). Substituted at 01:55, 5 May 2016 (UTC)
599:
383:
319:
242:
of real numbers, there exists a real number which is distinct from every element of
488:
could well be found and, in turn, would lead to a proof of
Goldbach's conjecture.
164:
837:
573:
437:
102:
836:. No special action is required regarding these talk page notices, other than
79:
484:" is wrong imho; instead, a constructive proof of the quoted statement about
915:
893:
780:
761:
739:
617:
581:
566:
546:
504:
445:
388:
350:
327:
313:
298:
278:
224:
752:
379:
465:... at present, no constructive proof of the statement is known
15:
705:
808:
for additional information. I made the following changes:
818:
http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf
199:
Why is the proof based on uncountability nonconstructive?
801:
594:
517:
not appear in the decimal expansion of pi", also Pi_1.)
696:
680:
650:
553:
Mistake in section Examples/Non-constructive proofs ?
405:
220:
hand, perhaps we should just find a better example.
101:, a collaborative effort to improve the coverage of
840:using the archive tool instructions below. Editors
711:
424:
633:Right now, the article says: "Define a function
598:, and are posted here for posterity. Following
826:This message was posted before February 2018.
592:The comment(s) below were originally left at
482:must also not have a known constructive proof
457:Constructive proof#Brouwerian counterexamples
8:
19:
796:I have just modified one external link on
522:Church's thesis (constructive mathematics)
47:
695:
679:
666:
649:
414:
407:
404:
399:The page states that "It turns out that
425:{\displaystyle {\sqrt {2}}^{\sqrt {2}}}
49:
7:
95:This article is within the scope of
236:constructive treatments of analysis
38:It is of interest to the following
14:
935:Mid-priority mathematics articles
800:. Please take a moment to review
682:if Goldbach's conjecture is false
600:several discussions in past years
115:Knowledge:WikiProject Mathematics
930:Start-Class mathematics articles
698:if Goldbach's conjecture is true
595:Talk:Constructive proof/Comments
118:Template:WikiProject Mathematics
82:
72:
51:
20:
451:Brouwerian weak counterexamples
135:This article has been rated as
660:
654:
479:is known, the quoted statement
1:
618:19:11, 7 September 2009 (UTC)
446:15:06, 27 February 2012 (UTC)
432:is irrational because of the
299:19:20, 22 December 2009 (UTC)
279:02:13, 19 November 2007 (UTC)
109:and see a list of open tasks.
916:01:31, 11 January 2022 (UTC)
547:16:11, 9 February 2015 (UTC)
505:11:50, 12 October 2013 (UTC)
894:13:51, 12 August 2017 (UTC)
781:18:17, 6 January 2017 (UTC)
762:21:15, 4 January 2017 (UTC)
740:19:52, 4 January 2017 (UTC)
951:
857:(last update: 5 June 2024)
793:Hello fellow Wikipedians,
582:21:48, 26 April 2015 (UTC)
567:20:54, 11 April 2015 (UTC)
493:SEP page externally linked
455:I just changed in section
169:It seems to me that this,
607:
434:GelfondâSchneider theorem
264:GelfondâSchneider theorem
225:15:12, 24 July 2006 (UTC)
195:13:37, 21 Feb 2006 (PST)
183:17:37, 10 Nov 2003 (UTC)
134:
67:
46:
395:Is Gelfond constructive?
389:19:58, 9 July 2010 (UTC)
351:18:05, 9 July 2010 (UTC)
141:project's priority scale
789:External links modified
328:19:38, 4 May 2024 (UTC)
314:18:21, 4 May 2024 (UTC)
284:Non Constructive Proofs
98:WikiProject Mathematics
713:
526:conservative extension
426:
28:This article is rated
714:
476:Because no such proof
427:
260:Nonconstructive proof
175:nonconstructive proof
838:regular verification
648:
637:of a natural number
403:
121:mathematics articles
899:Unrelated sentences
828:After February 2018
629:Definition by cases
304:I completely agree
882:InternetArchiveBot
833:InternetArchiveBot
798:Constructive proof
709:
704:
700:
684:
588:Assessment comment
422:
90:Mathematics portal
34:content assessment
858:
760:
699:
683:
623:
622:
532:over set theory).
419:
412:
387:
171:existence theorem
155:
154:
151:
150:
147:
146:
942:
892:
883:
856:
855:
834:
750:
718:
716:
715:
710:
708:
707:
701:
697:
685:
681:
605:
604:
597:
497:Jochen Burghardt
431:
429:
428:
423:
421:
420:
415:
413:
408:
377:
181:Charles Matthews
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
950:
949:
945:
944:
943:
941:
940:
939:
920:
919:
901:
886:
881:
849:
842:have permission
832:
806:this simple FaQ
791:
703:
702:
693:
687:
686:
677:
667:
646:
645:
631:
593:
590:
555:
453:
406:
401:
400:
397:
338:
336:Consistent with
286:
201:
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
948:
946:
938:
937:
932:
922:
921:
900:
897:
876:
875:
868:
821:
820:
812:Added archive
790:
787:
786:
785:
784:
783:
773:107.77.212.225
765:
764:
732:107.77.211.108
720:
719:
706:
694:
692:
689:
688:
678:
676:
673:
672:
670:
665:
662:
659:
656:
653:
630:
627:
621:
620:
610:Robert hoffman
589:
586:
585:
584:
554:
551:
550:
549:
535:
534:
533:
518:
514:
459:the sentence "
452:
449:
418:
411:
396:
393:
392:
391:
373:
372:
359:
358:
337:
334:
333:
332:
331:
330:
285:
282:
228:
227:
217:
216:
215:
200:
197:
159:
156:
153:
152:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
947:
936:
933:
931:
928:
927:
925:
918:
917:
913:
909:
904:
898:
896:
895:
890:
885:
884:
873:
869:
866:
862:
861:
860:
853:
847:
843:
839:
835:
829:
824:
819:
815:
811:
810:
809:
807:
803:
799:
794:
788:
782:
778:
774:
769:
768:
767:
766:
763:
758:
754:
748:
744:
743:
742:
741:
737:
733:
727:
723:
690:
674:
668:
663:
657:
651:
644:
643:
642:
640:
636:
628:
626:
619:
615:
611:
606:
603:
601:
596:
587:
583:
579:
575:
571:
570:
569:
568:
564:
560:
552:
548:
544:
540:
536:
531:
527:
523:
519:
515:
512:
511:
509:
508:
507:
506:
502:
498:
494:
489:
487:
483:
480:
477:
473:
468:
466:
462:
458:
450:
448:
447:
443:
439:
435:
416:
409:
394:
390:
385:
381:
375:
374:
370:
366:
361:
360:
355:
354:
353:
352:
348:
344:
343:88.196.63.146
335:
329:
325:
321:
317:
316:
315:
311:
307:
303:
302:
301:
300:
296:
292:
283:
281:
280:
276:
272:
267:
265:
261:
255:
253:
247:
245:
241:
237:
232:
226:
223:
222:192.75.48.150
218:
214:
210:
209:
207:
206:
205:
198:
196:
194:
190:
187:
184:
182:
178:
176:
172:
167:
166:
157:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
905:
902:
880:
877:
852:source check
831:
825:
822:
795:
792:
746:
728:
724:
721:
641:as follows:
638:
634:
632:
624:
591:
556:
539:74.216.224.3
529:
490:
485:
481:
478:
475:
471:
469:
464:
460:
454:
398:
368:
364:
339:
287:
271:Toby Bartels
268:
256:
248:
243:
239:
233:
229:
211:
202:
191:
188:
185:
179:
168:
161:
137:Mid-priority
136:
96:
62:Midâpriority
40:WikiProjects
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
924:Categories
908:Comiscuous
889:Report bug
306:Habiliscus
291:arsalan...
193:John Nagle
872:this tool
865:this tool
252:can't not
878:Cheers.â
463:" into "
320:D.Lazard
234:Indeed,
158:Untitled
802:my edit
559:Notrium
165:Mcandre
139:on the
574:Yecril
438:Tkuvho
357:logic.
36:scale.
912:talk
777:talk
757:talk
736:talk
614:talk
578:talk
563:talk
543:talk
501:talk
442:talk
384:talk
347:talk
324:talk
310:talk
295:talk
275:talk
173:and
846:RfC
816:to
753:CBM
530:not
380:CBM
367:to
266:).
131:Mid
926::
914:)
859:.
854:}}
850:{{
779:)
755:¡
738:)
616:)
580:)
565:)
545:)
537:--
503:)
444:)
382:¡
349:)
326:)
312:)
297:)
277:)
163:--
910:(
891:)
887:(
874:.
867:.
775:(
759:)
751:(
747:f
734:(
691:1
675:0
669:{
664:=
661:)
658:x
655:(
652:f
639:x
635:f
612:(
576:(
561:(
541:(
499:(
486:f
472:f
440:(
417:2
410:2
386:)
378:(
369:R
365:R
345:(
322:(
308:(
293:(
273:(
269:â
244:A
240:A
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
