Amúgy vannak a metamath-nál kevésbé fapados szoftverek, wikipedian megtalálsz néhányat. A legfeljettebbnek tűnő a Coq.
A négyszín tétel kapcsán wikipedia ezt írja:
"In 2005 Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel (Gonthier 2008)."
Nem tudom, hogy van-e azóta számítógépmentes bizonyítás, talán Gergő tud erről felfilágosítást adni.
Coq-nak tényleg szép a kezelőfelülete és leírás alapján igen sokat tud, egy hátránya számomra, hogy ha jól értelmezem a kategoriaelméletes matek-megalapozáson alapul elsődlegesen (persze biztos lehet vele szimulálni a sztenderdet is).
A kijelentésnek nem sok értelme van. Talán arra akartak utalni, hogy a legtöbb bizonyításban nem kell konkrét számokkal számolni, hanem általánosabb gondolatokból kell építkezni. Wiles bizonyításában konkrét számok valóban ritkán szerepelnek. A bizonyítás egyik alapötlete, hogy a PSL(2,F3) csoport feloldható, amihez jó tudni, hogy a csoport 12-elemű.
Ezt találtam a Metamathban: "Fortunately, most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12." -Wow nem rossz. Hogy lehet ez?
Meg ezt: "( + 1 2 ) = ( + 1 ( 1 + 1 ) ). Believe it or not, this is a perfectly valid theorem of set theory!"
elsoszulott, Te megmutattad nekem a matematikus paradicsomot. Úgy hívják, hogy Metamath Proof Explorer.
Amúgy most egyetemen projektmunkaként automatikus tételbizonyítást szeretnék csinálni Wolfram Mathematicával. Van valakinek valami jó ötlete, hogy milyen problémákat mutassak be? Valószínűleg csak nulladrendű logikai dolgokat fogok bizonyítani (normálformák, stb), nem tudom, hogy elsőrendben, vagy modális rendszerekkel mi a helyzet. Szóval ha van valami érdekes probléma, javaslat: jöhet:D
Egyik logikus-halmazelmélész ismerősöm azt vallja (bár ez lehet Számodra kissé szentségtörés), hogy a jelenleg létező halmazelméletek közül sok van ami ugyanolyan jól megfelelne a matek megalapozáára mint ZFC és csak "historical accident" , hogy éppen a ZFC vált széles körben elterjedtté.
Viszont ZFC+ {létezik valódi osztálynyi elérhetetlen} már tudja interpretálni a kategóriaelméletes megalapozást (meg a Tarski-Grothendieck halmazelméletet, meg a Morse-Kelley osztályelméletet stb), tehát ha a jól megszokott alapjaink felől akarunk továbbmenni azt is meg tudjuk tenni.
Az NBG esetében érdekes a helyzet. Mivel halmazokról ugyanazokat a tételek bizonyítják ZFC-vel (és így speciálisan ekvikonzisztensek), így erre való továbblépés nem hordozna veszélyt. Másrészt osztályváltozók meg véges axiomatizálhatóság techninailag kényelmes.
Azt hiszem ZFC összes tétele (pontosabban azoknak a megfelelő átkódolása) tétel ebben a kategóriaelméletes megalapozásban is. Fordítva viszont nem igaz.
Ha kevesen is, de azért vannak komoly matematikusok, akik nem a halmazelméleti magalapozás hívei. Magyarok közül például Makkai Mihály.
Számomra a kérdés úgy merül fel, hogy mi az, ami nélkülözhetetlen (ahhoz, ami engem vagy a többséget érdekel). Szerintem toposzelmélet nélkül vígan el lehet élni, kategóriaelmélet nélkül úgy ahogy, matematikai logika nélkül egyre kevésbé, halmazelmélet nélkül pedig egyáltalán nem. Hogy a jövőben hogy lesz, azt nem tudom.
A formulák elég konkrét és gyakorlatias dolgok, nem kell hozzájuk különösebb intuíció.
szerintem a halmazok nem léteznek
A matematikában az az általános hozzáállás, hogy ha egy axiómarendszerben nincs ellentmondás, akkor a benne szereplő fogalmak léteznek. Mindenképpen léteznek azon a szinten, hogy lehet róluk beszélni, egyértelmű kérdéseket feltenni és válaszokat adni stb. A halmazelmélet bevezetése szükségszerű volt a matematikában. Egyrészt konkrét problémák megkövetelték, hogy halmazokról beszéljünk (pl. mely pontokban konvergál egy Fourier-sor), másrészt a matematikusok elkezdtek halmazokban gondolkodni (vegyük pl. a bázis vagy az ideál fogalmát az algebrában, a határ fogalmát a topológiában, vagy az atlasz fogalmát a geometriában). Tehát nem az a kérdés, hogy a halmazok léteznek-e, hanem hogy miként dolgozzunk velük. A halmazelméletet nem lehet mellőzni a matematikában, mert a ma ismert eredmények és fogalmak 90%-a szervesen épül rá. Ha neadjisten ellentmondást találnánk a ZFC-ben, akkor azt gondosan korrigálnánk, de semmiképpen sem vetnénk el "filozófiai alapon".
Amikor definiáljuk a Turing-gépeket, azok matematikai fogalmak, és a precíz matematikai definícióhoz szükség van egy előző precíz Turing-gép definícióra.
A Turing-gépeket általában a halmazelmélet fogalmaival szokták definiálni, a halmazelmélet pedig nem feltételezi semmiféle Turing-gép fogalmát (Turing még csak gyerek volt, amikor a halmazelméletet már elég komolyan művelték). Persze amikor a halmazelméletről magáról teszünk fel kérdéseket (pl. van-e benne eldönthetetlen formula), akkor hasznos a Turing-gép fogalma, de ez más tészta. Amennyire én tudom, a Turing-gép a matematikusok gondolatvilágában nem szerepel első helyen. Az enyémben semmiképpen sem.
"Amikor definiáljuk a Turing-gépeket, azok matematikai fogalmak, és a precíz matematikai definícióhoz szükség van egy előző precíz Turing-gép definícióra"
Vagy végtelen sokáig kell csinálni a szinteket (halmazelmélet, metahalmazelmélet, metametahalmazelmélet...) vagy ell sem kell kezdeni. Nekem utóbbi a szimpatikusabb, de ismerek olyan matematikust, aki előbbivel dolgozik.
Én annyit ehhez hozzátennék, hogy az eredeti Turing-gép (az univerzum) nem egy precíz matematikai dolog. Amikor definiáljuk a Turing-gépeket, azok matematikai fogalmak, és a precíz matematikai definícióhoz szükség van egy előző precíz Turing-gép definícióra. Tehát valahol a matematikai precizitás megszakad, és csak a világról alkotott intuíció marad. De az nem egy precíz matematikai fogalom. Csak erre akartam felhívni a figyelmet.
Nevezetesen van olyan formula Erről beszéltem:D Az a létezés már intuitív fogalom.
Nem tudom... szerintem a halmazok nem léteznek. Amikor számolunk, vagy összességekkel dolgozunk, akkor van néhány általános törvényszerűség, amiket használunk, de ettől még nem kell elfogadnunk, hogy léteznek halmazok. Ez szerintem ugyanolyan, mint amikor ZFC-ről beszélünk, akkor beszélhetünk osztályokról, de attól még osztályok nem léteznek a rendszerben.
csak beleolvasgattam ebbe amiről beszélgettek, de ennek kapcsán merem beírni ide, hogy van egy logikai elmélet-kezdeményem, ami nagyon durva
persze nem gondolom hogy feltaláltam valamit, de ki tudja... mindenesetre ilyet még nem olvastam sehol mint amit "feltaláltam"
persze nem merem leírni ide (pár embernek mutattam eddig, egyik kezdte csak megérteni), de hátha lenne itt olyan aki vevő lenne arra hogy esélyt adjon nekem, hogy komolyan vesz :)
röviden valami olyasmiről van szó, ami teljesen alapvető logikai dolog, és minden ami létezik(!) ebből nő ki, a matematika is(!)
és sajnos olyan, hogyha valaki elolvassa (elkezdtem leírni) akkor először legyint hogy ez semmi extra, és itt követi el a hibát
Ezzel nem is lenne bajom, ha a költészet, filozófia stb. intuitív alapjai is ugyanannyira megalapozottnak számíthatnának, mint a matematika alapjai.
Szerintem tévedésben vagy a matematika intuitív alapjait illetően. A matematika precizitását a szigorú szabályok adják, mint a sakkban. Ide lehet lépni, ide meg nem stb. A szabályokat pedig a világos és jól megragadható kérdések motiválják, pl. hány részre oszthatja 100 kör a síkot. Nem kell felépíteni nagyon precíz matematikát ahhoz, hogy ilyeneket kérdezzünk, elég ha van egy gyakorlatias elképzelésünk a benne szereplő fogalmakról, amiket aztán finomíthatunk. Tehát fordítva működik a dolog: az ilyen kérdések köré épül a matematika igény szerint.
akkor azt arra vezetjük vissza, hogy "létezik olyan formula, hogy..."
Nem arra vezetjük vissza, hanem ezt jelenti a levezethetőség definíció szerint. Nevezetesen van olyan formula, ami azt fejezi ki, hogy az axiómákból a nevezett "létezik x, hogy..." formula következik.
Hiszen mondjuk a létezik halmaz kijelentés elég hihetetlennek tűnik számomra
Nem tudom, mi a hihetetlen ezen. A mindennapi életben is beszélünk dolgok sokaságáról, összességéről, együtteséről, pl. egy bolt árukészletéről, egy iskola tanulóiról, vagy a Btk. paragrafusairól. Ezek halmazok, a naiv értelemben. Egy 8 éves gyerek nem problémázik azon, hogy az egész számok halmaza létezik vagy sem. Mert nem is kell. Elmondják neki és pillanatok alatt megérti, mit jelent a fogalom (ha figyel).
"létezik x, hogy..." (ZFC-beli formulával leírva) levezethető, akkor azt arra vezetjük vissza, hogy "létezik olyan formula, hogy..."
mintha a létezést visszavezettük volna a létezés inzuitív fogalmára
A formulák meg levezetések ZFC-ben definiált fogalmak, ezért tud a Logika tételeket bizonyítani róluk. A létezés intuitív fogalma pedig emberenként változhat. Vannak akiknek bizonyos nagy számosságok létezése nyilvánvaló valóság, másoknak a megszámlálható végtelen sem létezik.
mert a a halmazelméletre hivatkozik
Az elsőrendű nyelv szintaktikájában vannak jelek meg egyszerű szabályok amikkel manipuláljuk őket. Nem kell hozzá halmazelmélet, sőt a nem halmazelméleti alapú matematikát csináló (nem túl sok) matematikus is rendelkezik valamilyen jelkészlettel és szabályokkal amik előírják, hogy egy teljesen formalizált bizonyítás micsoda.
"Igen. Ezzel szerintem nincsen gond. Te mi mást javasolnál helyette?"
Nekem az a gondom, hogy amikor precízen akarjuk vizsgálni, hogy "létezik x, hogy..." (ZFC-beli formulával leírva) levezethető, akkor azt arra vezetjük vissza, hogy "létezik olyan formula, hogy...". De ez nekem teljesen olyan, mintha a létezést visszavezettük volna a létezés inzuitív fogalmára, és így mintha önmagával magyaráznánk a dolgokat. Ezzel nem is lenne bajom, ha a költészet, filozófia stb. intuitív alapjai is ugyanannyira megalapozottnak számíthatnának, mint a matematika alapjai. (Hiszen mondjuk a létezik halmaz kijelentés elég hihetetlennek tűnik számomra, éppen annyira, mint a filozófia sok más kijelentése)
Amit esetleg javasolhatnék, mint a matematika egy nagyon precíz felépítése, az a Ruzsa Imre: Logikai szintaxis és szemantika című könyvben leírt feléptés. Ott azt hiszem éppen az elsőrendű nyelvek felírásához kell több, mint száztíz axióma, de az előző posztomban leírt második problémára még ebben a felépítésben sem találtam megoldást.
A válaszod második felében mutatott feloldást azért nem tudom száz százalékos feloldásként elfogadni, mert a a halmazelméletre hivatkozik, de annak a halmazelméletnek a felépítésekor ugyanezek a problémák jelentkeznek. (Mondkuk Ruzsa Imre is intuitívan használja a halmaz fogalmát a mű elején, úgyhogy ennek a kritériumnak az a mű sem felel meg)
Szóval lehet, hogy nincs is gond, csak én problémázok, de azért jó lenne tudni, hogy hol bukik meg a gondolatmenetem.
A fizikai valóság formulái és a ZFC-ben felépített formulák nem ugyanazok, mintahogy egy szállítmányozási hálózat sem ugyanaz mint a belőle épített gráf. A valóság egy szeletének ragadjuk meg a számunkra fontos tulajdonságait, azt matematikailag modellezzük és erről a matematikai modellről bizonyítunk dolgokat. Ha az eredmények a valóságra visszafordítva hasznosnak bizonyulnak akkor érdemes volt csinálni. Márpedig a matematikát használó tudományok módszerei és sikerei szerint érdemes.
"De ezekben az axiómarendszerekben vannak olyan axiómák, amelyek kimondásához szükséges a metanyelv, mégpedig amikor az adott axiómarendszer formuláiról beszélünk."
Igen. Ezzel szerintem nincsen gond. Te mi mást javasolnál helyette?
"Az az állítás, hogy az induktív módon meghatározott adott jelsorozatokon kívül minden egyéb jelsorozat nem formula, igencsak rendszeren kívülinek tűnik."
Ez jogos észrevétél.
Egy lehetséges precízzé tevés dallama: a legszűkebb olyan halmaz, ami tartalmaz ezt meg ezt és zárt az ilyen meg olyan műveletekre. Másik: olyan s amihez létezik véges sorozat melyre minden tag ez vagy az, vagy így meg úgy keletkezik a korábbi tagokból és az utolsó tag éppen s.
Elnézést, hogy mindenről ugyanaz jut eszembe (programozói szakmai ártalom), de érdekes, hogy hogy át lehet írni a párbeszédeteket Turing gépekre. Szerintem ezek ekvivaleens dolgok valahol. Ha nem haragszol átírom:
Tegyük fel, hogy az egész univerzum egy nagy számítógépen, egy Turing gépen fut (szimulálódik).
D: De a Turing gép felépítéséhez szükséges a meta Turing gép.
G: Nem kell hozzá a meta Turing gép, felépítheted egy Turing gép szimulációban (mint a világunk). Mint mondtam, a Turing gépet úgy kell megépítened, ahogy megtanulsz házat építeni. A turing gépet mechanikailag kell felépíteni először, utána lehet Turing gép szimulációt szoftverként megírni (Turing gépre).
De ezekben az axiómarendszerekben vannak olyan axiómák, amelyek kimondásához szükséges a metanyelv
Nem kell hozzá a metanyelv, kimondhatod a ZFC-ben. Mint mondtam, a ZFC-t úgy kell magadévá tenned, ahogy megtanulsz járni vagy beszélni. A ZFC-t intuitívan kell elsajátítani először, utána lehet formalizálni azt is és minden mást is (a ZFC-ben).
Ugyanez a helyzet a formulák induktív meghatározásakor.
A formulákat induktívan (azaz rekurzívan) tudod definiálni a ZFC-ben. Valójában bármi, ami eszedbe jut, formalizálható a ZFC-ben, így van kitalálva. Amennyire tudjuk, a ZFC minden matematikai elmélet megragadására alkalmas. Univerzális, ezért szeretjük.
Konkrét példa erre ZFC vagy PA felépítése. Mindkét rendszer axiomatizál bizonyos intuitív fogalmakat (halmaz, szám). De ezekben az axiómarendszerekben vannak olyan axiómák, amelyek kimondásához szükséges a metanyelv, mégpedig amikor az adott axiómarendszer formuláiról beszélünk. A formulákról pedig szükséges beszélni az axiómasémákban (helyettesítési, teljes indukciós).
Ugyanez a helyzet a formulák induktív meghatározásakor. Az az állítás, hogy az induktív módon meghatározott adott jelsorozatokon kívül minden egyéb jelsorozat nem formula, igencsak rendszeren kívülinek tűnik. (Mondjuk ez lehet, hogy kiküszöbölhető egy sokkal bonyolultabb definíció árán)
Formalizálásra szerintem úgy érdemes gondolni, mint egy módszer arra, hogy nagyon objektíven meg tudjuk mondani azt, hogy mit bizonyítottunk és ehhez milyen feltevéseket és következtetési szabályokat használtunk.
Egyre nagyobb adatbázisok vannak teljesen formalizált komoly tételekről pl metamath, Coq, Isabelle programokkal készítik ezeket.
Ezekután a "jó-e a bizonyításom?" kérdést a számítógépemnek is feltehetem, nem kell tapasztaltabb kollegák idejét rabolni.
Nem beszélve a bizonyító és interaktív bizonyító programokról. Van olyan tétel aminek máig nem ismert "computer-free" bizonyítása.
"mindig használjuk a "bizonyításainkban" ezt a nyelvet."
Ez nem teljesen értem. Tudsz mondani egy konkrét szituációt, amit problémásnak érzel?
"Tegyük fel, hogy adva van a ZFC szintaktikájának a felépítése. Ehhez használtuk a halmazelméletet"
Pont ezt beszéltük régebben, hogy a külső szintaktikai szinthez nem kell halmazelmélet, csak jelek egyszerű manipulálása.
Az én felfogásomban az 1-es pontod a helyes, kiegészítve ezzal, hogy matekot természettudományokban, informatikában stb használjuk, tehát itt bizonyos értelemben tapasztaljuk, hogy "valóságban igaz" amit bizonyítunk.
Mondjuk bennem fel sem merült az objektivitás hiánya, pont azért, mert tudom, hogy mechanikusan legyárthatók a matematikai tételek. Valami vagy szerepel a listában, vagy nem. Ha pedig neadjisten egy állítás és az ellentettje is szerepel a listában, akkor ott ette meg a fene.
amikor már felépítettük ZFC-t, akkor a precíz igazságdefiníció mindig csak egy metanyelvben ellenőrizhető
Ez vagy nem igaz, vagy nem értem. A ZFC-ben definiált igazságdefiníció csak olyan, mint bármilyen más definíció. Ennek folytán a vele kapcsolatos állítások ZFC-tételek (jó esetben), mint bármilyen más matematikai tétel. Pl. ZFC-ben egyszerű tétel, hogy "omegán igaz az xy=yx azonosság". Ez a tétel a ZFC-ben definiált igazságdefiníciót használja, és ZFC-ben ellenőrizzük az igazságértéket.
