Математик иҫбатлау

Бик боронғо замандарҙа табылған, меңйыллыҡтар дауамында иҫбатлау техникаһы өлгөһө булып торған геометрия дәреслегенең, Евклидтың «Башланғыстары» фрагментының береһе

Математик иҫбатлау — ниндәй ҙә булһа раҫлауҙың (теореманың) дөрөҫлөгөн нигеҙләү маҡсатында фекерләү, билдәле бер аксиомалар йыйылмаһы дөрөҫ булған осраҡта, математик раҫлау дөрөҫ икәнен күрһәтеүсе логик һығымталар сылбыры. Бөтә математика тарихы дауамында ^[⇨] иҫбатлау ысулдары һәм рөхсәт ителгән алымдары һиҙелерлек үҙгәрә, башлыса, нығыраҡ рәсмиләшеү һәм ҙурыраҡ сикләүҙәр яғына. Иҫбатлауҙы рәсмиләштереү мәсьәләһендә төп этап булып XIX быуатта математик логиканың^[⇨] барлыҡҡа килеүе һәм уны иҫбатлау техникалары саралары менән рәсмиләштереү тора. XX быуатта иҫбатлау теорияһы — иҫбатлауҙы математик объект булараҡ өйрәнеүсе теория^[⇨] барлыҡҡа килә. XX быуаттың икенсе яртыһында компьютерҙар барлыҡҡа килгәс, математик иҫбатлау ысулдарын программаларҙы тикшереү һәм синтез^[⇨] өсөн ҡулланыу ҙур әһәмиәткә эйә була, һәм хатта компьютер программалары һәм математик иҫбатлауҙар араһында структуралы ярашлылыҡ (соответствие Карри — Ховарда^[⇨]) урынлаштырыла, уның нигеҙендә автоматик иҫбатлау^[⇨] саралары булдырыла.

Иҫбатлауҙы төҙөгәндә ҡулланылған төп алымдар: тура иҫбатлау^[⇨], математик индукция һәм уның дөйөмләштереүҙәре^[⇨], киреһенән иҫбатлау^[⇨], контрапозиция^[⇨], төҙөү^[⇨], берәмтекләп ҡарау^[⇨], биекция урынлаштырыу^[⇨], ике төрлө иҫәп^[⇨]; ҡушымталарҙа математик иҫбатлау сифатында рәсми иҫбатлау бирмәгән, ләкин һөҙөмтәне практик ҡулланыуҙы тәьмин итеүсе ысулдар^[⇨] — ихтималлыҡ, статистик, яҡынса йәлеп ителә. Математиканың бүлегенә, ҡулланылған формализмға йәки математик мәктәпкә бәйле рәүештә бөтә ысулдар ҙа ҡаршылыҡһыҙ ҡабул ителә алмай, атап әйткәндә, конструктив иҫбатлау^[⇨] етди сикләүҙәр талап итә.

Математикала иҫбатлауҙың әһәмиәте

Башҡа фәндәрҙән айырмалы рәүештә, математикала эмпирик иҫбатлауҙарға юл ҡуйылмай: бөтә раҫлауҙар ҙа фәҡәт логик ысулдар менән иҫбатлана. Математикала төрлө объекттар һәм теоремалар араһында математик интуиция һәм аналогия мөһим роль уйнай; шулай булыуға ҡарамаҫтан, бөтә был саралар ғалимдар тарафынан тик иҫбатлау юлдарын эҙләгәндә генә ҡулланыла, иҫбатлау үҙе бындай сараларға нигеҙләнә алмай. Тәбиғи телдә яҙылған иҫбатлауҙар, аңлы уҡыусы деталдәрҙе үҙе тулыландыра ала тигән иҫәп менән, бик үк эҙмә-эҙлекле булмаҫҡа мөмкин. Иҫбатлауҙың ҡәтғилеге, уны формаль телдәге яҙыу рәүешендә күрһәтергә мөмкин булыуы менән гарантиялана (иҫбатлауҙы компьютер ярҙамында тикшергәндә шулай була ла инде). Ҡалып:Раздел не завершён

Раҫлауҙарҙың статусы

