Egy matematikai bizonyítás a matematika tudományában érvényesnek vagy igaznak tartott kijelentések érvényességének demonstrálásának, igazolásának módja. Elvileg pusztán abban különbözik a többi tudomány igazolási módszerétől, hogy matematikai természetű kijelentésekre használják. Gyakorlatilag azonban sokkal szigorúbban és következetesebben alkalmazza azt a módszert, melyet Descartes fejtett ki először az Értekezések a módszerről című könyvében, és melyet a tudományos kutatás gyakorlatával szemben támaszt követendő eljárásként.

A matematikában az igaz kijelentések igaz volta kizárólag gondolati úton, matematikai bizonyítással fedhető fel. A matematikai bizonyítással igaznak minősített kijelentéseket matematikai tételeknek nevezik.

A matematikai bizonyítás fogalma

Egy matematikai bizonyítás, vagy annak részletei lényegében abból állnak, hogy igaznak elfogadott kijelentéseket alapul véve kimondják egy másik kijelentés igaz voltát is. Az igazság átöröklésének ezen mozzanatait levezetési lépéseknek nevezik, melyeknek létjogosultsága a levezetési szabályok sokaságában rögzített feltételek alapján minősíthető helyesnek. Tekintsük példaként a következő állítást:

A kijelentés igazságát a következő gondolatmenettel igazolhatjuk.

Bizonyítás. Kiindulunk a 64 < 81 kétségbevonhatatlan matematikai igazságból (legalul) és kimutatjuk, hogy az állítás igaz. Közben – ezek a jelű közbevetések – már igazoltnak tekinthető matematikai tételekre hivatkozunk. Például a legalsó mozzanatnál felhasználjuk, hogy tetszőleges pozitív számra . Ha tehát , akkor teljesül . Itt tehát egy általános igazság speciális esetével állunk szemben. A pozitív -ekre értelmezett 12. gyök azonossága miatt A pozitív számok halmazán értelmezett függvény szigorú monotonitása miatt, azaz ha , akkor A hatványozás azonossága, továbbá a szorzás kommutativitása miattA 4. és 3. gyök definíciója miatt: és pozitív -re. Tehát igaz állításból (64 < 81 és a felhasznált műveleti szabályok) igaz következtetésekkel eljutottunk a kívánt állításig. ■

Egy matematikai bizonyítás végét általában a ■ szimbólummal jelölik.

A legalsó sorból a következőre tehát így jutottunk el: ha és és , akkor , de és , tehát . Vagyis adott egy „ha A, akkor B” alakú általános érvényű szabály. Tudjuk, hogy jelen esetben A, azaz a feltétel igaz, ez alapján tehát kijelenthetjük, hogy B, azaz a konklúzió is igaz. Az ilyen alakú gondolatmenetek láncolatát nevezzük (logikai) bizonyításnak.

Meg kell jegyeznünk, hogy az előbbi bizonyításban ugyan az igazság „felfelé áramlik” (az alsó állításról az eggyel fentebbire öröklődik az igaz minősítés), de az ötlet, a gondolat „lefelé halad”. A fő kérdés, hogy mi biztosítaná az állítás igazságát. Erre a kérdésre keresünk választ, és az első gondolat, hogy emeljük a 4 és 3 legkisebb közös többszöröse azaz 12-nek hatványára az egyenlőtlenséget, ezzel biztosítva, hogy összehasonlítható legyen a két szám. Ha ez utóbbi igaz lenne, akkor az állítás is. A bizonyítások kiötlésével, pszichológiájával foglalkozó témakör az úgy nevezett heurisztika, melynek fontosságára többek közt Pólya György hívta fel a figyelmet.

Formális és informális bizonyítás

Az, hogy miből származik a tételek igazsága – jobban mondva bizonyítottsága, bizonyíthatósága – azt a matematikusok közösségének döntő többsége, Frege és Hilbert bizonyításelméleti kutatásaira alapozva a következőképpen látja: Az A kijelentés bizonyítása lényegében nem más, mint állítások egy olyan véges (A1,A2, A3, …,An) sorozata, melyeknek utolsó eleme az A kijelentés és melynek tetszőleges B eleme vagy matematikai axióma vagy olyan kijelentés, ami előtt a sorozatban szerepel egy ' ha C, akkor B ' alakú kijelentés C-vel együtt. Eszerint a levezetések úgy származtatják át az axiómákról a tételre az érvényességet, hogy csupa olyan ' ha …, akkor … ' lépésekből álló láncokból állnak, ahol az legelső mondat axióma, az utolsó mondat pedig maga a tétel. A levezetések megalkotását a levezetési szabályok és módszerek, például az esetszétválasztás szabálya vagy az indirekt bizonyítás elve segítik.

