Probléma: a matematikusok szerint nem egyértelmű, mit jelent az “egyenlőségjel”

2024 / 06 / 06 / Felkai Ádám
Probléma: a matematikusok szerint nem egyértelmű, mit jelent az “egyenlőségjel”
Az “egyenlőségnek” a matematikusok számára több definíciója is létezik, ami sokáig nem okozott problémát, de a számítógépes bizonyításellenőrzés során már gondot jelent. Ennek megoldása a matematika alapjainak az újragondolását is igényelheti.

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)


A Marketplace sem mentes a csalóktól - a megoldás az adásvételi szerződés
A Marketplace sem mentes a csalóktól - a megoldás az adásvételi szerződés
Az internetes kereskedelem széles termékpalettájával és az egyre kedvezőbb ajánlatok térnyerésével egyre csak nő az online vásárlások száma. Ezzel párhuzamosan a vásárlásokat érintő csalások és visszaélések száma is egyre gyakoribbnak bizonyul. A megoldás a megfelelő körültekintés és a tájékozódás. Nagyban növeli a vásárlás biztonságát a piactereken az adásvételi szerződés készítése, amelyet a Szerzivel ma már könnyen és egyszerűen elkészíthet otthonról.
Az állat, amit Darwin a legjobban gyűlölt és ami nélkül nem született volna meg A fajok eredete
Az állat, amit Darwin a legjobban gyűlölt és ami nélkül nem született volna meg A fajok eredete
Charles Darwin az HMS Beagle-en tett útjáról érdekes elgondolásokkal tért vissza Angliába, de a természetes szelekcióról szóló elméletének kidolgozásához szüksége volt egy kezdő lökésre, amit a mindössze néhány milliméteres Mr. Arthrobalanus adott meg neki.
Ezek is érdekelhetnek
HELLO, EZ ITT A
RAKÉTA
Kövess minket a Facebookon!
A jövő legizgalmasabb cikkeit találod nálunk!
Hírlevél feliratkozás

Ne maradj le a jövőről! Iratkozz fel a hírlevelünkre, és minden héten elküldjük neked a legfrissebb és legérdekesebb híreket a technológia és a tudomány világából.



This site is protected by reCAPTCHA and the Google Privacy Policy and Terms of Service apply.