Математикала иҫбатланған раҫлау теорема тип атала (математик текстарҙа ғәҙәттә иҫбатлау кем тарафынандыр табылған тип фараз ителә; логика буйынса эштәр был ғәҙәттән ситләшеү булып тора, унда иҫбатлау төшөнсәһе үҙе тикшерелә); әгәр раҫлау ҙа, уны кире ҡағыу ҙа әле иҫбатланмаған булһа, бындай раҫлауҙы гипотеза тип атайҙар. Ҡайһы бер осраҡтарҙа теореманы иҫбатлау барышында лемма исеме аҫтында билдәле ябайыраҡ раҫлауҙар иҫбатлана.

Логик хаталары булған, йәғни уның буйынса рәсми иҫбатлауҙы тергеҙеү мөмкин булмаған текст, хата иҫбатлау тип атала. Математика тарихында күренекле ғалимдар дөрөҫ булмаған «иҫбатлауҙар» баҫтырып сығарған осраҡтар булған, ләкин ғәҙәттә уларҙың коллегалары йәки ғалимдар үҙҙәре тиҙ арала хатаны табалар (айырыуса йыш яңылыш иҫбатланған теоремаларҙың береһе — Бөйөк Ферма теоремаһы. Әле булһа ла был теореманың иҫбатланған икәнен белмәгән, һәм яңы хаталы «иҫбатлауҙар» тәҡдим итеүселәр осрай).

Тарихы

Антиклыҡ

Алыҫ Көнсығыш илдәрендә (Вавилонда, Боронғо Египетта, Боронғо Ҡытайҙа) математик мәсьәләләрҙең сығарылышы, ҡағиҙә булараҡ, нигеҙләмәйенсә килтерелә һәм догматик була, шулай ҙа Пифагор теоремаһының график нигеҙләүҙәрен Вавилондың шына яҙыулы таблицаларында осратырға мөмкин. Иҫбатлау төшөнсәһе б. э. тиклем VIII—VII быуаттарҙа Боронғо Грецияла ла булмаған. Әммә б. э. тиклем VI быуатта Грецияла логик иҫбатлау дөрөҫлөктө асыҡлауҙың төп ысулы булып китә. Был ваҡытта беренсе математик теориялар һәм донъяның математик моделдәре төҙөлгән була, улар тулыһынса заман талабына ярашлы күренештә булалар.

Тәүге иҫбатлауҙар иң ябай логик төҙөүҙәрҙе ҡулланғандар. Атап әйткәндә, диаметр түңәрәкте урталай бүлә, тигеҙ эргәле өсмөйөштөң нигеҙе эргәһендәге мөйөштәре тигеҙ, ике киҫешеүсе тура һыҙыҡ тигеҙ мөйөштәр яһай икәнде иҫбатлаусы Фалес Милетский, күрәһең, үҙенең иҫбатлауҙарында фигураларҙы бөкләү һәм өҫтөнә һалыу ысулдарын ҡулланған. Грек философы Прокл һүҙҙәре буйынса (б. э. V быуаты) «Ҡайһы берҙә ул мәсьәләләрҙе дөйөм ҡарай, ҡайһы берҙә күргәҙмәлелеккә таяна». Пифагор заманында уҡ иҫбатлау конкрет күҙаллауҙарҙан тик логик һығымталарға күсә. Парменид үҙенең иҫбатлауҙарында өсөнсө осраҡтың булмауы законын ҡуллана, ә уның уҡыусыһы Зенон апорияларында (Апори́я — уйлап сығарылған, логик дөрөҫ хәл (әйтеү, раҫлау, фекерләү йәки һығымта), уның ысын тормошта булыуы мөмкин түгел) мәғәнәһеҙлеккә еткереү ысулын файҙалана.

Иррационаллек төшөнсәһенең нигеҙе булған квадраттың яғы һәм диагоналенең үлсәнмәле булмауын, иҫбатланышы беренсе башлап тик Евклидтың Башланғыстарында (X) килтерелһә лә, пифагорсылар иҫбатлаған тип фараз ителә, ул киреһенән сығып иҫбатлана һәм һандарҙың икегә бүленеүсәнлек теорияһына нигеҙләнә. Математик иҫбатлауҙың әһәмиәтенә ҡараштар төрлөлөгө Евдокс (математиканы теоремалар күренешендә ойоштороу традицияһына нигеҙ һалыусы тип иҫәпләнгән, ләкин принципиаль рәүештә иҫбатлауҙарға мөрәжәғәт итмәгән) һәм Платон араһында конфликт сәбәптәренең береһе булыуы ихтимал .

