Кіріспе
математикалық дәлелдеу түрі. Деректер бойынша дәлелдеу, сонымен қатар жағдайлар бойынша дәлелдеу, жағдайларды талдау арқылы дәлелдеу, толық индукция немесе қара күш әдісі деп те аталатын бұл математикалық дәлелдеу әдісі, дәлелденуге тиіс мәлімдемені шекті сандағы жағдайларға немесе эквивалентті жағдайлар жиынына бөлуден тұрады, және әрбір жағдайдың қарастырылып отырған ұсыныстың дұрыс екендігі тексеріледі. Бұл тікелей дәлелдеу әдісі. Деректер бойынша дәлелдеу әдетте екі кезеңнен тұрады:
Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds. This is a method of direct proof. A proof by exhaustion typically contains two stages:
A proof that the set of cases is exhaustive; i. e., that each instance of the statement to be proved matches the conditions of (at least) one of the cases. A proof of each of the cases. The prevalence of digital computers has greatly increased the convenience of using the method of exhaustion (e. g., the first computer assisted proof of four color theorem in 1976), though such approaches can also be challenged on the basis of mathematical elegance. Expert systems can be used to arrive at answers to many of the questions posed to them. In theory, the proof by exhaustion method can be used whenever the number of cases is finite. However, because most mathematical sets are infinite, this method is rarely used to derive general mathematical results. In the Curry–Howard isomorphism, proof by exhaustion and case analysis are related to ML style pattern matching.
Біріншіден, жағдайлар жиынының толықтығы дәлелденеді; яғни, дәлелденуге тиіс мәлімдеменің әрбір мысалы (кемінде) бір жағдайдың шарттарына сәйкес келеді. Екіншіден, әрбір жағдайдың дәлелі келтіріледі. Цифрлық компьютерлердің кеңінен таралуы деректер бойынша дәлелдеу әдісін қолданудың ыңғайлылығын арттырды (мысалы, 1976 жылы төрт түс теоремасының алғашқы компьютерлік дәлелі), бірақ мұндай тәсілдер математикалық әсемдік тұрғысынан сынға ұшырауы мүмкін. Сараптық жүйелер оларға қойылған көптеген сұрақтарға жауап беру үшін қолданылуы мүмкін. Теориялық тұрғыдан алғанда, деректер бойынша дәлелдеу әдісі жағдайлар саны шекті болғанда қолданылуы мүмкін. Алайда, математикалық жиынтықтардың көпшілігі шексіз болғандықтан, бұл әдіс жалпы математикалық нәтижелерді алу үшін сирек қолданылады. Кьюри-Ховард изоморфизмінде деректер бойынша дәлелдеу және жағдайларды талдау ML стиліндегі үлгілермен сәйкестендіріледі.
Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds. This is a method of direct proof. A proof by exhaustion typically contains two stages:
A proof that the set of cases is exhaustive; i. e., that each instance of the statement to be proved matches the conditions of (at least) one of the cases. A proof of each of the cases. The prevalence of digital computers has greatly increased the convenience of using the method of exhaustion (e. g., the first computer assisted proof of four color theorem in 1976), though such approaches can also be challenged on the basis of mathematical elegance. Expert systems can be used to arrive at answers to many of the questions posed to them. In theory, the proof by exhaustion method can be used whenever the number of cases is finite. However, because most mathematical sets are infinite, this method is rarely used to derive general mathematical results. In the Curry–Howard isomorphism, proof by exhaustion and case analysis are related to ML style pattern matching.
Көркемдік
Математиктер көптеген жағдайларды қарастырып, сарқып дәлелдеуден аулақ болуды қалайды, себебі мұндай дәлелдеулер әдемі емес деп есептеледі. Мұндай дәлелдеулердің неліктен сәнді емес екенін түсіну үшін, барлық қазіргі заманғы жазғы Олимпиада ойындары 4-ке бөлінетін жылдары өткізіледі деген дәлелді қарастырайық:
Дәлел: Бірінші заманауи жазғы Олимпиада ойындары 1896 жылы өткізілді, содан кейін әр 4 жыл сайын (бірінші және екінші дүниежүзілік соғыстарға байланысты ойындар өткізілмеген, сондай-ақ 2020 жылғы Токио Олимпиадасы COVID-19 пандемиясының салдарынан 2021 жылға шегерілді). 1896 = 474 × 4 болғандықтан, 4-ке бөлінеді, ал келесі Олимпиада 474 × 4 + 4 = (474 + 1) × 4 жылы өткізіледі, бұл да 4-ке бөлінеді, және т.с.с. (бұл математикалық индукция арқылы дәлелдеу). Демек, бұл тұжырым дәлелденді. Бұл тұжырымды жазғы Олимпиада ойындары өткен жылдарды тізімдеп, олардың әрқайсысы 4-ке бөлінетінін тексеру арқылы да дәлелдеуге болады. 2016 жылға дейін 28 жазғы Олимпиада ойындары өткен, сондықтан бұл 28 жағдайды қарастыратын сарқып дәлелдеу болып табылады. Бұл әдемі болмауымен қатар, сарқып дәлелдеу әрбір жаңа жазғы Олимпиада ойындары өткізілген сайын қосымша жағдайды қажет етеді. Бұл математикалық индукция арқылы дәлелдеумен салыстырылады, ол осы тұжырымды болашақта шексіз дәлелдейді.
Істер саны
Деректер санын шектеусіз азайтуға болады. Кейде тек екі-үш жағдай ғана қарастырылады. Ал кейде мыңдаған, тіпті миллиондаған жағдай болуы мүмкін. Мысалы, шахматтың соңғы ойын позициясын қатаң шешу үшін сол мәселенің ойын ағашындағы көптеген мүмкін жағдайларды қарастыру қажет. Төрт түс теоремасының алғашқы дәлелі 1834 жағдайды қарастыру арқылы жүзеге асырылды. Бұл дәлел әртүрлі пікір тудырды, себебі жағдайлардың көп бөлігі компьютерлік бағдарлама арқылы, қолмен тексерілмеді. Бүгінгі күні төрт түс теоремасының ең қысқа дәлелі де 600-дан астам жағдайды қамтиды. Жалпы, дәлелдегі қателік мүмкіндігі жағдайлар саны артуымен бірге өседі. Көп жағдайларды қамтитын дәлел теореманың тек кездейсоқ түрде ғана дұрыс екенін сезім береді, ал оның артында жатқан қандай да бір принцип немесе байланыс жоқ сияқты. Басқа дәлелдеу түрлері, мысалы, индукция арқылы дәлелдеу (математикалық индукция) көбірек талғамды деп есептеледі. Дегенмен, дәлелдеудің басқа әдісі табылмайтын маңызды теоремалар да бар, мысалы:
10-реттік шекті проективтік жазықтықтың жоқтығын дәлелдеу. Шекті қарапайым топтардың жіктелуі. Кеплер болжамы. Бульдік пифагорлық үштіктер мәселесі.
The proof that there is no finite projective plane of order 10. The classification of finite simple groups. The Kepler conjecture. The Boolean Pythagorean triples problem.