Bizonyításelmélet és Gödel-tételkör

Minden BME-s hallgató számára (és persze minden BME-n kívüli érdeklődőnek is).

BMETE915042, Hivatalos cím: "Gödel tételkör, bizonyításelmélet"

Stream időpontja: hétfő 16:15-17:45, helye: https://www.twitch.tv/mozow, youtube linkek: .
M$ Teams csoport: .

Kredit: 3

Mi az a Gödel-tétel? Gödel első nemteljességi tétele -- a bizonyítás alapötletét tekintve -- a ,,hazug'' ősi paradoxonának (,,Ez a mondat hamis.'') megjelenése a matematika alapvető fontosságú rendszereiben. Azt mondja ki, hogy minden ellentmondásmentes, az elemi számelméletet tartalmazó, az emberi elme által áttekinthető axiómatikus rendszerben meg lehet fogalmazni olyan eldöntendő kérdést, melyet a rendszer nem tud eldönteni (abban az értelemben, hogy nem levezethető és nem cáfolható az igenlő válasz).

Miről szól a kurzus? A kurzus lényegében egy történetet mesél el arról, ami az 1900-as évek elejétől kb. harminc éven át zajlott abban az időszakban, amit a matematikatörténet a matematika megalapozási válságának nevez. A kurzus végén kimondjuk és bizonyítjuk a tételt, de emellett megpróbáljuk összegyűjteni a legfontosabb logikai, matematikafilozófiai és számításelméleti vonatkozásait és a megalapozási válságra kifejtett hatását. A naiv halmazelmélet ellentmondásai megteremtették az igényt ellentmondásmentes matematika felépítésére. Erre három válasz született: a hilberti formalista felfogás (a matematika szimbólumjáték), a brouweri intuicionizmus (a matematika a természetes számokból kiindulva, az emberi elme által végiggondolható módon felépíthető gondolatvilág) és Russell logicizmusa (a matematikai fogalmak logikai fogalmak). A kurzus során betekintést nyerünk mindhárom ideológiába és azokba a technikákba és problémákba, amiket ezek a kezdeményezések érintettek. Megismerkedünk a Hilbert-programmal, ami a matematika ellentmondásmentességét próbálta elérni, és amelynek eredményessége Gödel második nemteljességi tétele alapján erősen kétségessé vált. Példákon megnézzük, hogy Bertrand Russell logikafilozófiai gondolatai milyen lökéseket adtak a XX. századi analitikus nyelvfilozófiának. Illetve betekintünk abba, hogy a bizonyításelmélet stratégiái különösképpen Gerhard Gentzen természetes levezetési rendszereinek alapgondolata hogyan vált kiindulási alappá a nyelvfilozófia használatelméleti megközelítésére számára (a szavak jelentése használatukban rejlik).

2017-es jegyzet: (pdf)

2019-es jegyzet: (pdf)

Tematika

1. Nem-formális levezetés Bevezető, miről szól a tárgy?, szintaxis, szemantika, pragmatika, Hilbert-féle és természetes levezetés egy-egy példán, természetes levezetés
2. A levezethetőség szintaktikája. A lambda-kalkulus nyelve. Hogyan kódolja a matematikai logika a levezetéseket? Mit gondol bele ebbe a szintaxisba? (A lambda-kalkulus függvényes, nyelvészeti, bizonyításelméleti jelentése.)
3. Szabad és kötött változók, típusok, az implikacionális logika. A kötött változók szerepe, kifejezések típusba sorolása.
4. Implikacionális töredék és normalizáció. Normalizációs tétel, ágtétel, részformulatétel.
5. Ellentmondásmentesség és a matematikafilozófiai nyelvhasználat-elmélet. Ellentmondásmentesség, metatételek.
6. Nem-klasszikus logikák szemantikái. Intuicionista és kvantumlogika. Lineáris, topológiai és Boole-algabrai modellek.
7. Omega-tulajdonságok. Aritmetikák, a matematika megalapozásának Hilbert-féle programja, abszolút ellentmondásmentesség, omega-teljesség és omega-konzisztencia.
8. Primitív rekurzív függvények, finit matematika, felsorolhatóság, eldönthetőség.
9. Típuselméleti aritmetika. A Principia Mathematica szimbolizmusa. Gödel-számozás.
10. Gödel első nemteljességi tételének bizonyítása az 1930-as cikk alapján.[16][10][11]
11. Absztrakt Gödel-tételkör. Instabil önreferenciális rendszerek, a matematika megalapozhatatlansága.
12. Absztrakt Gödel-tételkör. Diofantikus egyenletek és Gödel-tételek.
(Legalább két hétfő elmarad.)