Математик иҫбатлауҙы рәсмиләштереү юлында Аристотель тарафынан логиканы барлыҡҡа килтереү мөһим момент булып тора, ул унда иҫбатлау өсөн ҡулланылған бөтә фекерләү ҡағиҙәләрен системаға һалырға һәм кодификацияларға тырыша, килеп тыуған төп ҡатмарлыҡтарҙы һәм ике мәғәнәлелектәрҙе тасуирлай. Аристотель иҫбатлауҙы фәндең мөһим өлөшө тип һанай, иҫбатлау «хәл-ваҡиғаларҙың асылын асып бирә» тип иҫәпләй. Ләкин Аристотелдың логикаһы боронғо грек математикаһына туранан-тура йоғонто яһамай, һәм иҫбатлауҙарҙа формаль логика мәсьәләләренә иғтибар итмәйҙәр.

Урта быуат һәм Яңы осор

Урта быуаттарҙа математика үҫешеү һәм схоластиканан логикаға таяныуға күсеү менән әкренләп формаль иҫбатлау тураһында төшөнсә булдырыла һәм уның ысулдары үҫешә. Математик индукция ысулын Герсонид нигеҙләгән һәм практикаға индергән тип иҫәпләнә. XVI быуаттан башлап боронғо грек математиктарының иҫбатлауҙарын тәнҡит күҙлегенән аңларға тырышыу осрай, мәҫәлән Пелетье, Евклидтың «Башланғыстарына» аңлатма биреп, өсмөйөштәр тигеҙлеген күсеш ярҙамында иҫбатлауҙы тәнҡитләй.

Яңы осорҙа математиканы тәбиғәт фәндәрендә ҡулланыу уңыш ҡаҙаныуы арҡаһында математик раҫлауҙар һәм иҫбатлауҙар ышанысла тип һанала, математика бөтә ҡалған фәндәр өсөн теүәллек һәм иҫбатланыусанлыҡ өлгөһө булып тора. Атап әйткәндә, Лейбниц аксиомаларҙы һәм һығымта яһау ҡағиҙәләрен ныҡ тип һанай һәм «бөтә иҫбат ителерлекте иҫбатлау» өсөн логиканың формаль системаһын төҙөргә тырыша. Ләкин, хатта XVIII быуатта ла иҫбатлау төшөнсәһе һаман да рәсмиләшмәгән һәм ҡоро фекерләүгә ҡоролған була, быға шул факт дәлил булып тора ала, Эйлер түбәндәге раҫлауҙарҙы бер үк ваҡытта нигеҙләп була тип иҫәпләй:

$\sum _{n=0}^{\infty }{1-(n\operatorname {mod} 2)\cdot 2}=0$ һәм $\sum _{n=1}^{\infty }{1-(n\operatorname {mod} 2)\cdot 2}=1$,

шулай уҡ:

$\sum _{n=0}^{\infty }{2^{n}}=-1$,

ул әлбиттә раҫлауҙарҙың мәғәнәһеҙлеген аңлай, уларҙың «иҫбатланыусанлығын» парадокс тип һанай.

XIX быуатта ҡайһы бер интуитив күренеп торған, формаль ысулдар менән иҫбатлау мөмкин булмаған ҡағиҙәләрҙе постулат итеп алыу кәрәклеге идеялары йышыраҡ тыуып тора. Постулат итеп алынған ҡағиҙәләргә бәйле рәүештә, иҫбатлауҙарҙың сағыштырмалылығын аңлауға тағы ла бер этәргес булып, күп быуаттар буйы Евклидтың параллеллек аксиомаһын уңышһыҙ иҫбатларға маташыуҙарҙан һуң Лобачевский, Бойяи, Гаусс һәм Риман тарафынан Евклид булмаған геометрияларҙың төҙөлөүе тора.

Формаль иҫбатлау

