Itt ugye valami olyasmi van, hogy tetszőleges rögzített véges rész esetén bizonyítható ZFC-ben hogy ez a véges rész konzisztens? Csak mert ha egy elmélet (itt most ZFC) minden véges része konzisztens, abból következne, hogy az egész is, az pedig ZFC-ben nem bizonyítható (ha ZFC konzisztens).

 

Igen, sőt, ZF-ben is. Ez Montague-Lévy. Következik, hogy a ZFC nem axiomatizálható végesen (de rekurzívan igen).

 

 

Valami olyasmi okozza ezt a jelenséget, hogy a végesség az ZFC-ben egy definiált fogalom, a metanyelvi szinten épített levezethetőségben pedig nyilván a "valóságban" lévő végességfogalommal dolgozunk?

 

 

Pontosan, én is így látom. Az a formula, amely a minden véges részek modelljének létezését mondja ki, a halmazelmélet nyelvén, tárgynyelvi formulával nem írható le. Ezért a halamzelmélet nyelvén ez a formula végtelen konjunkció, és mint ilyen, nem lehet tétel (a klasszikus elsőrendű logikában).

 

Másrészt ez azért igen plauzibilis, hihető állítás: a ZFC ellentmondásmentes! És ezt ZFC önmagáról a metaelméletben igazolja. Azonban - és erről is írtam már itt - a rekurzívan (azaz végső soron végesen) megfogalmazható, formulák felett kvantifikálható formulák "logikája" nincs rendesen megcsinálva (pl. teljességi, kompaktsági tétel hiánya).

 

Hasonló érveléseket érdekes módon pl. a Hajnal-Hamburger is elfogad (Függelék: Metatételek). A végtelen logikában Computable Formulas és Computable Logic néven említik ezt a logika-fragmentumot (pl. J. Barwise), és a Proof Theory-ban is foglalkoznak vele (végtelen, de rekurzív rendszámhosszú, effektivizálható) bizonyítások.

 

Mások, az algebrai logikában, az  alpha-rendű formulasémák logikájáról beszélnek, szemantikát is adnak neki(!), alpha általában megszámlálható rendszám.

 

 

Gondolj bele: ha ZFC omega lépésben igazolja magáról, hogy konzisztens (Gödel tétele ellenére), akkor micsoda világ nyílhat meg omega^omega^omega...:= epsilon_0, sőt még több lépésben?:)