Bizonyítási sémák speciálkollégium
1997 õsz
A speciálkollégium témája
a kombinatorika, bonyolultságelmélet és logika
határterületén lévõ problémakör.
A matematikán belül kialakult az igény a
matematikai bizonyítás definíciójára.
Az állítások és bizonyításuk formális definíció
alapján bizonyos jelsorozatok. Elvárjuk, hogy
egy tétel, illetve bizonyítás
jelsorozat ismeretében, már ne kelljen ötlet
a bizonyítás ellenõrzéshez, azaz
``egy gép is ellenõrizni
tudjá' a bizonyítást.
Egy matematikailag szabatos definíció
(amellett, hogy leírja miket tekintünk tételeknek)
tartalmaz egy algoritmust, amely egy (t,b),
``tételjelölt---bizonyításjelölt-pár''
inputot elfogad
vagy elvet.
Ezt az algoritmust korrektnek nevezzük, ha
egy t jelsorozat valóban tétel, akkor legyen olyan
b jelsorozat, amelyet az ellenõrzõ algoritmus elfogad,
illetve, ha t jelsorozat nem egy tételt ír
le, akkor tetszõleges b jelsorozatra
a bizonyítás ellenõrzõ algoritmus
vesse el (t,b)-t.
A legismertebb bizonyítási séma
a Hilbert- vagy Frege-féle séma, amelyben
a tételjelöltek
a halmazelmélet nyelvén
(vagy más nyelven) felírt
elsõrendû formulák;
a tételek a halmazelmélet axiómáinak
logikai következményei;
a bizonyításjelöltek
a halmazelmélet nyelvén felírt formulákból alkotott
véges sorozatok; és az ellenõrzõ algoritmus
azt ellenõrzi, hogy sorozatunk minden eleme
egy halmazelméleti axióma, illetve
sorozatunk elõzõ elemeibõl kikövetkeztethetõ
formula, továbbá sorozatunk utolsó eleme
a bizonyítandó állítás-e.
Gödel nevezetes teljességi tétele
azt mondja ki, hogy a fenti séma korrrekt az általunk
megkövetelt értelemben.
A klasszikus matematika eredményei
megfogalmazhatók úgy, hogy a bennük
szereplõ állítások tételek legyenek
a fenti értelemben és bizonyításaik a fenti
sémabeli bizonyítások legyenek.
A fentitõl eltérõ sok más bizonyítási séma
is létezik. Ezek az utóbbi idõkben
egyre fontosabb szerepet kapnak a bonyolultságelméletben és
kombinatorikában.
A természetesen felvetõdõ kérdések
szoros kapcsolatban állnak kódoláselmélettel,
illetve NP-teljességi kérdésekkel.
*
A speciálkollégium matematikus és programozó matematikus
hallgatók számára van meghírdetve.
Alapvetõ gráfelméleti és boznyolultságelméleti
fogalmak ismeretét feltételezzük.
Tanár szakos hallgatók számára
a speciálkollégium túl sok matematikai és bonyolultságelméleti
hivatkozást tartalmazhat. Ennek ellenére
aki merész és vállalja az esetleges plusz munkát
az profitálhat az elõadásokból
*
A speciálkollégiumon való jegyszerzés pontos feltételeit
a késõbbiekben adjuk meg.