Формаль иҫбатлау тураһында һөйләгәндә, бөтәһенән алда формаль моделде — формаль тел ярҙамында яҙылған аксиомалар күмәклеген, һәм һығымта яһау ҡағиҙәләрен тасуирлайҙар . Формаль һығымта тип, формаль телдә яҙылған, һәр береһе йә аксиома, йә алдағы юлдарҙан һығымта яһау ҡағиҙәләренең береһен ҡулланып табылған юлдарҙың сикле тәртипкә һалынған күмәклеге атала. Раҫлауҙы формаль иҫбатлау тип, һуңғы юлы бирелгән раҫлау булған формаль һығымта яһау атала. Формаль иҫбатланышы булған раҫлау, теорема тип, ә бирелгән формаль моделдә (формаль тел алфавиты, аксиомалар һәм һығымта яһау ҡағиҙәләре менән бергә ҡаралған) бөтә теоремалар күмәклеге формаль теория тип атала.

Әгәр теләһә ниндәй раҫлау өсөн уның үҙен йәки уның кире ҡағылышын иҫбатлап булһа, теория тулы тип атала. Әгәр теорияла раҫлауҙың үҙен уның кире ҡағылышы менән бергә иҫбатларға мөмкин булмаһа (йәки, шуға эквивалентлы, әгәр унда бер генә булһа ла иҫбатлап булмаған раҫлау булмаһа), теория ҡаршылыҡһыҙ тип атала. «Етерлек бай» математик теорияларҙың күбеһе, Гёделдың тулы булмау тураһында беренсе теоремаһы күрһәткәнсә, тулы түгелдәр йәки ҡаршылыҡлы булалар. Хәҙерге ваҡытта иң киң таралған аксиомалар йыйылмаһы булып, һайлау аксиомаһы менән бергә Цермело — Френкель аксиоматикаһы (ҡайһы бер математиктар һайлау аксиомаһын ҡулланыуға ҡарша сыҡһалар ҙа) тора. Был аксиомалар системаһы нигеҙендәге теория тулы түгел (мәҫәлән, унда континуум-гипотеза, был теория ҡаршылыҡһыҙ тип уйлағанда, иҫбатлана ла, кире ҡағыла ла алмай). Был теорияны математикала бөтә ерҙә лә ҡулланыуға ҡарамаҫтан, уның ҡаршылыҡһыҙ булыуы үҙенең ысулдары менән иҫбат ителә алмай. Шулай булыуға ҡарамаҫтан, күпселек математиктар уның ҡаршылыҡһыҙ булыуына ышана, кире осраҡта ҡапма-ҡаршылыҡтар күптән беленер ине тип иҫәпләйҙәр.

Иҫбатлауҙар теорияһы

Формаль иҫбатлауҙар менән математиканың махсус тармағы — иҫбатлауҙар теорияһы шөғөлләнә. Формаль иҫбатлауҙарҙың үҙҙәрен математиктар бер ҡасан да тиерлек ҡулланмайҙар, сөнки кешеләр аңлау өсөн улар бик ҡатмарлы һәм йыш ҡына бик күп урын биләйҙәр. Ҡалып:Раздел не завершён

Информатикала

Информатикала математик иҫбатлауҙар, иҫбат ителмәле программалау технологиялары сиктәрендә, алгоритмдарҙы һәм программаларҙы верификациялау һәм дөрөҫлөгөн анализлау өсөн ҡулланыла (ҡарағыҙ. логика в информатике) Ҡалып:Раздел не завершён

Формаль иҫбатлау ысулдары

Тура иҫбатлау

