Matematický důkaz | |
---|---|
Studoval v | teorie důkazů |
Účel projektu nebo mise | teorém |
Mediální soubory na Wikimedia Commons |
Matematický důkaz - uvažování ospravedlnit pravdivost tvrzení ( teorém ) [2] , řetězec logických závěrů ukazovat to, podřízený pravdivosti jistého souboru axiomů a pravidel závěru , sdělení je pravdivé. V závislosti na kontextu to může znamenat důkaz v rámci určitého formálního systému (posloupnost výroků sestavená podle zvláštních pravidel, psaná ve formálním jazyce ) nebo text v přirozeném jazyce ., ze kterého v případě potřeby můžeme obnovit formální důkaz. Potřeba formálního důkazu tvrzení je jedním z hlavních charakteristických rysů matematiky jako deduktivního oboru vědění, respektive pojem důkaz hraje ústřední roli v předmětu matematika , a dostupnost důkazů a jejich správnost určení stavu případných matematických výsledků .
V průběhu historie matematiky se představa o metodách a přijatelných metodách dokazování výrazně měnila, především ve směru větší formalizace a větších omezení. Klíčovým mezníkem v problematice formalizace důkazů bylo vytvoření matematické logiky v 19. století a její formalizace pomocí základních důkazních technik. Ve 20. století byla vybudována teorie důkazů – teorie, která studuje důkaz jako matematický objekt . S příchodem počítačů ve druhé polovině 20. století se používání matematických důkazových metod pro kontrolu a syntézu programů stalo obzvláště důležitým , a dokonce byla vytvořena strukturální korespondence mezi počítačovými programy a matematickými důkazy ( korespondence Curry-Howard ), na jehož základě prostředky automatického důkazu .
Hlavní techniky používané při konstrukci důkazů: přímý důkaz , matematická indukce a její zobecnění , důkaz kontradikcí , kontrapozice , konstrukce , výčet , stanovení bijekce , dvojitý počet ; v aplikacích se jako matematické důkazy používají i metody, které neposkytují formální důkaz, ale zajišťují praktickou použitelnost výsledku - pravděpodobnostní, statistický, přibližný. V závislosti na oboru matematiky, použitém formalismu nebo matematické škole nelze všechny metody bezpodmínečně akceptovat, zejména konstruktivní důkaz obsahuje vážná omezení.
Na rozdíl od jiných věd je empirický důkaz v matematice nepřijatelný: všechna tvrzení jsou dokazována výhradně logickými prostředky. Matematická intuice a analogie mezi různými objekty a teorémy hrají v matematice důležitou roli; všechny tyto prostředky však vědci využívají pouze při hledání důkazů, samotný důkaz o takové prostředky nemůže být založen. Důkazy psané v přirozených jazycích nemusí být příliš podrobné, s očekáváním, že trénovaný čtenář bude schopen rekonstruovat podrobnosti pro sebe. Přísnost důkazu je zaručena tím, že může být vyjádřen ve formě záznamu ve formálním jazyce (to se děje, když počítač kontroluje důkazy).
Dokázaná tvrzení v matematice se nazývají teorémy (v matematických textech se obvykle předpokládá, že důkaz někdo našel; výjimkou z tohoto zvyku jsou především práce o logice, v nichž se zkoumá samotný pojem důkazu); pokud ještě nebylo prokázáno ani tvrzení, ani jeho negace, pak se takové tvrzení nazývá hypotéza . Někdy jsou v procesu dokazování věty zvýrazněny důkazy méně komplikovaných tvrzení, nazývaných lemmata .
Některá matematická tvrzení jsou tradičně známa pod názvy, které neodpovídají jejich skutečnému stavu. Fermatova poslední věta tak nebyla nikdy nazývána Fermatovou hypotézou, a to ještě před jejím důkazem Andrewem Wilesem . Na druhou stranu, domněnka Poincare nadále nese toto jméno i po jejím důkazu G. Ya.Perelmanem .
Chybný důkaz je text obsahující logické chyby, tedy takový, ze kterého nelze obnovit formální důkaz. V historii matematiky se vyskytly případy, kdy významní vědci publikovali nesprávné „důkazy“, ale většinou jejich kolegové nebo oni sami rychle našli chyby (jednou z nejčastěji nesprávně dokázaných vět je Fermatova poslední věta . Stále existují lidé, kteří ne vědět o tom, že to bylo prokázáno, a nabízet nové falešné „důkazy“ [3] [4] ). Může být pouze chybné uznat jako důkaz „důkaz“ v přirozeném nebo formálním jazyce; formální důkaz nemůže být z definice nesprávný.
V zemích starověkého východu ( Babylon , Starověký Egypt , Starověká Čína ) bylo řešení matematických problémů zpravidla dáno neopodstatněně a bylo dogmatické , i když grafické odůvodnění Pythagorovy věty lze nalézt na babylonských klínových tabulkách . [5] . Koncept důkazu neexistoval ve starověkém Řecku v VIII-VII století před naším letopočtem. E. Nicméně již v VI století před naším letopočtem. E. v Řecku se logický důkaz stává hlavní metodou stanovení pravdy. V této době vznikly první matematické teorie a matematické modely světa, které měly zcela moderní vzhled, to znamená, že byly stavěny z konečného počtu premis pomocí logických závěrů.
První důkazy používaly nejjednodušší logické konstrukce. Zejména Thales z Milétu , který dokázal, že průměr rozděluje kruh na polovinu, úhly na základně rovnoramenného trojúhelníku jsou stejné, dvě protínající se čáry svírají stejné úhly, zjevně použil ve svých důkazech metody ohýbání a překrývání obrazců. Podle řeckého filozofa Prokla (5. století n. l.) „Někdy uvažoval o problému poněkud obecně, někdy se spoléhal na jasnost . Již za Pythagora se důkaz přesouvá od konkrétních myšlenek k čistě logickým závěrům [6] . V důkazech Parmenida je použit zákon vyloučeného středu a jeho žák Zeno používá redukci k absurditě v aporiích [7] .
Je známo, že důkaz o nesouměřitelnosti strany a úhlopříčky čtverce, který je základem konceptu iracionality , s největší pravděpodobností patří Pythagorejcům , ačkoli byl poprvé uveden pouze v Elementech Euklida (X), vychází z opačného a vychází z teorie dělitelnosti čísel dvěma [8] . Je možné, že rozdíly v názorech na roli matematického důkazu byly jedním z důvodů konfliktu mezi Eudoxem (který je považován za zakladatele tradice organizování matematiky ve formě vět , ale který se neuchýlil k důkazům v princip [9] ) a Platón [10] .
Důležitým momentem na cestě k budoucí formalizaci matematických důkazů bylo vytvoření Aristotelovy logiky , ve které se pokusil systematizovat a kodifikovat všechna pravidla uvažování užívaná pro důkazy, popsal hlavní vznikající obtíže a nejasnosti. Aristoteles předpokládal, že důkazy jsou důležitou součástí vědy, a věřil, že důkaz „odhaluje podstatu věcí“ [11] . Ale aristotelská logika neměla přímý dopad na starořeckou matematiku a v důkazech nebyla věnována žádná pozornost otázkám formální logiky [12] .
S rozvojem matematiky ve středověku a spoléháním se na logiku převzatou ze scholastiky se postupně vytvářejí představy o formálním důkazu a rozvíjejí se jeho metody. Gersonides zahrnují zdůvodnění a zavedení do praxe metody matematické indukce [13] . Od 16. století existují samostatné pokusy kriticky porozumět důkazům starověkých řeckých matematiků, například Peletier , komentující Euklidovy „Prvky“, kritizuje důkaz o rovnosti trojúhelníků posunutím [14] .
V moderní době, díky úspěchu aplikace matematiky v přírodních vědách, byly matematické výroky a důkazy považovány za spolehlivé, jakmile byla podána přesná a formální definice počátečních pojmů, a matematika jako celek byla považována za model přísnost a důkazy pro všechny ostatní disciplíny. Zejména Leibniz považuje axiomy a pravidla inference za neotřesitelné a snaží se vybudovat formální systém logiky, aby „dokázal vše, co lze dokázat“ [15] . Avšak i v 18. století byl koncept důkazu stále příliš neformální a spekulativní, důkazem toho může být skutečnost, že Euler považoval za oprávněná současně následující:
a ,stejně jako:
,pochopit samozřejmě nesmyslnost těchto tvrzení, ale s ohledem na jejich "prokazatelnost" paradoxy [16] .
V 19. století se stále častěji objevují myšlenky na nutnost postulovat některá intuitivně zřejmá pravidla, která nelze formálním způsobem dokázat. Dalším impulsem k pochopení relativity důkazů v závislosti na postulovaných principech po mnoha staletích neúspěšných pokusů dokázat axiom euklidovského paralelismu bylo vytvoření neeuklidovských geometrií Lobačevského , Bolyaie , Gausse a Riemanna [17] .
Když mluvíme o formálním důkazu, v první řadě popisují formální model - soubor axiomů , zapsaných pomocí formálního jazyka a pravidla pro odvození. Formální odvození je konečná uspořádaná množina řádků napsaných ve formálním jazyce, takže každý z nich je buď axiomem nebo získaným z předchozích řádků použitím jednoho z pravidel odvození. Formálním důkazem tvrzení je formální odvození, jehož poslední řádek je daný výrok. Výrok, který má formální důkaz, se nazývá teorém a soubor všech teorémů v daném formálním modelu (uvažovaný spolu s abecedou formálního jazyka, soubory axiomů a inferenčními pravidly) se nazývá formální teorie .
Teorie se nazývá úplná , pokud je pro jakýkoli výrok nebo jeho negace prokazatelná, a konzistentní , pokud v ní nejsou žádná tvrzení, která lze dokázat společně s jejich negacemi (nebo ekvivalentně, pokud v ní existuje alespoň jedno neprokazatelné tvrzení). Většina "bohatých" matematických teorií, jak ukazuje první Gödelův teorém o neúplnosti , je buď neúplná, nebo nekonzistentní. Nejběžnějším souborem axiomů v naší době je Zermelo-Fraenkelův axiom s axiomem výběru (ačkoli někteří matematici jsou proti použití druhého). Teorie založená na tomto systému axiomů není úplná (např. hypotézu kontinua v ní nelze ani dokázat, ani vyvrátit – za předpokladu, že je tato teorie konzistentní). Navzdory širokému použití této teorie v matematice nelze její konzistenci dokázat vlastními metodami. Přesto drtivá většina matematiků věří v její konzistenci a věří, že jinak by byly rozpory objeveny už dávno.
Formálním důkazům se věnuje speciální obor matematika - teorie důkazů . Samotné formální důkazy matematika téměř nikdy nepoužívá, protože jsou pro lidské vnímání velmi složité a často zabírají mnoho místa.
V informatice se matematické důkazy používají k ověření a analýze správnosti algoritmů a programů (viz logika v informatice ) v rámci programovacích technologií založených na důkazech.
Přímý důkaz zahrnuje použití pouze přímé deduktivní inference z tvrzení, která jsou považována za pravdivá (axiomy, dříve dokázaná lemmata a teorémy), bez použití soudů s negací jakýchkoli tvrzení [18] . Například pro přímý důkaz jsou za přijatelná následující čísla (v přirozeném dedukčním zápisu :
, , ( modus ponens ).Substituce je také považována za metodu přímého důkazu: pokud je tvrzení pravdivé pro jakékoli hodnoty volných proměnných, které jsou v něm obsaženy, pak nahrazení jakýchkoli konkrétních hodnot namísto nějaké jejich podmnožiny ve všech výskytech ( zvláštní případ vzorec ) uvádí správné tvrzení v zápisu přirozeného odvození (neformální zápis, zjednodušený na jednu proměnnou):
V některých případech lze nepřímé důkazy pomocí negativního uvažování, zejména u konečných objektů, snadno zredukovat na přímé bez ztráty obecnosti, ale zdaleka tomu tak není vždy pro tvrzení o nekonečných sbírkách a s rostoucí hodnotou konstruktivních důkazů v v matematice dvacátého století se považuje za důležité najít přímé důkazy pro tvrzení, která byla považována za prokázaná, ale nepřímými metodami.
V teorii důkazů byla vyvinuta formální definice přímého důkazu [19] .
Induktivní metoda , která umožňuje přejít od konkrétních výroků k univerzálním výrokům, je nejzajímavější při aplikaci na nekonečné kolekce objektů, ale její formulace a použitelnost se výrazně liší v závislosti na rozsahu aplikace.
Nejjednodušší induktivní metodou [20] je matematická indukce , závěr týkající se přirozené řady , jehož myšlenkou je prosadit určitý zákon pro všechna přirozená čísla, založený na faktech jeho implementace pro jednotu a následující pravdě pro každé následující číslo v zápisu přirozeného závěru:
.Metodu matematické indukce lze přirozeně aplikovat na jakékoli počitatelné kolekce objektů, je považována za spolehlivou a legitimní jak v klasických, tak v intuicionistických a konstruktivních dokazovacích systémech. Metoda je axiomatizována v systému axiomů Peanovy aritmetiky .
Složitější otázkou je, zda lze induktivní metodu rozšířit na nespočetné kolekce. V rámci naivní teorie množin byla vytvořena metoda transfinitní indukce , která umožňuje rozšířit pravidlo induktivní inference pro jakékoli dobře uspořádané množiny podle schématu podobného matematické indukci. Možnost použití induktivního uvažování pro nespočetné kolekce a v intuicionistické logice , známé jako bar-indukce [21] , byla nalezena .
Existuje konstruktivní metoda strukturální indukce , která umožňuje aplikovat indukci na dobře uspořádané kolekce objektů, ale podléhající jejich rekurzivní definici .
Důkaz kontradikcí používá logickou metodu přivedení do bodu absurdity a je postaven podle následujícího schématu: aby se dokázalo tvrzení , předpokládá se, že je nepravdivé, a pak v deduktivním řetězci dojdou k například záměrně nepravdivý výrok, ze kterého se podle zákona dvojí negace vyvozuje závěr o pravdě , v přirozených inferenčních zápisech:
Bylo by mnohem lepší to napsat takto. Důkaz kontradikcí je schéma:
Formalizuje metodu důkazu kontradikcí.
V intuicionistických a konstruktivních systémech se důkaz kontradikcí nepoužívá, protože zákon dvojí negace není přijat.
Poznámka . Toto schéma je podobné jinému - schématu důkazu redukcí do absurdity . V důsledku toho jsou často zmatení. Přes některé podobnosti však mají odlišný tvar. Navíc se liší nejen formou, ale i podstatou a tato odlišnost je zásadní povahy.
Kontrapoziční důkaz používá zákon kontrapozice a spočívá v následujícím: k prokázání skutečnosti, že tvrzenínásledujeje třeba prokázat, že negacevyplývá z negace, v symbolice přirozeného závěru:
.Kontrapoziční důkaz je redukován na metodu rozporu : u důkazu se kontroluje jeho negace a protože platí premisa , je odhalen rozpor.
Jako příklad kontrapozičního důkazu [22] stanoví skutečnost, že když je liché , pak je i liché ( ), k tomu je kontrapozice dokázána, že je-li sudé, pak je také sudé.
V systémech, které neakceptují zákon dvojí negace, kontrapoziční důkaz neplatí.
Pro tvrzení, jako jsou věty o existenci , ve kterých je přítomnost nějakého objektu formulována jako výsledek, například existence čísla, které splňuje nějaké podmínky, je nejcharakterističtějším typem důkazu přímé nalezení požadovaného objektu pomocí metod odpovídající formální systém nebo použití kontextu odpovídajícího oddílu. Mnoho klasických existenčních teorémů je dokázáno kontradikcí: redukcí na absurditu předpoklad, že objekt s danými vlastnostmi neexistuje, ale takové důkazy jsou považovány za nekonstruktivní, a proto se v intuicionistické a konstruktivní matematice používají pouze důkazy konstrukcí. za taková prohlášení.
V některých případech se pro prokázání tvrzení vytřídí všechny možné varianty množiny, ve vztahu k níž je tvrzení formulováno ( úplný výčet ), nebo se všechny možné varianty rozdělí do konečného počtu tříd představujících konkrétní případy a pro každou z které se dokazování provádí samostatně [23] . Důkaz metodou vyčerpání opcí se zpravidla skládá ze dvou fází:
Počet možností může být poměrně velký, například k prokázání hypotézy čtyř barev bylo zapotřebí téměř 2 000 různých možností, než se pomocí počítače vytřídily . Objevení se takových důkazů na konci 20. století v souvislosti s rozvojem výpočetní techniky vyvolalo otázku jejich postavení v matematické vědě kvůli možným problémům s ověřitelností [24] .
Bijection proof se používá k vytvoření prohlášení o velikosti nebo struktuře sbírky nebo srovnatelnosti sbírky s jakoukoli jinou sbírkou a spočívá ve vytvoření vzájemné korespondence mezi zkoumaným souborem a souborem se známými vlastnostmi. [25] . Jinými slovy, důkaz tvrzení o určité sbírce je redukován na důkaz vytvořením bijekce , případně s dalšími omezeními, se sbírkou, pro kterou je tento výrok znám.
Nejjednodušší příklady bijektivních důkazů jsou důkazy kombinatorických tvrzení o počtu kombinací nebo počtu prvků množin, složitějšími příklady jsou ustavení izomorfismů , homeomorfismů , difeomorfismů , bimorfismů , díky nimž jsou vlastnosti již známého objektu , který jsou invariantní s ohledem na jeden nebo speciální druh bijekce.
Tradičně se konec důkazu označoval zkratkou „ QED “, z latinského výrazu lat. Quod Erat Demonstrandum („Co bylo požadováno k prokázání“). V moderních dílech se k označení konce důkazu častěji používá znak □ nebo ■, ‣, // a také ruská zkratka h.t.d.
Slovníky a encyklopedie | |
---|---|
V bibliografických katalozích |