Кіріспе
Математикадағы дәлелдеу әдісі
Математикада конструктивті дәлелдеу – математикалық объектінің бар екенін, осы объектіні құру немесе оны құру тәсілін ұсыну арқылы көрсететін дәлелдеу әдісі. Бұл, мысал келтірмей объектінің бар екенін дәлелдейтін конструктивті емес дәлелдеуге (сонымен қатар, барлыққа қатысты дәлел немесе таза барлыққа қатысты теорема деп те аталады) қарсы келеді. Келесіде келтірілген күшті түсінікпен шатасуды болдырмау үшін мұндай конструктивті дәлелдеуді кейде тиімді дәлелдеу деп атайды. Конструктивті дәлелдеу конструктивті математикада қолданылатын жарамды дәлелдеудің күшті түсінігін де білдіре алады. Конструктивизм – нақты құрылмаған объектілердің бар екенін пайдаланатын барлық дәлелдеу әдістерін қабылдамайтын математикалық философия. Бұл, атап айтқанда, шығарылған орта заңының, шексіздік аксиомасының және таңдау аксиомасының қолданылуын жоққа шығарады және кейбір терминологияның мағынасын өзгертеді (мысалы, "немесе" термині классикалық математикаға қарағанда конструктивті математикада күшті мағынаға ие). Кейбір конструктивті емес дәлелдеулер белгілі бір тұжырым жалған болса, қайшылыққа келетінін көрсетеді; соның салдарынан тұжырым дұрыс болуы керек (қайшылық арқылы дәлелдеу). Дегенмен, жарылыс принципі (ex falso quodlibet) конструктивті математиканың кейбір түрлерінде, соның ішінде интуиционизмде де қабылданған. Конструктивті дәлелдеулерді сертификатталған математикалық алгоритмдерді анықтау ретінде қарастыруға болады: бұл идея конструктивті логиканың Брауэр–Хейтинг–Колмогоров интерпретациясында, дәлелдеулер мен бағдарламалар арасындағы Керри–Ховард сәйкестігінде, Пер Мартин Лёфтің интуиционистік типтер теориясы және Тьерри Коканд пен Жерар Хюеттің конструкциялар есебі сияқты логикалық жүйелерде зерттеледі.
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non constructive proof (also known as an existence proof or pure existence theorem), which proves the existence of a particular kind of object without providing an example. For avoiding confusion with the stronger concept that follows, such a constructive proof is sometimes called an effective proof. A constructive proof may also refer to the stronger concept of a proof that is valid in constructive mathematics. Constructivism is a mathematical philosophy that rejects all proof methods that involve the existence of objects that are not explicitly built. This excludes, in particular, the use of the law of the excluded middle, the axiom of infinity, and the axiom of choice, and induces a different meaning for some terminology (for example, the term "or" has a stronger meaning in constructive mathematics than in classical). 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. Constructive proofs can be seen as defining certified mathematical algorithms: this idea is explored in the Brouwer–Heyting–Kolmogorov interpretation of constructive logic, the Curry–Howard correspondence between proofs and programs, and such logical systems as Per Martin Löf's intuitionistic type theory, and Thierry Coquand and Gérard Huet's calculus of constructions.
Браувердің қарсы мысалдары
Конструктивті математикада, классикалық математикадағы сияқты, бір мәлімдемеге қарсы мысал келтіру арқылы оны жоққа шығаруға болады. Дегенмен, мәлімдеме конструктивті емес екенін көрсету үшін Брауэрлік қарсы мысал да келтіруге болады. Мұндай қарсы мысал мәлімдеме белгілі бір принципті білдіретінін көрсетеді, ол конструктивті емес. Егер мәлімдеме конструктивті емес принципті білдіретінін конструктивті түрде дәлелдеу мүмкін болса, онда мәлімдеменің өзі конструктивті түрде дәлелденбейді. Мысалы, белгілі бір мәлімдеме, қарама-қарсылық принципін білдіруі мүмкін. Осы типтегі Брауэрлік қарсы мысалдың бір мысалы – Диаконеску теоремасы, ол конструктивті жиын теориясы жүйелерінде таңдау аксиомасы конструктивті емес екенін көрсетеді, себебі таңдау аксиомасы мұндай жүйелерде қарама-қарсылық принципін білдіреді. Конструктивті кері математика саласы бұл идеяны одан әрі дамытады, принциптерді олардың «қаншалықты конструктивті емес» екеніне қарай жіктейді, оларды қарама-қарсылық принципінің әртүрлі бөліктерімен теңестіре отырып. Брауэр «әлсіз» қарсы мысалдарды да ұсынды. Мұндай қарсы мысалдар мәлімдемені жоққа шығармайды, олар тек қазіргі уақытта мәлімдемеге конструктивті дәлелдің жоқ екенін көрсетеді. Бір әлсіз қарсы мысал математикадағы шешілмеген мәселені алудан басталады, мысалы, Гольдбахтың болжамын, ол 4-тен үлкен кез келген жұп табиғи санның екі жай санның қосындысы болатынын сұрайды. Рационал сандардың a(n) тізбесін былай анықтаңыз: әр n үшін a(n) мәні толық іздеу арқылы анықталады, сондықтан a конструктивті түрде жақсы анықталған тізбек. Сонымен қатар, a – конвергенцияның белгілі бір жылдамдығы бар Коши тізбегі болғандықтан, конструктивті математикадағы нақты сандарға қатысты әдеттегідей қарау бойынша, ол кейбір нақты сан α-ға жақындайды. α нақты саны туралы бірнеше фактілерді конструктивті түрде дәлелдеуге болады. Дегенмен, конструктивті математикадағы сөздердің әртүрлі мағынасын ескере отырып, егер «α = 0 немесе α ≠ 0» деген конструктивті дәлел болса, онда бұл Гольдбахтың болжамына конструктивті дәлел бар дегенді білдіреді (бірінші жағдайда) немесе Гольдбахтың болжамының жалған екеніне конструктивті дәлел (екінші жағдайда). Мұндай дәлел жоқ болғандықтан, келтірілген мәлімдемеде де конструктивті дәлел болуы керек емес. Дегенмен, Гольдбахтың болжамы конструктивті дәлелге ие болуы мүмкін (біз қазір оның бар-жоғын білмейміз), бұл жағдайда келтірілген мәлімдеме де конструктивті дәлелге ие болады, бірақ ол қазіргі уақытта белгісіз. Әлсіз қарсы мысалдардың негізгі практикалық қолданылуы – мәселенің «қиындығын» анықтау. Мысалы, жоғарыда келтірілген қарсы мысал келтірілген мәлімдеменің «кем дегенде Гольдбахтың болжамын дәлелдеу сияқты қиын» екенін көрсетеді. Мұндай әлсіз қарсы мысалдар көбінесе шектелген білім принципімен байланысты.
For each n, the value of a(n) can be determined by exhaustive search, and so a is a well defined sequence, constructively. Moreover, because a is a Cauchy sequence with a fixed rate
of convergence, a converges to some real number α, according to the usual treatment of real numbers in constructive mathematics. Several facts about the real number α can be proved constructively. However, based on the different meaning of the words in constructive mathematics, if there is a constructive proof that "α = 0 or α ≠ 0" then this would mean that there is a constructive proof of Goldbach's conjecture (in the former case) or a constructive proof that Goldbach's conjecture is false (in the latter case). Because no such proof is known, the quoted statement must also not have a known constructive proof. However, it is entirely possible that Goldbach's conjecture may have a constructive proof (as we do not know at present whether it does), in which case the quoted statement would have a constructive proof as well, albeit one that is unknown at present. The main practical use of weak counterexamples is to identify the "hardness" of a problem. For example, the counterexample just shown shows that the quoted statement is "at least as hard to prove" as Goldbach's conjecture. Weak counterexamples of this sort are often related to the limited principle of omniscience.