És F az melyik állítás? Vagy bonyolult, mint pl. a gödeli mondatok?

Az eredeti kérdésem meg arra irányult, hogy "metabizonyítás" adható arra, hogy valamelyik formula hamis, de ekkor ez a bizonyítás formalizálható-e ZFC keretein belül. Mert ha igen, akkor van olyan formula, aminek az igazsága ZFC-ben nem eldönthető (mint ahogyan azt bizonyítani lehetett az érvelésben), másrészt a meta ZFC-ben eldönthető, hogy az a formula hamis (mint ahogyan azt bizonyítani lehet a metaérveléssel). Tehát a formula igazsága végeredményben ZFC1-ben nem eldönthető, és ZFC2-ben eldönthető.

Ugyanígy még engem érdekelne, hogy ugye ZFC-ben akkor végülis megfogalmazható-e, és van-e értelme annak, hogy "a legkisebb, ZFC-ben nem definiálható rendszám". Szerintem kicsit hasonló a két probléma.