Тура иҫбатлау^[en] дөрөҫ тип иҫәпләнгән раҫлауҙарҙан (аксиомаларҙан, элек иҫбатланған леммалар һәм теоремаларҙан), ниндәйҙер раҫлауҙарҙы кире ҡаҡҡан фекерләүҙе ҡулланмайынса, тик туранан-тура дедуктив һығымтаны ҡулланыуҙы күҙ уңында тота. Мәҫәлән, тура иҫбатлау өсөн ошо фигуралар ҡулай тип иҫәпләнә (натураль һығымта^[en] нотацияһында:

${\frac {A,B}{A}}$, ${\frac {A\Rightarrow B,B\Rightarrow C}{A\Rightarrow C}}$, ${\frac {A,A\Rightarrow B}{B}}$ (modus ponens).

Шулай уҡ алмаштырыу тура иҫбатлау ысулы тип иҫәпләнә: әгәр $A$ раҫлауы уға ингән ирекле үҙгәреүсәндең бөтә ҡиммәттәре өсөн дә дөрөҫ булһа, бөтә урында ла уларҙың ниндәй ҙә булһа аҫкүмәклеге урынына ниндәйҙер конкрет ҡиммәтте ҡуйыу (формуланың айырым осрағы) дөрөҫ раҫлау бирә, натураль һығымта нотацияһында (формаль булмаған яҙыу, бер үҙгәреүсәнгә тиклем ябайлаштырылған):

${\frac {\forall x\,A(x)}{A[x:=a]}}$

Ҡайһы бер осраҡтарҙа кире ҡағып фекерләүҙе ҡулланыусы тура булмаған иҫбатлауҙар, бигерәк тә сикле объекттарға ҡарата, ябай ғына итеп, дөйөмлөккә зыян килтермәй, тура иҫбатлауға ҡайтарып ҡалдырыла алалар, ләкин сикһеҙ тупланмалар тураһында раҫлауҙарға ҡарата был һәр ваҡытта ла улай булмай, һәм конструктив иҫбатлауҙарҙың XX быуат математикаһында әһәмиәте артыу менән, тура булмаған ысулдар менән иҫбатланған раҫлауҙарҙың тура иҫбатланышын табыу мөһим тип һанала.

Иҫбатлау теорияһында тура иҫбатлауҙың формаль билдәләмәһе бирелгән.

Индукция

Айырым раҫлауҙарҙан дөйөм раҫлауҙарға күсергә мөмкинлек биргән индуктив ысулды объекттарҙың сикһеҙ тупланмаһына ҡулланыу айырыуса ҡыҙыҡлы, ләкин уның әйтелеше һәм ҡулланыусанлығы ҡулланыу өлкәһенә бәйле рәүештә һиҙелерлек айырыла.

Иң ябай индуктив ысул — математик индукция, натураль рәткә ҡарата һығымта, идеяһы ниндәйҙер закондың берәмек өсөн үтәлеүенән һәм һәр артабанғы һан өсөн дөрөҫлөгөнән уның бөтә натураль һандар өсөн үтәлеүен раҫлауҙан тора, натураль һығымта нотацияһында:

${\frac {P(1),\forall n\in \mathbb {N} (P(n)\Rightarrow P(n+1))}{\forall n\in \mathbb {N} (P(n))}}$.

Математик индукция ысулы объекттарҙың теләһә ниндәй иҫәпле йыйылмаһы өсөн тәбиғи рәүештә ҡулланылырға мөмкин, иҫбатлауҙарҙың классик, шулай уҡ интуицион һәм конструктив системаларында ышаныслы һәм законлы тип иҫәпләнә. Ысул Пеано арифметикаһы аксиомалары системаһында аксиомалаштырыла.

Индуктив ысулды иҫәпле булмаған йыйылмаларға таратыу мөмкинлеге ҡатмарлы мәсьәлә булып тора. Күмәклектәрҙең хәйләһеҙ теорияһы сиктәрендә трансфинит индукция ысулы эшләнгән, ул индуктив һығымта яһау ҡағиҙәһен математик индукцияға оҡшаш схема буйынса теләһә ниндәй тулыһынса тәртипкә һалынған күмәклек өсөн таратырға мөмкинлек бирә. Интуицион логикала ла, бар-индукция^[en] булараҡ билдәле булған, индуктивҡа оҡшаш фекерләүҙе иҫәпле булмаған йыйылмалар өсөн ҡулланыу мөмкинлеге табылған.

Структуралы индукцияның, индукцияны объекттарҙың тулыһынса тәртипкә һалынған йыйылмаларына ҡарата, уларға рекурсив билдәләмә биргән осраҡта ҡулланырға мөмкинлек биргән конструктив ысулы бар.

Киреһенән сығып иҫбатлау

Киреһенән сығып иҫбатлау мәғәнәһеҙлеккә еткереү логик алымын ҡуллана һәм ошо схема буйынса төҙөлә: $A$ раҫлауын иҫбат итеү өсөн ул дөрөҫ түгел тип фараз ителә, ә аҙаҡ дедуктив сынйыр буйынса күрәләтә ялған раҫлауға киләләр, мәҫәлән, $B\land \neg B$, бынан икеләтә инҡар итеү законына ярашлы $A$-ның дөрөҫлөгө тураһында һығымта яһала, натураль һығымта яһау нотацияһында:

${\frac {\neg A\Rightarrow (B\land \neg B)}{A}}$.

Интуицион һәм конструктив системаларҙа киреһенән сығып иҫбатлау ҡулланылмай, сөнки икеләтә инҡар итеү законы ҡабул ителмәй.

Контрапозиция

Контрапозицион иҫбатлау^[en] контрапозиция законын ҡуллана һәм шунан ғибәрәт: $A$ раҫлауынан $B$ раҫлауы килеп сыға тигән фактты иҫбатлау өсөн, $B$-ны кире ҡағыуҙан $A$-ны кире ҡағыу килеп сығыуын күрһәтергә кәрәк, натураль һығымта символикаһында:

${\frac {\neg B\Rightarrow \neg A}{A\Rightarrow B}}$.

Контрапозицион иҫбатлау киреһенән сығып иҫбатлау^[⇨] ысулына ҡайтып ҡала: $A\Rightarrow B$ иҫбатлау өсөн уның $\neg (A\Rightarrow B)\equiv \ A\land \neg B$ кире ҡағыуы тикшерелә, ә $\neg B\Rightarrow \neg A\equiv \neg (A\land \neg B)$ йүнәлтмәһе булғанлыҡтан, ҡапма-ҡаршылыҡ асыҡлана.

Контрапозицион иҫбатлауға миҫал рәүешендә, әгәр $n^{2}$ таҡ булһа, ул саҡта $n$ шулай уҡ таҡ була ($n\in \mathbb {N}$) тигән фактты иҫбатлау килтерелә, бының өсөн, әгәр $n$ — йоп булһа, ул саҡта $n^{2}$ шулай уҡ йоп тигән контрапозиция иҫбатлана.

Икеләтә кире ҡағыу законын ҡабул итмәгән системаларҙа контрапозицион иҫбатлау ҡулланылмай.

Төҙөү

Һығымта сифатында билдәле бер сифаттарға эйә булған ниндәйҙер объекттың булыуы әйтелгән ысынбарлыҡ теоремаһы тибындағы раҫлауҙар өсөн, мәҫәлән, ниндәйҙер шарттарҙы ҡәнәғәтләндергән һандың булыуы, иҫбатлауҙың иң хас булған төрө — ярашлы формаль системаның ысулдарын ҡулланып туранан-тура эҙләнгән объектты табыу. Күп классик ысынбарлыҡ теоремалары киреһенән сығып, йәғни бирелгән үҙсәнлектәргә эйә булған объект юҡ тип фараз итеүҙе мәғәнәһеҙлеккә еткереү юлы менән иҫбатланғандар, ләкин ундай иҫбатлауҙар конструктив түгел тип иҫәпләнәләр, һәм, ярашлы рәүештә, интуицион һәм конструктив математикала бындай раҫлауҙар өсөн тик төҙөү юлы менән иҫбатлау ҡулланыла.

Брутфорс ысулы

Ҡайһы бер осраҡтарҙа раҫлауҙы иҫбат итеү өсөн, раҫлауҙа әйтелгән йыйылманың бөтә мөмкин булған варианттарын берәмтекләп ҡарап сығалар (тулы тикшереү) йәки бөтә мөмкин булған варианттар айырым осраҡтар булып торған сикле һандағы кластарға бүленә, һәм һәр береһенә ҡарата иҫбатлау айырым башҡарыла. Ҡағиҙә булараҡ, Брутфорс ысулы менән иҫбатлау ике этаптан тора:

1. бөтә мөмкин булған айырым осраҡтарҙы асыҡлау, һәм башҡа айырым осраҡтар юҡ икәнен иҫбат итеү,
2. һәр айырым осраҡты иҫбат итеү.

Варианттар һаны күп булырға мөмкин, мәҫәлән, дүрт буяу гипотезаһын иҫбат итеү өсөн 2 мең тиерлек төрлө варианттарҙы компьютер ярҙамында ҡарап сығыу талап ителә. XX быуат аҙағында иҫәпләү техникаһы үҫешеү менән бәйле ошондай иҫбатлауҙарҙың барлыҡҡа килеүе, тикшереү менән проблемалар булыуы ихтималлыҡтан, математика фәнендә уларҙың статусы тураһында мәсьәләне күтәрә.

Биекция

en^{[bijective proof]} ысулы менән иҫбат итеү йыйылманың үлсәме йәки структураһы тураһында, йәки йыйылманы ниндәй ҙә булһа икенсе йыйылма менән сағыштырыу тураһында раҫлауҙарҙы иҫбатлау өсөн ҡулланыла, һәм өйрәнелгән $A$ күмәклеге һәм билдәле үҙсәнлектәргә эйә булған $B$ күмәклеге араһында үҙ-ара-бер ҡиммәтле ярашлыҡ төҙөүҙән тора. Икенсе төрлө әйткәндә, ниндәйҙер йыйылма тураһында раҫлауҙарҙы иҫбат итеү, был раҫлау дөрөҫ булған йыйылма менән биекция төҙөп иҫбатлауға ҡайтарып ҡалдырыла. Биектив иҫбатлауҙың иң ябай миҫалы — ойоштормалар һаны йәки күмәклектең элементтары һаны тураһында комбинаторлы раҫлауҙарҙы иҫбатлау, ҡатмарлыраҡ миҫалдар — изоморфизмдар, гомеоморфизмдар, диффеоморфизмдар, биморфизмдар урынлаштырыу, шуның иҫәбенә өйрәнелгән $A$ объектына йәки йыйылмаға билдәле булған $B$ объектының, биекцияның ошо йәки махсус төрөнә ҡарата инвариантлы үҙсәнлектәре күсерелә.

Геометрик иҫбатлау

Геометрическое доказательство теоремы Пифагора

Символдар

Ҡалып:Раздел не завершён Традиция булараҡ иҫбатлауҙың тамамланыуы ҡыҫҡаса «Q.E.D.» тип тамғалана, латинса лат. Quod Erat Demonstrandum әйтеменән («Шуны иҫбат итеү талап ителә ине»). Хәҙерге хеҙмәттәрҙә иҫбатлауҙың тамамланыуын билдәләү өсөн йышыраҡ □ йәки ■, ‣, // тамғалары, шулай уҡ урыҫ аббревиатураһы ч. т. д. ҡулланыла.

Әҙәбиәт

• С древнейших времён до начала Нового времени // История математики / Под редакцией Юшкевича А. П., в трёх томах. — М.: Наука, 1970. — Т. I.
• Справочная книга по математической логике. IV. Теория доказательств и конструктивная математика = Handbook of Mathematical Logic / Барвайс Дж.. — М.: Наука, 1983. — 392 с.
• Бурбаки Н. Основания математики. Логика. Теория множеств // Очерки по истории математики / И. Г. Башмакова (перевод с французского). — М: Издательство иностранной литературы, 1963. — С. 37—53. — 292 с. — (Элементы математики).
• Доказательство / Ю. А. Гастев // Большая советская энциклопедия : [в 30 т.] / гл. ред. А. М. Прохоров. — 3-е изд. — М. : Советская энциклопедия, 1969—1978.
• Даан-Дальмедико А., Пейффер Ж. Пути и лабиринты. Очерки по истории математики = Routes et dédales / Перевод с французского А. А. Брядинской под редакцией И. Г. Башмаковой. — М.: Мир, 1986. — С. 394—402. — 432 с. — (Современная математика. Популярная серия). — 50 000 экз.
• Владимир Андреевич Успенский. Простейшие примеры математических доказательств. — МЦНМО, 2011. — 56 с. — 2000 экз. — ISBN 978-5-94057-879-6.
• Franklin J., Daoud A. Proof in the Mathematics. — Sydney: Quakers Hill Press, 2001. — 98 p. — ISBN 1876192003.
• Hammak R. Book of Proof (ингл.) (2009). Дата обращения: 11 май 2013. Архивировано 13 май 2013 года.
• Krantz S. G.^[en]. The Proof is in the Pudding. A Look at the Changing Nature of Mathematical Proof. — N. Y.: Springer, 2011. — 281 p. — ISBN 978-0387489087.

Һылтанмалар

• Ю. Л. Ершов «Доказательность в математике», программа А. Гордона от 16 июня 2003 года