Irodalom, amit érinthetünk:

[1] Ruzsa Imre--Máté András, Bevezetés a modern logikába, Osiris, 1997. (1.3. fej.)
[2] Alfred Tarski, J. H. Woodger Logic, Semantics, Metamathematics. Papers from 1923 to 1938, 1956 [3] Prawitz, Dag, Natural Deduction -- A Proof-Theoretical Study, Stockholm, Almqvist & Wicksell, 1965. (Ch.: I-III)
[4] Dummett, Michael, A metafizika logikai alapjai, Osiris, 2000. (8. fej.)
[5] Saul Kripke, Megnevezés és szükségszerűség, szerk. és utószó Zvolenszky Zsófia, ford. Bárány Tibor. Akadémiai, Bp., 2007.
[6] Whitehead and Russell, Incomplete symbols: Descriptions, in: From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, ed.: Jean Van Heijenoort, Harvard University Press, 1967.
[7] Alfred Tarski, What are logical notions? History and Philosophy of Logic 7 (2):143-154 (1986)
[8] Zach, Richard, The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program, Synthese, 137:211-259, 2001.
[9] Kristóf János, Az analízis logikai alapjai, ELTE jegyzet, 1996.
[10] Kurt Gödel, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, in From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, ed.: Jean Van Heijenoort Harvard University Press, 1967
[11] Serény György, Gödel-tételkör, BME jegyzet.
[12] Smullyan, Raymond, Gödel nemteljességi tételei, TypoTEX, Budapest, 2005.
[13] Csaba Ferenc, (szerk.), A matematika filozófiája a XXI. század küszöbén. Osiris, Bp. 2003.
[14] Troelstra, A. S., Schwichtenberg, H., 2000, Basic Proof Theory, second edition. Cambridge: Cambridge University Press.
[15] Bell, J. L., 1993a. ‘Hilbert's epsilon-operator and classical logic’, Journal of Philosophical Logic, 22: 1–18.
[16] Jon Barwise (ed.), Handbook of Mathematical Logic (Studies in Logic and the Foundations of Mathematics), North-Holland; New edition edition (1 Mar. 1982)
[17] Torkel Franzén, Gödel nemteljességi tételei (Értelmezések és félreértések), TypoTeX, 2014.

Plakát (pdf)

Javasolt tételek (később)

Olvasmányok

(en)Hilary Putnam, "Is Logic Empirical?" or "The Logic of Quantum Mechanics" (pdf)
(en)Lakatos Imre, A Renaissance of Empiricism in the Recent Philosophy of Mathematics, The British Journal for the Philosophy of Science, Vol. 27, No. 3 (Sep., 1976), pp. 201-223, Oxford University Press (pdf)
(hu)Hilary Putnam, Modell és valóság (pdf)
(hu)Gottlob Frege, Fogalomírás (1879) c. könyvének egy rövid részlete és Jelentés és jelölet (1892) (pdf)
(hu)Dag Prawitz, Jelentés és bizonyítás: a klasszikus és intuicionista logika konfliktusa (pdf)
(hu)Alfred Tarski, Melyek a logikai fogalmak? (pdf), (en)(pdf)
(en)Sorensen, Urzyczyn, Curry--Howard Isomorphism (typed lambda calculus) (pdf)
(en)Russell & Whitehead, Incomplete symols: Descriptions (ps/djvu)
(en)Simon András, Introduction to Lambda Calculus (type free lambda calculus), (pdf)
(hu)William W. Tait, Finitizmus (pdf)
(hu)Paul Benacerraf, Amik a számok nem lehetnek (pdf)
(hu)Colin McLarty, Miért ne lehetnének a számok azok, amiknek lenniük kell? (pdf)
(hu)Georg Boolos, Még egyszer az iterációról (pdf)
(hu)Charles Parsons, Matematikai személet (pdf)
(hu)Richard Tieszen, A matematikai személet és Husserl fenomenológiája (pdf)
(hu)Kalmár László, A Hilbert-féle bizonyításelmélet célkitüzései, módszerei és eredményei (pdf) Matematikai és fizikai lapok, Bd. 48 (1941), S. 65–119.
(hu)Péter Rózsa, Az axiomatikus módszer korlátai (pdf) Matematikai és fizikai lapok, Bd. 48 (1941), pp. 120–143.
(hu)Kurt Gödel, Néhány tétel a matematika megalapozásáról és ezek következményei (pdf)
(en)Kurt Gödel, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, (ps/djvu)


Molnár Zoltán Gábor
2019. jan. 27.