(Esetleg olyasmiről van szó, hogy valahogy a beágyazzuk a másodrendű logikát az elsőrendűbe olymódon, hogy a másodrendű logikai formákat halmazokként tekintjük a halmazok elsőrendű nyelvén, és akkor mindent elsőrendben tudunk tárgyalni?)
(Sajnos az ottani diszkusziót nem teljesen értem, ezért nem vagyok biztos benne 100%-ig, hogy az összefüggőség tényleg nem elsőrendben megfogalmazható tulajdonság, de 99%-ig azért biztos vagyok benne.)
Igen, a halmazelméletben ezt jól meg tudod fogalmazni. Igazából a halmazelmélet pont úgy van "kitalálva", hogy mindent precízen ki tudjunk fejezni a matematikában, vagy legalábbis erre tökéletesen alkalmas.
A formalizálhatósággal kapcsolatos agályaimnak az volt az alapja, hogy ha mondjuk a gráfelmélet nyelvét bővíted egy s és egy t konstansszimbolummal és azt szeretnéd mondani, hogy van s és t között út, akkor nem nagyon tudtam, hogy ez hogy lehetne csinálni, de aztán rájöttem, hogy ha a halmazelmélet nyelvén beszélek akkor ezt meg tudom fogalmazni egy omegán értelmezett függvényt bevezetve (az eredeti nehézség onnan jött, hogy csak adott n-re n hosszú út létezését kifejező formulát tudtam csinálni, végtelen sok formulát meg nem vagyolhatok össze).
Köszönöm szépen, ez hasznos információ. Nyilván ebben el kell mélyedni, hogy az ember (szubjektív) véleményt alkosson. Mint mondtam, gyakorlati szempontból ZFC-ben fel lehet építeni a matematikai logikát. Ennek annyi baja van, hogy ha ZFC inkonzisztens, akkor bukta van, de akkor persze sok más bukta is van.
El kéne olvasnom rendesen ezt a jegyzetet, hogy normális véleményt mondhassak, de ehhez most sem időm, sem kedvem nincsen. Beleolvasva a pontokba, nem sokat értek belőlük, pl. az 5-ösben (122. oldal) ezt mondja:
A mindennapi matematikai bizonyításokban sokszor a következőképpen járunk el. Tegyük fel, hogy bebizonyítottuk a "van x: A" formuláról, hogy tétel. Ekkor azt mondjuk, hogy "legyen T olyan objektum, amelyre (T|x)A tétel", majd tovább folytatjuk a bizonyítást.
Én ezt nem értem. Én a bizonyításaimban ha egy "van x: A" alakú formulát (tételt) használok, akkor ezt úgy használom, ahogy le van írva: felteszem, hogy van egy x, amire az A formula igaz. Más szóval van egy x halmaz, amit az A formulában az "x" szimbólum helyére írva a kapott formula igaz lesz, és innen haladok tovább. Nem értem, miféle T objektumról beszél a szerző, amit a mindennapi bizonyításokban használnánk.
Mindenesetre megnyugtató, hogy a 9-es pont szerint a matematikai elméletek egyenértékek "bizonyos értelemben" az elsőrendű elméletekkel. Én Csirmaz jegyzetéből tanultam a matematikai logikát. A jegyzet azt a nézetet követi, hogy a matematikai elméletek megegyeznek az elsőrendű elméletekkel, továbbá mind a szintaktikát, mind a szemantikát ZFC-ben építi fel. Tehát a formulák halmazokról szólnak, a változók értékei halmazok, és egy elmélet modelljei is halmazokkal írhatók le. Az biztos, hogy gyakorlati matematikai szempontból ez teljesen kielégítő felépítés, a legtöbb matematikus számára ZFC az univerzum (esetleg közeli rokonai, mint ZF). Filozófiai vagy logikai szempontból esetleg mást is lehet mondani, illetve ZFC ellentmondásossága esetén újra kéne gondolni mindent, de ezzel nem foglalkoztam idáig (és gyanúm szerint ezután sem).
Huh, ennyire nem akartam belemerülni. Esetleg oszd meg velünk azt a 8 pontot. Lehet, hogy a szerző talált egy jobb módszert a matematika megalapozására, mint az elsőrendű elméletek, de ha így is van, arról kevesen tudnak. A MathSciNet tanúsága szerint a szerző munkái a funkcionálanalízis területéről valók (nem a logika területéről) és nem keltettek nagy feltűnést (25 év alatt 8 cikk, ezekre 6 nyilvántartott hivatkozás).
Akkor ha jól értem a legkevésbé sem osztod azt a nézetet miszerint:
"A fenti ´eszrev´etel f´eny´eben mondhat´o, hogy az els˝orend˝u elm´eletek kev´esb´e alkalmasak a matematika megalapoz´as´ara, mint az 5. pontban t´argyalt matematikai elm´eletek. De az els˝orend˝u nyelveket ´es elm´eleteket eredetileg sem erre, hanem logikai vizsg´alatok c´elj´ara fejlesztett´ek ki."
A "fenti észrevételek" rész arra vonatkozik, hogy a szerző előtte 8 pontban összefoglalja, hogy az Általa matematikai elméletnek nevezett dolgok milyen tekintetben jobbak, mint az elsőrendű elméletek.
Hogy pontos hivatkozást is adjak: Kristóf János Tanár Úr "A matematikai analízis logikai alapjai" című jegyzetnének 121. oldalának közepétől sorakoztatja fel az érveit, előtte pedig számomra teljesen ismeretlen logikai eszközöket használ a "matematikai elméletek" fölépítésére, amik lényegesen mások mint az elsőrendű elméletek.
Elsőrendű elméletek milyen viszonyban vannak pontosan a "matematikai elméletekkel"?
Minden általam ismert matematikai elmélet formalizálható mint elsőrendű elmélet.
Elsőrendű nyelven mik pontosan a formalizálhatóság korlátai?
Nem ismerek ilyen korlátot, legalább is nem olyat, ami a matematikában korlátként jelentkezne.
(Nyilván azt nem lehet formalizálni, hogy teszem azt egy Turing gép megáll-e, mert ha lehetne, akkor teljesség miatt ezt el is lehetne dönteni, holott tudjuk, hogy ez eldönthetetlen)
Természetesen lehet azt formalizálni, hogy egy Turing-gép megáll-e. Ahogy emberi szavakkal pontosan meg tudod fogalmazni (tudod definiálni), hogy mit jelent a Turing-gép és annak megállása, úgy ezt ZFC-ben (vagy akár PA-ban is) meg tudod tenni. A megállási probléma eldönthetetlensége mutatja, hogy ZFC (vagy akár PA) nem teljes.
Azokat a tételeket, amiket "az ember az iskolában tanul" mind le lehet írni mondjuk a halmazelméletnek a nagyon egyszerű nyelvén és a bizonyításelméletnél megismert levezetés szerint le lehet vezetni?
Minden általunk tanult tétel megfogalmazható és bizonyítható ZFC-ben. Nekünk embereknek megvan az a képességünk, hogy nem kifejezetten formális a gondolkozásunk (hanem sokszor képi, analógiás, intuitív), ezért a legtöbb bizonyításunk jóval hosszabb lenne rendesen formalizálva, mint ahogy kitaláljuk vagy tanuljuk. Ha egy tétel vagy a bizonyítása nem formalizálható ZFC-ben, akkor azt a matematikusok többsége nem fogadja el tételnek. Persze vannak alternatív axiómarendszerek, de ezek a matematikusok kisebb csoportját érdeklik (pl. logikusokat, halmazelmélészeket).
Olvasgattam egy logikai irományt és jópár dolog fölmerült bennem:
Elsőrendű elméletek milyen viszonyban vannak pontosan a "matematikai elméletekkel"?
Mit mond Hilbert két epsilon tétele?
Elsőrendű nyelven mik pontosan a formalizálhatóság korlátai? (Nyilván azt nem lehet formalizálni, hogy teszem azt egy Turing gép megáll-e, mert ha lehetne, akkor teljesség miatt ezt el is lehetne dönteni, holott tudjuk, hogy ez eldönthetetlen)
ZFC miért olyan "nagyon jó"?
Azokat a tételeket, amiket "az ember az iskolában tanul" mind le lehet írni mondjuk a halmazelméletnek a nagyon egyszerű nyelvén és a bizonyításelméletnél megismert levezetés szerint le lehet vezetni?
Bizonyára, de ezt most nem tudom átgondolni, lehetséges, hogy egy halmaz (pl. megszámlálható halmazok) effektív definícióval jólrendezhető, de maga az univerzum nem.
Először is, természetesen vannak ZF-ben effektíven jólrendezhető halmazok; ilyen mondjuk Ord egy megfelelő halmaza (nyilván nem az összes). Én persze nem erre gondoltam; másrészt az "effektív definíció" alatt magát a rendezést definiáló halmazelméleti formulát értettem, nem olyan tételt, hogy mondjuk "létezik Sigma_2^1-jólrendezés". Efféle tétel több is létezik (pl. Gödel, Jensen, Harrington).
Azt hiszem, annyit lehet mondani erről, hogy ha egy halmaz (a Church-tézis értelmében) effektív formulával jólrendezhető, akkor ez AC nélkül jólrendezhető, ZF+alkalmas formula elméletében. Ehhez nem szükséges, sejtésem szerint, hogy a halmazuniverzumnak definiálható jólrendezése legyen.
Az mindenképpen érdekes (egyébként), hogy a megszámlálható/kontinuum számosságú halmazok effektív formulával jólrendezhetők-e valamilyen ZFC-struktúrában, ahol nincs definiálható osztály-jólrendezés. Milyen axióma szükséges - ezt nem tudom.
feltesszük azt, hogy létezik definiálható jólrendezés. ZF+V=L alatt például van ilyen, mint ahogyan HOD-ban is. HOD ilyen szempontból maximális.
Egészen pontosan, ezekben a modellekben van osztály-jólrendezés, ami különben a modellbeli AC igazságának igazolása (Gödel, L esetében). Bizonyára, de ezt most nem tudom átgondolni, lehetséges, hogy egy halmaz (pl. megszámlálható halmazok) effektív definícióval jólrendezhető, de maga az univerzum nem.
Itt egy plusz feltétel: feltesszük azt, hogy létezik definiálható jólrendezés. ZF+V=L alatt például van ilyen, mint ahogyan HOD-ban is. HOD ilyen szempontból maximális.
Másrészt ilyenkor mindig alkalmazhatunk AC-t (szükségtelenül), akkor viszont a függvény sosem(!) lesz definiált. Tehát Replacement nélkül mindig van halmaz-értékkészletű függény, de éppen a konstruktivitást veszítjük el.
Ez úgy hangzik, mintha a séma és az axióma helyettesíthetné egymást valamilyen értelemben, ami nem igaz.
Mint már említettem, világos az is, hogy van összesség, amely halmaz ZFC-ben, de nem ZC-ben. Márcsak ezért sem lehetnek ekvivalensek, semmilyen absztrakt (nemkonstruktív) értelemben sem.
Az viszont igaz, és ezt akartam mondani, hogy ha ZFC-modellben Replacement-tel f függvényt definiálunk, amelynek értékkészlete persze halmaz, akkor f értelmezési tartományához tudunk rendelni AC-vel más halmazokat. Például vesszük D_f egy elemét, unióját egy akármilyen halmazzal, és kiválasztunk egy elemet az így kapott halmazból. Az AC-vel nyert R_f szintén halmaz lesz, és ez a lényeg.
Végül, valamivel értelmesebb téma. Ismert, hogy van megszámlálható Peano-modell. Jólrendezzük most a megszámlálható halmazokat, és vegyük a minimális Peano-modellt. Így AC-vel tényleg definiáltunk egy halmazt. Igaz ugyan, hogy a definíció semmitmondó.
Így az AC-vel konstruktívak tudtunk lenni. Ez a megoldás egyébként ismert.
Hjorth egy cikkét olvastam először erről: egy infinitary elméletet nem feltétlenül axiomatizálhatunk egymástól független formulákkal!
Ennek, azt sejtem, kombinatorikai okai is vannak.
Azért gondolom, hogy kombinatorikai is lehet a probléma, mert valójában végtelen gráffal dolgozunk. A gráf a jólrendezett formulákból áll. A levezetés a gráfon értelmezett speciális rekurzív függvény.
Tájékoztatásul mondom el, hogy ma már olyan first order logika is van, amelyben a levezetések egy nemsztenderd Peano-modell véges, és végtelenül nagy számaival Gödel-számozhatók. Ebben a speciális infinitary logic-ban következmény-reláció (algebrai lezárási operátor), és vele modellemélet van teljességi tétellel, és egyéb szokásos tételekkel (Beth-tétel, például).
Ebben a végtelen logikában csak a levezetések (speciális alakú formulák) lehetnek végtelenek. Minden más formula véges. Nem tudom, hogy mennyire lehet általánosítani. Azt tudom, hogy független axiomatizáció lehetséges; más infinitary logikáknál ez pl. a kontinuumhipotézishez, a Vaught-sejtéshez kötött (Lomega1, omega esetben).
Ez egyébként annak idején engem meglepett, Gerg Hjorth egy cikkét olvastam először erről: egy infinitary elméletet nem feltétlenül axiomatizálhatunk egymástól független formulákkal!
De arról, hogy ilyen formula létezik, tehát ami reprezentálja PA konzisztenciáját csak akkor bizonyosodhatnánk meg, ha PA inkonzisztens lenne.
Abban az értelemben, ahogyan szeretnéd, semmiképpen sem lehet a PA konzisztenciája PA-ban reprezentálható. Az azt jelentené, hogy pontosan akkor vezethető le, ha a PA konzisztens, ami nem lehet, mert ellentmondásból minden következik.
A válasz tehát az, hogy nem "reprezentálhatjuk" a PA konzisztenciáját a PA-ban. Ha a PA inkonzisztens, akkor Consis tétel voltából ezt tudod, de akkor bármilyen mondat levezethető, például 0=1, ami így persze szintén "reprezentál".
Consis abban az értelemben reprezentál pontosan, hogy a véges természetes számokon pontosan akkor igaz, ha a PA konzisztens.
Nem igazán értem, hogy ez miért jelentené azt, hogy a PA-n belül nem tudjuk levezetni a PA konziszenciáját. Hiszen ebben az esetben kéne egy formula, amire teljesül, hogy reprezentálja PA konzisztenciáját PA-ban és nem is vezethető le. De arról, hogy ilyen formula létezik, tehát ami reprezentálja PA konzisztenciáját csak akkor bizonyosodhatnánk meg, ha PA inkonzisztens lenne.
Rossz a következtetés. Arról, hogy van olyan Consis formula, amely reprezentálja PA konzisztenciáját nem akkor bizonyosodhatunk meg, ha a PA inkonzisztens, sőt, semmi köze nincs hozzá.
Consis azért jól reprezentál, mert a PA-tételek felsorolhatók, és akkor van őket felsoroló P rekurzív függvény, amelyre PA-ban a Gödel-féle kritériumok teljesülnek, és ebből a P-ből definiáljuk Consis-t. Ez ZF-tétel.
Azért jelentené az állításom azt, hogy PA-n belül nem tudjuk levezetni a PA konzisztenciáját, a Gödel-i Consis-szal, mert ez Gödel tétele, és a kérdés erre vonatkozott.
Lehet más mondat, amely szintén reprezentál. Erre Gödel tétele nem vonatkozik, ám ha egyáltalán le tudjuk vezetni, az semmit sem jelent, mert ha a PA ellentmondásos, akkor is le tudjuk vezetni (és a negációját is). Ezért mondhatjuk: PA semmiképpen sem tudja levezetni a saját valódi konzisztenciáját.
"Arról meg tudunk győződni, hogy ha a Consis-t nem tudjuk levezetni, akkor a (metanyelvi) konzisztenciát nem tudjuk levezetni, de a PA konzisztens"
Nem igazán értem, hogy ez miért jelentené azt, hogy a PA-n belül nem tudjuk levezetni a PA konziszenciáját. Hiszen ebben az esetben kéne egy formula, amire teljesül, hogy reprezentálja PA konzisztenciáját PA-ban és nem is vezethető le. De arról, hogy ilyen formula létezik, tehát ami reprezentálja PA konzisztenciáját csak akkor bizonyosodhatnánk meg, ha PA inkonzisztens lenne.
De miért baj? Nem lehet vele sok tudományos elméletet formalizálni?
Ez nehéz kérdés. Voltaképpen lehet formalizálni, de valóban problematikus, kontraintuitív eredményekre vezet. A parakonzisztens logikák szemantikája kevéssé kidolgozott, márpedig akkor nem tudod azt gondolni, hogy valamilyen entitásokról szóló állításaid vannak, hiszen nincs ilyen formalizmus. De akkor mit gondolj?
J. Hintikka például olyan parakonzisztens modelleket gondolt el, amelyek időben(!) változnak. Tehát a modellelméletbe bevezette az idő fogalmát! Az ellentmondás annyit jelent, hogy a fi állítás igazságértéke a modellben változik. A matematikusok számára ez elfogadhatatlan metafizikai feltételrendszer.
A fizikai matematika is teljesen megváltozik, a tételek bizonyítását át kell írni.
Másrészt a fizikában valóban vannak inkonzisztenciák, mint mondjuk a renormálás, a kvantummechanika plauzibilis értelmezései. Végül a Predikátumkalkulus tényleg furcsa: minden x F(x) implikálja, hogy létezik x F(x). Következik, hogy van legalább egy repülő ló (ez a standard példa mindig), pegazus, csak mert elképzelhető ellentmondás nélkül.
Vagy a legtriviálisabb példa: adjunk tudományelméleti magyarázatot arra, hogy 0=1-ből miért következik az összes állítás! Ilyet senki sem tudott még adni.
A parakonzisztens logikák egyik motivációja az volt, hogy az abszolút konzisztenciát igazolják, miközben az aritmetika eldönthetetlen.
Ha egy logikában az ellentmondásból nem következik minden, nyilván van értelme annak is, ha levezetjük a konzisztenciát hűen tükröző tárgynyelvi mondatot. Ez azonban nem jelent abszolút konzisztencia-bizonyítást.
Meg kell említeni, hogy a konzisztencia-bizonyítások általában egyaránt metanyelvi és tárgynyelvi jellegűek, mint pl. Gentzen igazolása a Peano-aritmetikára. Itt nem a Gödel-féle Consis-mondatot igazolja másik rendszerben, hanem a metanyelvi konzisztenciát; egyszerre érvel a metaelméletben, és a tárgynyelvi elméletben, és a tétel egy metatétel.
A metatételből persze követketethetünk arra, hogy a tárgynyelvi Consis-formulák is igazak a sztenderd modellen, de ez metabizonyítás!
Valamelyik előző hozzászólásban már kifejtettem, hogy a Consis bármelyik tárgynyelvi formájának előállítása reménytelen (sőt, azt hiszem, nem is lehetséges) az aritmetikában.
Nyilván, a vegyes metaelméleti konzisztencia-bizonyításnak is akkor van értelme, ha a metaelmélet, és a másik rendszer konzisztenciáját feltesszük. Ez még abszolút konzisztencia-bizonyítás esetén is így van: az Állításlogika abszolút konzisztenciája nem véges, hanem végtelen esetre redukált, azonban rekurzívan, formulaindukcióval finitizálunk. Feltevés (axióma), hogy ezt lehetséges, és konzisztens.
"De Te eleve azzal a feltételezéssel élsz, hogy a PA konzisztens, akkor Gödel tétele miatt igazad van, de Feferman konstrukciója szerint nincs igazad, ám akkor is igaz, hogy PA-ban eldönthetetlen a saját konzisztenciája, metanyelvi értelemben.
Ekkor tehát igazad van: nincs olyan mondat, amely ha levezethető PA-ban, akkor a PA konzisztens (ez abból következik, hogy ellentmondásból minden következik)."
Bocsánat, ez sztornó (bár a matematikai állítások magukban igazak):
Emájti állítása az, hogy
"az a metanyelvi mondat, hogy az 'aritemtika konzisztenciáját nem vezethetjük le az aritmetikában' nem igaz",
ami semmiképpen sem igaz, hiszen igaz, hogy metanyelvi értelemben a PA konzisztenciáját semmiképpen sem vezethetjük le a PA-ban.
De még akkor sem, ha van egy jó tárgynyelvi megfelelőnk (Feferman-féle Consis), hiszen ellentmondásból minden következik.
Ehhez mit szólsz, nem igazán értettem korábban, hogy ezt elfogadod-e, vagy csak az a problémád, hogy itt az omega-konzisztenciáról van szó.
"az a metanyelvi mondat, hogy az 'aritemtika konzisztenciáját nem vezethetjük le az aritmetikában' nem igaz, mert egyszerűen nem tudunk meggyőződni arról, hogy amennyiben Consis-t nem tudjuk levezetni, akkor azzal egyúttal a konzisztenciát nem tudjuk levezetni."
A mondat első állítása nem igaz, mert a Gödel-i Consis pontosan akkor igaz a sztenderd modellen, ha a Peano-aritmetika konzisztens, és ha a Consis-t le tudjuk vezetni, akkor a PA ellentmondásos.
De Te eleve azzal a feltételezéssel élsz, hogy a PA konzisztens, akkor Gödel tétele miatt igazad van, de Feferman konstrukciója szerint nincs igazad, ám akkor is igaz, hogy PA-ban eldönthetetlen a saját konzisztenciája, metanyelvi értelemben.
Ekkor tehát igazad van: nincs olyan mondat, amely ha levezethető PA-ban, akkor a PA konzisztens (ez abból következik, hogy ellentmondásból minden következik).
A konzisztencia eldöntése az aritmetikában együtt jár a tételek osztályának eldönthetetlenségével. A parakonzisztens logikák egyik motivációja az volt, hogy az abszolút konzisztenciát igazolják, miközben az aritmetika eldönthetetlen. Van ilyen rendszer: a Predikátumkalkulus konzisztenciája abszolút (finit) módon igazolható, de a PK nem dönthető el.
A mondat második állítása hibás.
Arról meg tudunk győződni, hogy ha a Consis-t nem tudjuk levezetni, akkor a (metanyelvi) konzisztenciát nem tudjuk levezetni, de a PA konzisztens. Ez Gödel tétele.
Arról nem tudunk meggyőződni, hogy a Consis-t nem tudjuk levezetni (ha tényleg nincs levezetés). Ekkor a metanyelvi konzisztenciát sem tudjuk, vagyis a PA konzisztenciája ekkor eldönthetetlen.
Mivel a mondatok hibásak, az implikációval nem foglalkoztam.