Ez utóbbi, a legszélesebb körben elfogadott nézetet nevezik formalista álláspontnak. Kétségkívül eredményezi a tételek érvényességét, és jól körülhatárolt fogalmai révén vizsgálhatóvá, kutathatóvá teszi a bizonyítások témakörét. A matematikai logikában ennek az eljárásnak a formális megfogalmazásaként definiálják a formális rendszerbeli levezetést.

Kritikák

Ezzel szemben például Kalmár László – aki maga is a matematikai logika kiemelkedő tudósa volt – felhívja a figyelmet a formalista szemlélet hiányosságaira. A tételek igazolásához hozzátartozik az, hogy az alkalmazásaikban működjenek, használhatóak legyenek.

Brouwer és követői az intuicionisták arra mutatnak rá, hogy a matematikai tételek bizonyítása emberi tevékenység. Nem elég elvi úton igazolni, hogy létezik egy, a fenti értelemben vett bizonyításnak nevezett véges formulasorozat. Egy bizonyítás csak akkor érvényes, ha ezt a formulasorozatot már valaki végiggondolta – szemben például Gödel teljességi tételével, melyben csak a bizonyíthatóságok vannak igazolva, de nem a bizonyítottságok. A matematikai tételek csak akkor érvényesek, ha bizonyításaik közvetlen kapcsolatban vannak a matematika alapintuíciójával, a természetes számokkal.

Szociálkonstruktivizmus

Lakatos Imre sokkal messzebbre megy állásfoglalásában. Szerinte egy matematikai bizonyítás elvégzése esetén a fent vázolt formális eljárás kivitelezése csak a feladat töredéke. Egy tételt bizonyítani sokkal több, mint a levezetését megalkotni, éspedig bizonyítani annyit tesz, mint olyan matematikai fogalomtárat és levezetési eszközrendszert kialakítani, mely a tétel – formalista értelemben vett – levezethetőségének elégséges (és lehetőleg szükséges) feltételeit biztosítja. A matematikai tevékenységben a kihívást nem pusztán a levezetések megtalálása jelenti, hanem olyan elmélet megalkotása, mely egyszerre biztosítja az addig elfogadott tételek és a bizonyítani kívánt igaz tétel – formalista értelemben vett – levezethetőségét. Lakatos álláspontjának igazolását a Gödel-tételekben látja. A tételek metodológiai következménye, hogy semmilyen releváns matematikai elméletet nem lehet egyetlen formális rendszer keretében leírni, mert mindig megfogalmazhatók lesznek benne olyan állítások, melyeknek igaz vagy hamis voltáról levezetéssel vagy cáfolással nem leszünk képes meggyőződni.

Történeti áttekintés

Lásd még: A logika története, A matematikafilozófia története.

Egy állítás melletti érvelés elfogadott menetét és az alkalmazható technikákat a Szókratész korabeli görög filozófusok alakították ki. A matematikai állítások melletti érvelés mai napig elfogadott formáit Arisztotelész Organonjában és Eukleidész Elemek című művében, illetve néhol Platón műveiben találhatjuk meg elsőként. Ezekben a művekben elvi, a logikai érvelésben elkövetett hibát nem találhatunk, annál inkább találunk azonban hézagokat, hiányzó láncszemeket a bizonyításokban. A XIX. század nagy matematikusai és logikusai (Cauchy, Weierstrass, Abel, Bolzano, Frege) mutattak rá arra, hogy nem elegendő a bizonyítást hihetőnek, elfogadhatónak ítélni, alaposan elemzés alá kell vetni a bizonyítás lépéseit magukat is. Ekkor alakult ki a szigorú bizonyításelemzés eljárása, mely a matematika tudománymetodológiájának legjellegzetesebb sajátossága.

Bizonyítási módszerek

Bár a levezetés fenti definíciója egyfajta egyenes út szemléletes képét mutatja, mely az axiómáktól a tételig vezet, valójában egy A állítás levezetésénél az egyedi lépésekben nagyon sok addigi tételt felhasználnak. Itt inkább arra kell gondolni, hogy egy adott matematikai elmélet (például az euklideszi geometria vagy a számelmélet) összes tételként ismert állításának következménye A. Ezt így jelöljük: vagy Nem kell azonban a bizonyításokat ténylegesen az axiómákig visszavezetni, valójában ez lehetetlen is lenne. Ehelyett elegendő megmutatni, hogy ha valamely A kijelentés levezethető, akkor milyen lépésekkel kell kiegészíteni a levezetését ahhoz, hogy a B kijelentés is levezethető legyen. Azt, hogy az A állítás levezethetőségéből következik a B állítás levezethetősége (tehát a levezetési lépést) a következőképpen jelöljük:

A matematikai állítások (legalapvetőbb, de már értelmes) logikai szerkezete a következő lehet:

| diszjunkció (alternáció) | | ' A vagy B ' |- | konjunkció | | ' A és B ' |- | implikáció (kondicionális) | |' ha A, akkor B ' |- | negáció | |' nem A ' |- | univerzális kvantifikáció | |' minden x-re A ' |- | egzisztenciális kvantifikáció | |' van olyan x, ami A ' |- | egyenlőség (azonosság) | |' t egyenlő (azonos) s-sel ' |} Ezeken kívül a matematika nagyon sok nemlogikai, „szakmai” kifejezést is tartalmaz, például a részhalmaz (⊆), eleme (∈), oszthatóság (.|.), ... szimbólumokat. Ezekkel is lehet mondatokat képezni, melyek értelmét vagy ezek definíciója, vagy a rájuk vonatkozó axiómák adják meg.

Az alábbiakban összefoglaljuk, hogy milyen elvezetési szabályok biztosítják ezeknek az állításoknak a helyességét.

A bizonyításokat vizsgálva egyfajta kettősségre bukkanhatunk. Az egyik típus, amikor lépésről lépésre előrehaladva építjük föl az A bizonyításából a B bizonyítását, vigyázva természetesen arra, hogy a levezetési lépéseket jól végezzük és az igazság öröklődjön az egyik lépésről a másikra. Ezt nevezik direkt bizonyításnak. A másik típus az amikor egy állítás ellenkezőjének lehetetlenségét demonstráljuk – amúgy szintén aprólékos levezetési lépésenként. Ez az indirekt bizonyítás. A kettősség megjelenése a ókori görög deduktív matematika kialakulása idejére tehető, amikor két eltérő igazolási mód vetélkedett egymással, a konstruktív bizonyítás (a thalészi kongruenciabizonyítás) és a Parmenidész által egyedüli igazolási módnak tartott, a lehetetlenre történő visszavezetést alkalmazó érvelés (reductio ad absurdum).

Direkt bizonyítás Pozitív egy kijelentés, ha nincs benne tagadás (¬). Ezek levezetése alkotja a direkt bizonyítások mintapéldányait. Az alábbi szabályok együttesét a lentebb említendő, hozzájuk tartozó kiküszöbölési szabályokkal együtt pozitív logikának nevezzük.

{|class="wikitable" ! Állítás ! Az állítás feltétele ! Megjegyzés |- align="center" | A ∧ B | | A ∧ B levezethető, ha A is és B is levezethető |- align="center" | A ⇒ B | | A ⇒ B levezethető, ha axiómának tekintve A-t (tehát feltéve A-t) ebből levezethető B (dedukciótétel) |- align="center" | (∀x)A | | (∀x)A levezethető, ha az A(x) nyitott kifejezés levezethető (univerzális generalizáció) |- align="center" | A ∨ B | | A ∨ B levezethető, ha vagy A, vagy B levezethető |- align="center" | (∃x)A | | (∃x)A levezethető, ha az A(x) nyitott kifejezésben az x helyére valamely t dolgot helyettesítve az A(t) kijelentés levezethető

Ezeket a szabályokat a logikai jelek bevezetési szabályának nevezik, erre utal a (jel be) jelölés.

Dedukciótétel Az egyik legtipikusabb direkt bizonyítási lépés a dedukciótétel, mely az informális levezetések során a következőképpen jelenik meg. Egy ' ha A, akkor B ' feltételes állítást akarunk bizonyítani. Ekkor azt mondjuk, hogy „tegyük fel, hogy A igaz” ezzel azt jelezzük, hogy az A állítást úgy fogjuk tekinteni, mintha igaz jobban mondva axióma lenne. A formális elméletben ez azt jelenti, hogy áttérünk a elméletről az A-val, mint axiómával bővített elméletre. Ebben bebizonyítjuk a B kijelentést, tehát belátjuk, hogy . Majd a bizonyítást ezzel zárjuk: „tehát feltéve A-t, teljesül B, vagyis ha A, akkor B”. Ezzel jelezzük, hogy a dedukciótételt alkalmazzuk és levezettük ' ha A, akkor B '-t.

Reductio ad absurdum

A ¬ A kijelentés levezethetőségének feltételét a reductio ad absurdum vagyis a lehetetlenre való visszavezetés szabálya adja meg. Ez az indirekt bizonyítások központi lépése. Alkalmazásánál felhasználjuk az ellentmondásos elmélet illetve az ellentmondás fogalmát. Ellentmondásosnak nevezünk egy T elméletet, ha létezik olyan C kijelentés, hogy a C ∧ ¬C (C és nem C) állítás levezethető T-ben, azaz ha

{|class="wikitable"