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.

Most el kell mennem, de majd benézek valamikor.