Vagy bonyolult, mint pl. a gödeli mondatok?

 

Szubjektív, hogy mi a bonyolult. De igen, egy gödeli mondatról van szó, pontosabban a példámban "minden n-re F(n)" egy gödeli mondat a példámban, feltéve hogy ZFC konzisztens és omega-konzisztens.

 

"metabizonyítás" adható arra

 

Szerintem metabizonyítások nem léteznek, legfeljebb "metaérvek", filozofikus érvek, vagy érzések. Minden bizonyítás axiómákat használ és persze formalizálható a ZFC-ben (akkor is, ha nem ZFC-beli bizonyításról van szó).

 

másrészt a meta ZFC-ben eldönthető

 

Nem ismerek "meta ZFC"-t.

 

Tehát a formula igazsága végeredményben ZFC1-ben nem eldönthető, és ZFC2-ben eldönthető.

 

Nem ismerek ZFC1-et meg ZFC2-t. Van a ZFC és kész.

 

ugye ZFC-ben akkor végülis megfogalmazható-e, és van-e értelme annak, hogy "a legkisebb, ZFC-ben nem definiálható rendszám"

 

Nem világos, mit értesz megfogalmazáson meg értelmen. Számomra "a legkisebb, ZFC-ben nem definiálható rendszám" nem létezik. Szerintem ez egy értelmetlen fogalom (halandzsa). Persze ha veszel egy másfajta halmazelméletet és ott definiálod a "rendszám" és a "ZFC-beli definiálhatóság" fogalmát, ott már értelme lehet ennek a fogalomnak. De persze ebben a másfajta halmazelméletben egészen mást fog jelenteni a rendszám, mint a ZFC-ben. Illetve a ZFC-ben is megcsinálhatod ezt, de csak egy furcsán definiálható rendszámot fogsz kapni, semmi többet.