Математик иҫбатлау битенең сығанаҡ тексын ҡарарға

{{Значения|Доказательство}}
[[Файл:Oxyrhynchus papyrus with Euclid's Elements.jpg|right|thumb|250px|Бик боронғо замандарҙа табылған, меңйыллыҡтар дауамында иҫбатлау техникаһы өлгөһө булып торған геометрия дәреслегенең, Евклидтың [[Евклидтың Башланғыстары|«Башланғыстары»]] фрагментының береһе<ref>{{cite web
|url=http://www.math.ubc.ca/~cass/Euclid/papyrus/papyrus.html
|title=One of the Oldest Extant Diagrams from Euclid
|author=Bill Casselman
|authorlink=
|coauthors=
|date=
|publisher=University of British Columbia
|accessdate=2008-09-26
}}</ref>]]
'''Математик иҫбатлау''' — ниндәй ҙә булһа раҫлауҙың ([[Теорема|теореманың]]) дөрөҫлөгөн нигеҙләү маҡсатында фекерләү<ref>{{книга
|часть =
|заглавие = Математический энциклопедический словарь
|оригинал =|автор =|ссылка =|isbn = 
|страницы = 211
|год = 1988
|место =  М.
|издательство = [[Большая Российская энциклопедия (издательство)|«Сов. энциклопедия »]]
}}</ref>, билдәле бер [[аксиома]]лар йыйылмаһы дөрөҫ булған осраҡта, математик раҫлау дөрөҫ икәнен күрһәтеүсе логик һығымталар сылбыры.
Бөтә [[математика тарихы]] дауамында {{Переход|#История}} иҫбатлау ысулдары һәм рөхсәт ителгән алымдары һиҙелерлек үҙгәрә, башлыса, нығыраҡ рәсмиләшеү һәм ҙурыраҡ сикләүҙәр яғына. Иҫбатлауҙы рәсмиләштереү мәсьәләһендә төп этап булып XIX быуатта [[Математик логика|математик логиканың]]{{Переход|#Математическая логика}} барлыҡҡа килеүе һәм уны иҫбатлау техникалары саралары менән рәсмиләштереү тора. XX быуатта [[иҫбатлау теорияһы]] — иҫбатлауҙы математик объект булараҡ өйрәнеүсе теория{{Переход|#Теория доказательств}} барлыҡҡа килә. XX быуаттың икенсе яртыһында компьютерҙар барлыҡҡа килгәс, математик иҫбатлау ысулдарын [[Компьютер программаһы|программаларҙы]] тикшереү һәм синтез{{Переход|#Формальная верификация}} өсөн ҡулланыу ҙур әһәмиәткә эйә була, һәм хатта компьютер программалары һәм математик иҫбатлауҙар араһында структуралы ярашлылыҡ ([[соответствие Карри — Ховарда]]{{Переход|#Соответствие Карри — Ховарда}}) урынлаштырыла, уның нигеҙендә [[автоматик иҫбатлау]]{{Переход|#Автоматическое доказательство}} саралары булдырыла.

Иҫбатлауҙы төҙөгәндә ҡулланылған төп алымдар: тура иҫбатлау{{Переход|#Прямое доказательство}}, [[математик индукция]] һәм уның дөйөмләштереүҙәре{{Переход|#Индукция}}, [[киреһенән иҫбатлау]]{{Переход|#Доказательство от противного}}, [[Контрапозиция законы|контрапозиция]]{{Переход|#Контрапозиция}}, төҙөү{{Переход|#Построение}}, берәмтекләп ҡарау{{Переход|#Перебор}}, биекция урынлаштырыу{{Переход|#Биекция}}, ике төрлө иҫәп{{Переход|#Двойной счёт}}; [[Ғәмәли тикшеренеүҙәр|ҡушымталарҙа]] математик иҫбатлау сифатында рәсми иҫбатлау бирмәгән, ләкин һөҙөмтәне практик ҡулланыуҙы тәьмин итеүсе ысулдар{{Переход|#Прикладные методы}} — ихтималлыҡ, статистик, яҡынса йәлеп ителә. Математиканың бүлегенә, ҡулланылған формализмға йәки математик мәктәпкә бәйле рәүештә бөтә ысулдар ҙа ҡаршылыҡһыҙ ҡабул ителә алмай, атап әйткәндә, конструктив иҫбатлау{{Переход|#Конструктивное доказательство}} етди сикләүҙәр талап итә.

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

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

Логик хаталары булған, йәғни уның буйынса рәсми иҫбатлауҙы тергеҙеү мөмкин булмаған текст, хата иҫбатлау тип атала. Математика тарихында күренекле ғалимдар дөрөҫ булмаған «иҫбатлауҙар» баҫтырып сығарған осраҡтар булған, ләкин ғәҙәттә уларҙың коллегалары йәки ғалимдар үҙҙәре тиҙ арала хатаны табалар (айырыуса йыш яңылыш иҫбатланған теоремаларҙың береһе — [[Бөйөк Ферма теоремаһы]]. Әле булһа ла был теореманың иҫбатланған икәнен белмәгән, һәм яңы хаталы «иҫбатлауҙар» тәҡдим итеүселәр осрай<ref name="KvantoFLT">{{статья |автор=Гастев Ю., Смолянский М. |заглавие=Несколько слов о Великой теореме Ферма |издание=[[Квант (журнал)|Квант]] |год=1972 |том=8 |страницы=23—25 |ссылка=http://kvant.mccme.ru/1972/08/neskolko_slov_o_velikoj_teorem.htm}}</ref><ref>{{cite web|author=Цымбалов А. С.|datepublished=|url=http://www.conf.muh.ru/080215/thesis_Tsimbalov.htm|title=Теорема Ферма|work=Доклад на конференцию|publisher=Современная гуманитарная академия|accessdate=2011-5-14|deadlink=yes|archiveurl=https://web.archive.org/web/20090330061311/http://www.conf.muh.ru/080215/thesis_Tsimbalov.htm|archivedate=2009-03-30}} {{Webarchive|url=https://web.archive.org/web/20090330061311/http://www.conf.muh.ru/080215/thesis_Tsimbalov.htm |date=2009-03-30 }}}</ref>).
== Тарихы ==

=== Антиклыҡ ===
[[Боронғо Көнсығыш|Алыҫ Көнсығыш]] илдәрендә ([[Вавилон]]да, [[Боронғо Египет]]та, [[Боронғо Ҡытай|Боронғо Ҡытайҙа]]) математик мәсьәләләрҙең сығарылышы, ҡағиҙә булараҡ, нигеҙләмәйенсә килтерелә һәм [[догма]]тик була, шулай ҙа Пифагор теоремаһының график нигеҙләүҙәрен Вавилондың [[Шына яҙыу|шына яҙыулы таблицаларында]] осратырға мөмкин{{Sfn|Кранц|2011|p=44|loc=The Babylonians had certain diagrams that indicate why the Pythagorean theorem is true, and tablets have been found to validate this fact}}. Иҫбатлау төшөнсәһе б. э. тиклем VIII—VII быуаттарҙа [[Боронғо Греция]]ла ла булмаған. Әммә б. э. тиклем VI быуатта Грецияла логик иҫбатлау дөрөҫлөктө асыҡлауҙың төп ысулы булып китә. Был ваҡытта беренсе математик теориялар һәм донъяның [[Математик модель|математик моделдәре]] төҙөлгән була, улар тулыһынса заман талабына ярашлы күренештә булалар.

Тәүге иҫбатлауҙар иң ябай логик төҙөүҙәрҙе ҡулланғандар. Атап әйткәндә, [[диаметр]] түңәрәкте урталай бүлә, [[Тигеҙ эргәле өсмөйөш|тигеҙ эргәле өсмөйөштөң]] нигеҙе эргәһендәге мөйөштәре тигеҙ, ике киҫешеүсе тура һыҙыҡ тигеҙ мөйөштәр яһай икәнде иҫбатлаусы [[Фалес Милетский]], күрәһең, үҙенең иҫбатлауҙарында фигураларҙы бөкләү һәм өҫтөнә һалыу ысулдарын ҡулланған. Грек философы [[Прокл Диадох|Прокл]] һүҙҙәре буйынса (б. э. V быуаты) <cite>«Ҡайһы берҙә ул мәсьәләләрҙе дөйөм ҡарай, ҡайһы берҙә күргәҙмәлелеккә таяна»</cite>. [[Пифагор]] заманында уҡ иҫбатлау конкрет күҙаллауҙарҙан тик логик һығымталарға күсә{{sfn|История математики, том I|1970|с=65—66}}. [[Парменид]] үҙенең иҫбатлауҙарында [[өсөнсө осраҡтың булмауы законы]]н ҡуллана, ә уның уҡыусыһы [[Зенон Элейский|Зенон]] [[Апории Зенона|апорияларында]] (Апори́я — уйлап сығарылған, логик дөрөҫ хәл (әйтеү, раҫлау, фекерләү йәки һығымта), уның ысын тормошта булыуы мөмкин түгел) [[Абсурд|мәғәнәһеҙлеккә еткереү]] ысулын файҙалана{{Sfn|Бурбаки|1963|с=11}}.

[[Иррациональ һан|Иррационаллек]] төшөнсәһенең нигеҙе булған квадраттың яғы һәм диагоналенең үлсәнмәле булмауын, иҫбатланышы беренсе башлап тик [[Евклидтың Башланғыстары]]нда (X) килтерелһә лә, [[Пифагореизм|пифагорсылар]] иҫбатлаған тип фараз ителә, ул [[Киреһенән сығып иҫбатлау|киреһенән сығып]] иҫбатлана һәм һандарҙың икегә бүленеүсәнлек теорияһына нигеҙләнә{{sfn|История математики, том I|1970|с=73}}. Математик иҫбатлауҙың әһәмиәтенә ҡараштар төрлөлөгө [[Евдокс]] (математиканы [[Теория|теоремалар]] күренешендә ойоштороу традицияһына нигеҙ һалыусы тип иҫәпләнгән, ләкин принципиаль рәүештә иҫбатлауҙарға мөрәжәғәт итмәгән{{Sfn|Кранц|2011|p=44—45|loc=<…> Eudoxus who began the grand tradition of organizing mathematics into theorems <…> What Eudoxus gained in the rigor and precision of his mathematical formulations, he lost because he did not prove anything}}) һәм [[Платон]] араһында конфликт сәбәптәренең береһе булыуы ихтимал {{sfn|История математики, том I|1970|с=95}}.

Математик иҫбатлауҙы рәсмиләштереү юлында [[Аристотель]] тарафынан [[логика]]ны барлыҡҡа килтереү мөһим момент булып тора, ул унда иҫбатлау өсөн ҡулланылған бөтә фекерләү ҡағиҙәләрен системаға һалырға һәм кодификацияларға тырыша, килеп тыуған төп ҡатмарлыҡтарҙы һәм ике мәғәнәлелектәрҙе тасуирлай. Аристотель иҫбатлауҙы фәндең мөһим өлөшө тип һанай, иҫбатлау <cite>«хәл-ваҡиғаларҙың асылын асып бирә» тип иҫәпләй</cite>{{sfn|История математики, том I|1970|с=59—61}}. Ләкин Аристотелдың логикаһы боронғо грек математикаһына туранан-тура йоғонто яһамай, һәм иҫбатлауҙарҙа формаль логика мәсьәләләренә иғтибар итмәйҙәр{{Sfn|Бурбаки|1963|с=12—14|loc=Труды Аристотеля и его преемников, по-видимому, не оказали заметного влияния на математику. Греческие математики в своих исследованиях шли по пути, предложенному пифагорейцами и их последователями в IV в. (Теодором, Теэтетом, Евдоксом), и мало интересовались формальной логикой при изложении своих результатов}}.

=== Урта быуат һәм Яңы осор ===
[[Урта быуаттар|Урта быуаттарҙа]] математика үҫешеү һәм [[схоластика]]нан логикаға таяныуға күсеү менән әкренләп формаль иҫбатлау тураһында төшөнсә булдырыла һәм уның ысулдары үҫешә. [[Математик индукция]] ысулын [[Герсонид]] нигеҙләгән һәм практикаға индергән тип иҫәпләнә<ref>{{статья
 |автор = Rabinovich, N. L. 
 |заглавие = Rabbi Levi ben Gershom and the origins of mathematical induction
 |ссылка =
 |издание =Archive for History of Exact Sciences
 |тип= |место= |издательство= 
 |год=1970 |выпуск=6 |том=|номер=
 |страницы=237—248}}</ref>. XVI быуаттан башлап боронғо грек математиктарының иҫбатлауҙарын тәнҡит күҙлегенән аңларға тырышыу осрай, мәҫәлән [[Пелетье, Жак|Пелетье]], Евклидтың «Башланғыстарына» аңлатма биреп, өсмөйөштәр тигеҙлеген күсеш ярҙамында иҫбатлауҙы тәнҡитләй{{Sfn|Бурбаки|1963|c=27}}.

[[Яңы осор|Яңы осорҙа]] математиканы тәбиғәт фәндәрендә ҡулланыу уңыш ҡаҙаныуы арҡаһында математик раҫлауҙар һәм иҫбатлауҙар ышанысла тип һанала, математика бөтә ҡалған фәндәр өсөн теүәллек һәм иҫбатланыусанлыҡ өлгөһө булып тора. Атап әйткәндә, [[Лейбниц, Готфрид Вильгельм|Лейбниц]] аксиомаларҙы һәм һығымта яһау ҡағиҙәләрен ныҡ тип һанай һәм <cite>«бөтә иҫбат ителерлекте иҫбатлау» өсөн логиканың формаль системаһын төҙөргә тырыша</cite>{{Sfn|Бурбаки|1963|c=22}}. Ләкин, хатта XVIII быуатта ла иҫбатлау төшөнсәһе һаман да рәсмиләшмәгән һәм ҡоро фекерләүгә ҡоролған була, быға шул факт дәлил булып тора ала, [[Эйлер, Леонард|Эйлер]] түбәндәге раҫлауҙарҙы бер үк ваҡытта нигеҙләп була тип иҫәпләй:
: <math>\sum_{n=0}^\infty {1 - (n \operatorname{mod} 2) \cdot 2} = 0</math> һәм <math>\sum_{n=1}^\infty {1 - (n \operatorname{mod} 2) \cdot 2} = 1</math>,
шулай уҡ:
: <math>\sum_{n=0}^\infty {2^n} = -1</math>,
ул әлбиттә раҫлауҙарҙың мәғәнәһеҙлеген аңлай, уларҙың «иҫбатланыусанлығын» парадокс тип һанай{{Sfn|Кранц|2011|p=74—75|loc=3.1. Euler and the Profundity of Intuition}}.

XIX быуатта ҡайһы бер интуитив күренеп торған, формаль ысулдар менән иҫбатлау мөмкин булмаған ҡағиҙәләрҙе постулат итеп алыу кәрәклеге идеялары йышыраҡ тыуып тора. Постулат итеп алынған ҡағиҙәләргә бәйле рәүештә, иҫбатлауҙарҙың сағыштырмалылығын аңлауға тағы ла бер этәргес булып, күп быуаттар буйы [[Евклидтың параллеллек аксиомаһы|Евклидтың параллеллек аксиомаһын]] уңышһыҙ иҫбатларға маташыуҙарҙан һуң [[Лобачевский, Николай Иванович|Лобачевский]], [[Бойяи, Янош|Бойяи]], [[Гаусс, Карл Фридрих|Гаусс]] һәм [[Риман, Георг Фридрих Бернхард|Риман]] тарафынан [[Евклид булмаған геометрия|Евклид булмаған геометрияларҙың]] төҙөлөүе тора{{Sfn|Бурбаки|1963|с=25—26}}.

=== Логиканы рәсмиләштереү һәм Гильберт программаһы ===
{{В планах|дата=30 сентября 2016}}

=== Интуиционизм ===
{{В планах|дата=30 сентября 2016}}

=== Тулы булмағанлыҡ тураһында теоремалар ===
{{В планах|дата=30 сентября 2016}}

=== Конструктивизм ===
{{main|Конструктивная математика}}
{{В планах|дата=30 сентября 2016}}

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

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

== Иҫбатлауҙар теорияһы ==
{{main|Теория доказательств}}
Формаль иҫбатлауҙар менән математиканың махсус тармағы — [[иҫбатлауҙар теорияһы]] шөғөлләнә. Формаль иҫбатлауҙарҙың үҙҙәрен математиктар бер ҡасан да тиерлек ҡулланмайҙар, сөнки кешеләр аңлау өсөн улар бик ҡатмарлы һәм йыш ҡына бик күп урын биләйҙәр.
{{Раздел не завершён}}

== Информатикала ==
[[Информатика|Информатикала]] математик иҫбатлауҙар, иҫбат ителмәле программалау технологиялары сиктәрендә, [[алгоритм]]дарҙы һәм программаларҙы верификациялау һәм дөрөҫлөгөн анализлау өсөн ҡулланыла (ҡарағыҙ. [[логика в информатике]])<!--[[Соответствие Карри — Ховарда]], [[Автоматическое доказательство]]? [[Доказательное программирование]], [[Доказательное программирование]], [[формальная верификация]]-->
{{Раздел не завершён}}

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

=== Тура иҫбатлау ===
{{нп5|Тура иҫбатлау||en|Direct proof}} дөрөҫ тип иҫәпләнгән раҫлауҙарҙан (аксиомаларҙан, элек иҫбатланған леммалар һәм теоремаларҙан), ниндәйҙер раҫлауҙарҙы кире ҡаҡҡан фекерләүҙе ҡулланмайынса, тик туранан-тура дедуктив һығымтаны ҡулланыуҙы күҙ уңында тота{{Sfn|Хаммак|2009|c=95—109|loc=Chapter 4. Direct proof}}. Мәҫәлән, тура иҫбатлау өсөн ошо фигуралар ҡулай тип иҫәпләнә ({{нп5|Натуральный вывод|натураль һығымта|en|Natural deduction}} нотацияһында:
: <math>\frac{A, B}{A}</math>, <math>\frac{A \Rightarrow B, B \Rightarrow C}{A \Rightarrow C}</math>, <math>\frac{A, A \Rightarrow B}{B}</math> ([[modus ponens]]).
Шулай уҡ алмаштырыу тура иҫбатлау ысулы тип иҫәпләнә: әгәр <math>A</math> раҫлауы уға ингән ирекле үҙгәреүсәндең бөтә ҡиммәттәре өсөн дә дөрөҫ булһа, бөтә урында ла уларҙың ниндәй ҙә булһа аҫкүмәклеге урынына ниндәйҙер конкрет ҡиммәтте ҡуйыу ([[формуланың айырым осрағы]]) дөрөҫ раҫлау бирә, натураль һығымта нотацияһында (формаль булмаған яҙыу, бер үҙгәреүсәнгә тиклем ябайлаштырылған):
: <math>\frac{\forall x \, A(x)}{A[x:=a]}</math>

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

Иҫбатлау теорияһында тура иҫбатлауҙың формаль билдәләмәһе бирелгән{{Sfn|Справочная книга по математической логике, том IV|1983|loc=Глава 3. Стетмен Р. Теорема Эрбрана и генценовское понятие прямого доказательства|с=84—99}}.

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

Иң ябай индуктив ысул{{Sfn|Хаммак|2009|c=152—154|loc=Chapter 10. Mathematical Induction}} — [[математик индукция]], [[Натураль һан|натураль рәткә]] ҡарата һығымта, идеяһы ниндәйҙер закондың берәмек өсөн үтәлеүенән һәм һәр артабанғы һан өсөн дөрөҫлөгөнән уның бөтә натураль һандар өсөн үтәлеүен раҫлауҙан тора, натураль һығымта нотацияһында:
: <math>\frac{P(1), \forall n\in \mathbb N (P(n) \Rightarrow P(n+1))}{\forall n \in \mathbb N (P(n))}</math>.

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

Индуктив ысулды [[Иҫәпле булмаған күмәклек|иҫәпле булмаған]] йыйылмаларға таратыу мөмкинлеге ҡатмарлы мәсьәлә булып тора. [[Күмәклектәрҙең хәйләһеҙ теорияһы]] сиктәрендә [[Трансфинит индукция|трансфинит индукция]] ысулы эшләнгән, ул индуктив һығымта яһау ҡағиҙәһен математик индукцияға оҡшаш схема буйынса теләһә ниндәй [[Тулыһынса тәртипкә һалынған күмәклек|тулыһынса тәртипкә һалынған күмәклек]] өсөн таратырға мөмкинлек бирә. [[Интуиционизм|Интуицион логикала]] ла, {{нп5|бар-индукция||en|Bar induction}} булараҡ билдәле булған, индуктивҡа оҡшаш фекерләүҙе иҫәпле булмаған йыйылмалар өсөн ҡулланыу мөмкинлеге табылған<ref>{{Из|МЭ|статья=Бар-индукция|ссылка=http://dic.academic.ru/dic.nsf/enc_mathematics/374/БАР|автор=[[Драгалин, Альберт Григорьевич|Драгалин А. Г.]]}}</ref>.

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

=== Киреһенән сығып иҫбатлау ===
{{Main|Доказательство от противного}}
Киреһенән сығып иҫбатлау [[мәғәнәһеҙлеккә еткереү]] логик алымын ҡуллана һәм ошо схема буйынса төҙөлә: <math>A</math> раҫлауын иҫбат итеү өсөн ул дөрөҫ түгел тип фараз ителә, ә аҙаҡ дедуктив сынйыр буйынса күрәләтә ялған раҫлауға киләләр, мәҫәлән, <math>B \land \neg B</math>, бынан [[Икеләтә инҡар итеү законы|икеләтә инҡар итеү законына]] ярашлы <math>A</math>-ның дөрөҫлөгө тураһында һығымта яһала, натураль һығымта яһау  нотацияһында:
: <math>\frac{\neg A \Rightarrow (B \land \neg B)}{A}</math>.

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

=== Контрапозиция ===
{{нп5|Контрапозицион иҫбатлау ||en|Proof by contrapositive}} [[контрапозиция законы]]н ҡуллана һәм шунан ғибәрәт: <math>A</math> раҫлауынан <math>B</math> раҫлауы килеп сыға тигән фактты иҫбатлау өсөн, <math>B</math>-ны кире ҡағыуҙан <math>A</math>-ны кире ҡағыу килеп сығыуын күрһәтергә кәрәк, натураль һығымта символикаһында:
: <math>\frac{\neg B \Rightarrow \neg A}{A \Rightarrow B}</math>.
Контрапозицион иҫбатлау киреһенән сығып иҫбатлау{{Переход|#От противного}} ысулына ҡайтып ҡала: <math>A \Rightarrow B</math> иҫбатлау өсөн уның <math>\neg (A \Rightarrow B) \equiv \ A \land \neg B</math> кире ҡағыуы тикшерелә, ә <math>\neg B \Rightarrow \neg A \equiv \neg (A \land \neg B)</math> йүнәлтмәһе булғанлыҡтан, ҡапма-ҡаршылыҡ асыҡлана.

Контрапозицион иҫбатлауға миҫал рәүешендә{{Sfn|Хаммак|2009|c=129—138|loc=Chapter 7. Proving Non-Conditional Statements}}, әгәр <math>n^2</math> [[Таҡ һан|таҡ]] булһа, ул саҡта <math>n</math> шулай уҡ таҡ була (<math>n \in \mathbb N</math>) тигән фактты иҫбатлау килтерелә, бының өсөн, әгәр <math>n</math> — йоп булһа, ул саҡта <math>n^2</math> шулай уҡ йоп тигән контрапозиция иҫбатлана.

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

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

=== {{comment|Брутфорс ысулы|барлыҡ булған мөмкинлектәрҙе берәмләп тикшереп сығыу, бөтә мөмкин булған варианттарҙы ҡарап сығыу}} ===
Ҡайһы бер осраҡтарҙа раҫлауҙы иҫбат итеү өсөн, раҫлауҙа әйтелгән йыйылманың бөтә мөмкин булған варианттарын берәмтекләп ҡарап сығалар ([[тулы тикшереү]]) йәки бөтә мөмкин булған варианттар [[Айырым осраҡ (логика)|айырым осраҡтар]] булып торған сикле һандағы кластарға бүленә, һәм һәр береһенә ҡарата иҫбатлау айырым башҡарыла. Ҡағиҙә булараҡ, {{comment|Брутфорс ысулы|барлыҡ булған мөмкинлектәрҙе берәмләп тикшереп сығыу, бөтә мөмкин булған варианттарҙы ҡарап сығыу}} менән иҫбатлау ике этаптан тора:
# бөтә мөмкин булған айырым осраҡтарҙы асыҡлау, һәм башҡа айырым осраҡтар юҡ икәнен иҫбат итеү,
# һәр айырым осраҡты иҫбат итеү.
Варианттар һаны күп булырға мөмкин, мәҫәлән, [[Дүрт буяу проблемаһы|дүрт буяу гипотезаһын]] иҫбат итеү өсөн 2 мең тиерлек төрлө варианттарҙы [[компьютер]] ярҙамында ҡарап сығыу талап ителә. XX быуат аҙағында иҫәпләү техникаһы үҫешеү менән бәйле ошондай иҫбатлауҙарҙың барлыҡҡа килеүе, тикшереү менән проблемалар булыуы ихтималлыҡтан, математика фәнендә уларҙың статусы тураһында мәсьәләне күтәрә<ref>{{статья |автор=Самохин А. В. |заглавие=Проблема четырех красок: неоконченная история доказательства |издание=[[Соросовский образовательный журнал]] |год=2000 |номер=7 |страницы=91—96 |ссылка=http://window.edu.ru/window_catalog/files/r20367/0007_091.pdf }}{{Недоступная ссылка|date=Июль 2018 |bot=InternetArchiveBot }}</ref>.

=== Биекция ===
{{нп5|Биекция урынлаштырыу|en|bijective proof}} ысулы менән иҫбат итеү йыйылманың үлсәме йәки структураһы тураһында, йәки йыйылманы ниндәй ҙә булһа икенсе йыйылма менән сағыштырыу тураһында раҫлауҙарҙы иҫбатлау өсөн ҡулланыла, һәм өйрәнелгән <math>A</math> күмәклеге һәм билдәле үҙсәнлектәргә эйә булған <math>B</math> күмәклеге араһында [[Үҙ-ара-бер ҡиммәтле сағылыш|үҙ-ара-бер ҡиммәтле ярашлыҡ]] төҙөүҙән тора<ref>{{cite web|url=http://www-math.mit.edu/~rstan/bij.pdf|title=Bijective proof problems|author=[[Стэнли, Ричард|Stanley R.]]|date=2009-08-18|work=|publisher=|accessdate=2013-05-12|lang=en|archiveurl=https://www.webcitation.org/6GaJp1gCA?url=http://www-math.mit.edu/~rstan/bij.pdf|archivedate=2013-05-13|deadlink=no}}</ref>. Икенсе төрлө әйткәндә, ниндәйҙер йыйылма тураһында раҫлауҙарҙы иҫбат итеү, был раҫлау дөрөҫ булған йыйылма менән [[Биектив сағылыш|биекция]] төҙөп иҫбатлауға ҡайтарып ҡалдырыла.
Биектив иҫбатлауҙың иң ябай миҫалы — ойоштормалар һаны йәки күмәклектең элементтары һаны тураһында [[Комбинаторика|комбинаторлы]] раҫлауҙарҙы иҫбатлау, ҡатмарлыраҡ миҫалдар — [[изоморфизм]]дар, [[гомеоморфизм]]дар, [[диффеоморфизм]]дар, [[биморфизм]]дар урынлаштырыу, шуның иҫәбенә өйрәнелгән <math>A</math> объектына йәки йыйылмаға  билдәле булған <math>B</math> объектының, биекцияның ошо йәки махсус төрөнә ҡарата [[Инвариант (математика)|инвариантлы]] үҙсәнлектәре күсерелә.

=== Икеләтә иҫәп ===
{{В планах|дата=30 сентября 2016}}

=== Геометрик иҫбатлау ===
[[Файл:Pythagorean proof.png|thumb|Геометрическое доказательство теоремы Пифагора]]
{{В планах|дата=30 сентября 2016}}

== Ғәмәли ысулдар ==

===  Яҡынса ысулдар ===
{{В планах|дата=30 сентября 2016}}

=== Ихтималлыҡ ысулдары ===
{{В планах|дата=30 сентября 2016}}

=== Статистик ысулдар ===
{{В планах|дата=30 сентября 2016}}

== Терминология ==
{{В планах|посвящён=терминам, используемым в доказательствах — «необходимо», «необходимо и достаточно», «тогда и только тогда», «в общем случае», «с точностью до…»|дата=30 сентября 2016}}

== Символдар ==
{{Раздел не завершён}}
Традиция булараҡ иҫбатлауҙың тамамланыуы ҡыҫҡаса «[[Q.E.D.]]» тип тамғалана, латинса {{lang-la|Quod Erat Demonstrandum}} әйтеменән («Шуны иҫбат итеү талап ителә ине»). Хәҙерге хеҙмәттәрҙә иҫбатлауҙың тамамланыуын билдәләү өсөн йышыраҡ □ йәки ■, ‣, // тамғалары, шулай уҡ урыҫ аббревиатураһы ''ч. т. д.'' ҡулланыла.

== Иҫкәрмәләр ==
{{Иҫкәрмәләр}}

== Әҙәбиәт ==
* {{книга |часть=С древнейших времён до начала Нового времени
  |заглавие=История математики |ссылка=http://ilib.mccme.ru/djvu/istoria/istmat1.htm
  |ответственный=Под редакцией [[Юшкевич, Адольф Павлович|Юшкевича А. П.]], в трёх томах
  |место=М. |издательство=Наука |год=1970 |том=I |ref=История математики, том I }}
* {{книга
 |автор         = 
 |заглавие      = Справочная книга по математической логике. IV. Теория доказательств и конструктивная математика
 |оригинал      = Handbook of Mathematical Logic
 |ссылка        = 
 |викитека      = 
 |ответственный = Барвайс Дж.
 |издание       = 
 |место         = М.
 |издательство  = [[Наука (издательство)|Наука]]
 |год           = 1983
 |страниц       = 392
 |ref           = Справочная книга по математической логике, том IV
}}
* {{книга
 |автор         = [[Николя Бурбаки|Бурбаки Н.]]
 |часть         = Основания математики. Логика. Теория множеств
 |ссылка часть  = 
 |заглавие      = Очерки по истории математики
 |оригинал      = 
 |ссылка        = 
 |викитека      = 
 |ответственный = [[Башмакова, Изабелла Григорьевна|И. Г. Башмакова]] (перевод с французского) 
 |издание       = 
 |место         = М
 |издательство  = Издательство иностранной литературы
 |год           = 1963
 |страницы      = 37—53
 |страниц       = 292
 |серия         = Элементы математики
 |тираж         = 
 |ref           = Бурбаки
}}
* {{БСЭ3|автор=[[Гастев, Юрий Алексеевич|Ю. А. Гастев]]|Доказательство|ref=БСЭ}}
* {{книга
 |автор         = Даан-Дальмедико А., Пейффер Ж.
 |заглавие      = Пути и лабиринты. Очерки по истории математики
 |оригинал      = Routes et dédales
 |ссылка        = 
 |викитека      = 
 |ответственный = Перевод с французского А. А. Брядинской под редакцией И. Г. Башмаковой
 |место         = М. 
 |издательство  = Мир
 |год           = 1986
 |страницы      = 394—402
 |страниц       = 432
 |серия         = Современная математика. Популярная серия
 |тираж         = 50 000
 |ref           = Даан-Дальмедико, Пейффер
}}
* {{Книга|автор=[[Владимир Андреевич Успенский]]|заглавие=Простейшие примеры математических доказательств|ссылка=http://www.mccme.ru/mmmf-lectures/books/books/books.php#book-34|ответственный=|издание=|место=|издательство=[[МЦНМО]]|год=2011|страницы=|страниц=56|isbn=978-5-94057-879-6|тираж=2000}}
* {{книга
 |автор         = Franklin J., Daoud A. 
 |заглавие      = Proof in the Mathematics
 |ссылка        = 
 |викитека      = 
 |место         = [[Сидней|Sydney]]
 |издательство  = Quakers Hill Press
 |год           = 2001
 |allpages      = 98
 |серия         = 
 |isbn          = 1876192003
 |тираж         = 
 |ref           = Франклин, Дауд
}}
* {{cite web
 |url         = http://www.people.vcu.edu/~rhammack/BookOfProof/BookOfProof.pdf
 |title       = Book of Proof
 |author      = Hammak R.
 |date        = 2009
 |work        = 
 |publisher   = 
 |accessdate  = 2013-05-11
 |lang        = en
 |ref         = Хаммак2009
 |archiveurl  = https://www.webcitation.org/6GaJpU09p?url=http://www.people.vcu.edu/~rhammack/BookOfProof/BookOfProof.pdf
 |archivedate = 2013-05-13
 |deadlink    = no
}}
* {{книга
 |автор         = {{Нп5|Кранц, Стивен|Krantz S. G.|en|Steven G. Krantz}}
 |заглавие      = The Proof is in the Pudding. A Look at the Changing Nature of Mathematical Proof
 |оригинал      = 
 |ссылка        = http://www.math.wustl.edu/~sk/books/proof.pdf
 |викитека      = 
 |ответственный = 
 |издание       = 
 |место         = N. Y.
 |издательство  = [[Springer Science+Business Media|Springer]]
 |год           = 2011
 |allpages      = 281
 |isbn          = 978-0387489087
 |тираж         = 
 |ref           = Кранц
}}

== Һылтанмалар ==
* [[Ершов, Юрий Леонидович|Ю. Л. Ершов]] ''[https://web.archive.org/web/20090719063356/http://rutube.ru/tracks/1543805.html «Доказательность в математике»]'', программа [[Гордон, Александр Гарриевич|А. Гордона]] от 16 июня 2003 года
[[Категория:Математик логика]]