Pénzes István (szerk.): Műszaki nagyjaink 6. Matematikusok, az oktatás, a gépészet és a villamos vontatás alkotói, kiváló lisztvegyészek (Budapest, 1986)
Dr. Ádám András - Dr. Dömösi Pál: Kalmár László
eldöntse, érvényes-e az a formula, vagy érvénytelen.15 Az ilyen általános módszer keresésének kérdését eldöntésproblémának nevezik a matematikai logika művelői. Jelöljük az értelmes formulák összességét F-íe\. Az eldöntésproblémával foglalkozó kutatásoknak két fő iránya van: (1) Találjunk E-ben minél bővebb G formula-osztályokat úgy, hogy egységes eljárásunk van a G-be tartozó formulák érvényes vagy érvénytelen voltának meghatározására. (2) Találjunk F-ben minél szűkebb H formula-osztályokat úgy, hogy egységes eljárásunk van, amely minden E-beli / formulához egy i/-beli h formulát rendel, és teljesül az az állítás, hogy / pontosan akkor érvényes, ha érvényes h is. Az eldöntésprobléma teljes megoldását az jelentené, ha találni sikerülne olyan G, H formula-osztályokat (a fenti tulajdonságokkal), hogy G~DH lenne igaz rájuk.16 Azonban — amint Church a harmincas évek közepén bebizonyította —- ez (általánosan rekurzív eszközökkel) elvileg elérhetetlen. Kalmár egyszerűsített bizonyítást adott [51], [54] az eldöntésprobléma teljes megoldásának lehetetlenségére (6. ábra). Ez a tény természetesen egyáltalán nem vonja maga után azt, hogy az (1), (2) kutatási irányok művelése ne volna értékes; maga Kalmár László — és vele együttműködve Burányi János — számos dolgozatban járult hozzá a (2) irányban folyó kutatásokhoz. Az ebben az irányban elért eredményekről Surányi könyvben is áttekintést adott [C. 11]17 Kalmárnak a matematikai logikai vizsgálatai nem merültek ki a fentebb vázolt témák körébe vágó munkáival. Jónéhánv további, logikai tárgyú dolgozata közül most röviden utalunk néhányra. A [12] közleményben az állításkalkulus axiomatizálhatóságának adja egyszerű tárgyalását (annak a ténynek, hogy megadható véges sok axióma és véges sok következtetési szabály úgy, hogy ezek alkalmazásával éppen az állításkalkulus azonosan igaz formulái nyerhetőek). A [42] munkában egy, a logika és az algebra határán álló tételre nyer új bizonyítást: arra, hogy az asszociatív rendszerek szó-problémájára nem létezik 15 Itt tehát már túlléptünk azon, hogy egyetlen lerögzített axiómarendszerrel dolgozzunk. Csupán az értelmes formulák felépítésére vonatkozó logikai elvek és az érvényesség igazolására szolgáló következtetési szabályok szolgálnak alapfeltevésekül. — Szakszerűbben szólva, „értelmes” formula helyett a „jólképzett” formula precízen körülhatárolt fogalmát szokás tekinteni; egy formula „érvényes” vagy „érvénytelen” volta helyett pedig azt szokás vizsgálni, hogy vajon „van olyan modell, amelyben a formula teljesül”, ületve „a formula nem teljesül az elképzelhető modellek egyikében sem”. 16 Ha az (1), (2) főirányok összetalálkoznának (ha GOH elérhető volna), ez bizonyos értelemben sterillé tenné a matematikát. Az eldöntésprobléma ezen teljes megoldása azt jelentené, hogy gépies módszer áll rendelkezésünkre, amely (elvben) újabb ötletek nélkül, mechanikusan képes eldönteni bármely formula igaz vagy hamis voltát, vagyis amely bármely értelmes matematikai sejtésre, ami csak felmerül, mechanikus eljárással tud választ adni. 17 Az (1) kutatási irányról Wilhelm Ackermann írt könyvet [C.l] A hetvenes évek végén újabb összefoglaló munkák is megjelentek az elmélet korszerű állásáról. 5 5 Műszaki nagyjaink VI. 65