1+1=2 – az előbbi művelet olyan egyszerű, hogy már akár óvódások is képesek elvégezni. Azonban mire utal pontosan az egyenlőségjel? Mit jelent, hogy valami egyenlő valami mással? Hagyományosan az “egyenlő” azt jelenti, hogy egy egyenlet két oldalán ugyanaz a matematikai objektum található. Ez a felfogás az ókorból ered, és végül a 16. században lett formalizálva. A 19. század végi halmazelmélet azonban már egy új szemléletet hozott: halmazokat akkor tekintünk egyenlőnek, ha ugyanazokat az elemeket tartalmazzák. A halmazelmélet egyébként amúgy is őrült egy világ – erről már korábban is írtunk:

Az angol, aki kinyírta a matematikát: Bertrand Russell Az 1800-as évek végén Gottlob Frege megpróbálta megalapozni a matematikát a szimbolikus logika segítségével. Aztán jött Bertrand Russell, és jól széttrollkodta az egészet. Elmondjuk, hogy lehet ezt könnyen megérteni.

Azonban a halmazok esetén a dolog még ennél is bonyolultabb. Ízlelgessük a szót: izomorfizmus – ez azt jelenti, hogy két halmaz akkor tekinthető egyenlőnek, ha az elemeik között egyértelmű leképezés van, még akkor is, ha maguk az elemek különböznek. Például az {1, 2, 3} és {a, b, c} halmazok egymással leképezhetők, így izomorfok.

Mindezzel sokáig nem is volt gond, hiszen a matematikai kontextusból kiderült, melyik egyenlőségre gondolunk éppen, egy elsős matek munkafüzetben például nyilván nem az izomorfizmusra. A gond akkor kezdődik, amikor már pontos definíciókra van szükség – mint például az olyan számítógépes ellenőrző-programoknál, mint a Coq, az Isabelle vagy a HOL Light.

Ezek az ellenőrző programok olyan szoftverek, amelyek a matematikai bizonyítások helyességét ellenőrzik. A szoftverek algoritmusai lépésről lépésre átvizsgálják a bizonyításokat, és ellenőrzik, hogy minden logikai lépés helyes-e. Az ilyen programok célja, hogy kiszűrjék az emberi hibákat és biztosítsák a bizonyítások pontosságát.

Mint arról most a New Scientist cikke beszámol, Kevin Buzzard, az Imperial College London munkatársa, és mások rámutattak, hogy az egyenlőség meghatározásának a fentebb leírt kétértelműsége már tehát problémát jelent a bizonyítások számítógépes formalizálása során. A jelenlegi számítógépes bizonyítási rendszerek ugyanis nehezen birkóznak meg azzal, hogy a matematikusok az egyenlőséget eléggé “árnyaltan” alkalmazzák, ami alatt elsősorban a fejlett matematikai munkákban gyakori kanonikus izomorfizmusokat kell érteni.

Mi a megoldás? Laikusként is logikusnak tűnhet, hogy két opció jön szóba: vagy a matematikát kell átalakítani vagy a számítógépes rendszereket. A szakemberek egyik csoportja az előbbi lehetőséget támogatja – eszerint alapjaiban kell megváltoztatni a matematika definícióit, aminek célja, hogy azonosnak tekintsük a kanonikus izomorfizmust és az egyenlőséget. Ezzel ugyanis leegyszerűsítenénk a számítógépes bizonyítási rendszerek munkáját. Ezt a lehetőséget a homotópia típuselméletben vizsgálják, ahol a hagyományos egyenlőség és a kanonikus izomorfizmus tehát ugyanazt jelenti.

Buzzard és mások azonban a meglévő axiómák átdolgozása ellen érvelnek, és inkább a jelenlegi számítógépes bizonyítási rendszerek fejlesztését javasolják, hogy azok jobban kezeljék a matematikai egyenlőség fentebb röviden vázolt, komplex kérdéskörét. Szerintük ugyanis praktikusabb megoldás a jelenlegi matematikai alapok fenntartása mellett a számítási eszközök fejlesztése.

(Kép: Pixabay/Mohamed_hassan)