Bizonyítási elmélet
A bizonyítási elmélet a matematikai logika egy része , amely a bizonyításokat formális matematikai objektumok formájában mutatja be, matematikai módszerekkel elemezve azokat. A bizonyításokat általában induktív módon definiált adatszerkezetekként mutatják be , mint például listák és fák, amelyeket a formális rendszerek axiómái és következtetési szabályai szerint hoznak létre. Így a bizonyítási elmélet szintaktikai , szemben a szemantikai modellelmélettel . A modellelmélettel , az axiomatikus halmazelmélettel és a számításelmélettel együtt a bizonyításelmélet a matematika egyik úgynevezett „négy pillére” [1] . A bizonyítási elmélet a bizonyítás fogalmának pontos meghatározását használja annak bizonyítására, hogy egy adott állítás bizonyítása egy adott matematikai elméleten belül lehetetlen. [2]
A bizonyítási elmélet fontos a filozófiai logika számára , ahol a bizonyításelméleti szemantika gondolata önálló érdeklődésre tart számot, amely elképzelés a strukturális bizonyítási elmélet formális logikai módszereinek megvalósíthatóságán alapul.
Történelem
Bár a logika formalizálását jelentősen előremozdították olyan szerzők, mint H. Frege , J. Peano , B. Russell és R. Dedekind munkái , a modern bizonyítási elmélet történetét általában úgy tekintik, mint amely D. Hilberttel kezdődött , aki elindította az úgynevezett Hilbert-programot a matematika alapjaira. Kurt Gödel eredeti bizonyítási elméleti munkája előbb továbbfejlesztette, majd megcáfolta ezt a programot: teljességi tétele kezdetben jó előjelnek tűnt Hilbert azon céljához, hogy az egész matematikát véges formális rendszerként mutassa be; a befejezetlenségi tételei azonban azt mutatták, hogy ez a cél elérhetetlen. Mindezt a munkát Hilbert-rendszereknek nevezett bizonyítási számításokkal végezték .
Ezzel párhuzamosan a szerkezeti bizonyítási elmélet alapjait is kidolgozták . Jan Lukasiewicz 1926-ban felvetette, hogy a Hilbert-féle rendszereket a logika axiomatikus ábrázolásának alapjául lehetne javítani, ha a feltételezésekből levont következtetéseket következtetési szabályokkal változtatják. Ennek az ötletnek a kidolgozása során S. Yankovsky (1929) és G. Gentzen (1934) egymástól függetlenül létrehoztak egy természetes dedukciós kalkulusnak (természetes következtetésnek) nevezett rendszereket, kombinálva azokat Gentzen megközelítésével, amely bevezeti a szimmetria gondolatát az állításokra vonatkozó feltételezések között. a bevezetés szabályai, valamint a propozíciók törlési szabályokban való elfogadásának következményei, amely gondolat a bizonyítási elméletben nagyon fontosnak bizonyult. Gentzen (1934) tovább vezette az úgynevezett szekvenciális kalkulusokat , amelyek jobban kifejezik a logikai konnektívumok kettősségét, és alapvetően hozzájárultak az intuicionista logika formalizálásához; ő szolgáltatta a Peano aritmetika következetességének első kombinatorikus bizonyítékát is. A természetes dedukció és a szekvenciális számítás fejlődése bevezette az analitikus bizonyítás alapgondolatát a bizonyítási elméletbe.
Formális és informális bizonyítás
A mindennapi matematikai gyakorlat informális bizonyítása nem olyan, mint a bizonyítási elmélet formális bizonyítása. Inkább olyanok, mint a magas szintű vázlatok, amelyek lehetővé teszik a szakértő számára, hogy kellő idő és türelemmel legalább elvileg rekonstruálja a formai bizonyítékot. A legtöbb matematikus számára a teljesen formális bizonyítási eljárás túl pedáns és bőbeszédű ahhoz, hogy gyakran használják.
A formális bizonyítások számítógép segítségével, interaktív tételbizonyító rendszerben készülnek. Lényeges, hogy ezek a bizonyítások automatikusan is ellenőrizhetők legyenek. A formális bizonyítások ellenőrzése általában egyszerű, míg a bizonyítások keresése (automatikus tételbizonyítás) általában nehéz. Egy matematikai kiadványban szereplő informális bizonyítás azonban hetekig tartó gondos elemzést és ellenőrzést igényel, és még mindig tartalmazhat hibákat.
Bizonyítási számítások típusai
A bizonyítási számítások három leghíresebb típusa:
- Hilbert-számítás
- Természetes levonási számítások
- Sorozatszámítás
Mindegyikük teljes axiomatikus formalizálást adhat a klasszikus vagy intuicionista megközelítés propozíciós vagy predikátumlogikájának, szinte bármilyen modális logikának és számos szubstrukturális logikának, például releváns vagy lineáris logikának. Valójában meglehetősen nehéz olyan logikát találni, amelyet ne lehetne ábrázolni az egyik ilyen számításban.
Konzisztenciabizonyítások
Mint már említettük, a formális elméletekben a bizonyítások matematikai tanulmányozásának lendületét Hilbert programja adta. A program központi gondolata az volt, hogy ha véges (véges) bizonyítást tudunk adni a matematikusok számára szükséges összes egzakt formális elmélet konzisztenciájára, akkor ezeket az elméleteket egy metamatematikai érvvel igazolhatjuk, amely megmutatja, hogy minden univerzális (általánosan érvényes) az állítások (szakmailag bizonyítható mondataik) végesen igazak; így ha egyszer indokolt, többé nem törődünk egzisztenciális tételeik nem véges implikációival, és az ideális entitások létezésének ál-értelmű konvencióinak tekintjük őket.
A program kudarcát K. Gödel befejezetlenségi tételei okozták, amelyek megmutatták, hogy néhány elmélet, amely elég erős ahhoz, hogy egyszerű aritmetikai igazságokat fejezzen ki, nem tudja bizonyítani saját következetességét. Azóta sok kutatás történt ebben a témában, és olyan eredmények születtek, amelyek különösen a következőket adják: a konzisztencia követelményének gyengülése; a gödel-i eredmény magjának axiomatizálása a modális nyelv, bizonyíthatósági logika szempontjából; elméletek transzfinit iterációja A. Turing és S. Feferman szerint ; az önellenőrző elméletek közelmúltbeli felfedezése – olyan rendszerek, amelyek elég erősek az önérvényesítéshez, de túl gyengék a diagonális érvvel szemben , amely Gödel kulcsfontosságú érve a bizonyíthatatlanság mellett.
Strukturális bizonyítékok elmélete
A strukturális bizonyítási elmélet a bizonyítási elmélet azon ága, amely azokat a bizonyítási számításokat vizsgálja, amelyek alátámasztják az analitikus bizonyítás fogalmát . Az analitikus bizonyítás fogalmát Gentzen vezette be a szekvenciák kiszámításához. Természetes dedukciós számítása is alátámasztja az analitikus bizonyítás fogalmát. Azt mondjuk, hogy az analitikus bizonyítások normál formák, amelyek a normálforma fogalmához kapcsolódnak a terminus átíró rendszerekben. Az egzotikusabb bizonyítási számítások, mint például I. Giro bizonyítási hálózatai is támogatják az analitikus bizonyítás fogalmát.
A strukturális bizonyítási elmélet a Curry-Howard megfeleltetésen keresztül kapcsolódik a típuselmélethez , amely a természetes dedukciós kalkulus normalizálási folyamata és a tipizált lambda -számítás béta-redukciója közötti szerkezeti analógián alapul . Ez a megfeleltetés adja az M.-Lef által kidolgozott intuicionista típuselmélet alapját, és gyakran kiterjesztik a háromoldalú megfeleltetésre is, amelynek harmadik támasza a karteziánus zárt kategóriák.
Bizonyításelméleti szemantika
A nyelvészet, a logikai típusú nyelvtan, a kategorikus nyelvtan és a Montagu-nyelvtan a strukturális bizonyítási elméleten alapuló formalizmust használja, hogy formális szemantikát adjon a természetes nyelvnek.
Táblázatrendszerek
Az analitikus táblázatok az analitikus bizonyítás központi gondolatát használják a strukturális bizonyítási elméletből, hogy megoldási eljárásokat biztosítsanak a logikák széles skálájához.
Ordinális elemzés
Számos kellően kifejező formális elmélet társítható a rájuk jellemző sorszámmal, amelyet az elmélet bizonyítási-elméleti sorszámaként ismerünk . Az ordinális elemzés olyan terület, amelynek tárgya az elméletek bizonyítási-elméleti ordinálisainak számítása.
G. Gentzen kiszámította az elsőrendű Peano aritmetika ordinálisát - megállapította, hogy a konzisztencia az ordinális transzfinit indukciójával igazolható . További vizsgálatok kimutatták, hogy a transzfinit indukció elve bizonyítja a nál kisebb ordinálisokat, de magára az ordinálisra nem , és hogy azok a kiszámítható függvények, amelyeknek mindenhol - határozottsága -ben igazolható , egybeesnek -rekurzív függvényekkel. Bár általános esetben más elméleteknél az eredmények analógjainak nem kell egyidejűleg végbemenniük ugyanarra a sorszámra, a természetes, kellően erős elméletek esetében általában ezeknek az eredményeknek analógjai nem adnak különböző sorszámokat ugyanarra az elméletre. (valamint a bizonyítási-elméleti sorszám meghatározásának egyéb megközelítései).
Bizonyításelméleti ordinálisokat számoltak a Kripke-Platek halmazelmélet számos másodrendű aritmetikai töredékére és kiterjesztésére. A teljes másodrendű aritmetika és az erősebb elméletek, különösen a Zermelo-Fraenkel halmazelmélet bizonyítási-elméleti ordinálisának kiszámításának kérdése továbbra is nyitott marad.
A bizonyítási logika (szubstrukturális logika) elemzése
Számos fontos logika származik a strukturális bizonyítási elméletben felmerülő logikai struktúra figyelembevételéből.
Lásd még
- Modellelmélet
- Bizonyíték (igaz)
- Bizonyítási módszerek
- Köztes logikák
Linkek
- Hao Wang (1981) Népszerű előadások a matematikai logikáról. ISBN 0-442-23109-1 .
- D. Barwise (szerk., 1978). Matematikai logika kézikönyve, vols. tizennégy.
- G. Takeuchi. A bizonyítékok elmélete. M., Mir, 1978
- A. Troelstra (1996). Alapvető bizonyítási elmélet. Sorozatban: Cambridge Treatises on Theoretical Computer Science, University of Cambridge, ISBN 0-521-77911-1 .
- D. von Plateau (2008). Bizonyításelmélet fejlesztése. Stanford Filozófiai Enciklopédia.
Jegyzetek
- ↑ Pl. Wang (1981), pp. 3-4, és Barwise (1978).
- ↑ Bizonyításelmélet, 1978 , p. 5.
Irodalom
- Takeuchi G. Bizonyításelmélet. - M . : Mir, 1978. - 412 p.
 Szótárak és enciklopédiák | ||||
|---|---|---|---|---|
| ||||
| Logikák | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Filozófia • Szemantika • Szintaxis • Történelem | |||||||||
| Logikai csoportok |
| ||||||||
| Alkatrészek |
| ||||||||
| Logikai szimbólumok listája | |||||||||