Nem is mondtam, hogy tétel lenne, csak hogy biztos van egy szigorú szintaktikai "levezetése" annak a bizonyos metaérvelésnek, mert ha nem lenne, akkor nem lenne igaz a Church tézis (ami ilyen szempontból egy naiv természetes nyelven megfogalmazott matematikai tételnek is tekinthető). De mivel nem tudom, hogy konkrétan hogy is néz ki formálisan egy ilyen "levezetés", ezért nem tudom, hogy ZFC-ben bizonyítható-e, vagy hogyan formalizálható. Erre kérdeztem rá, hogy lehet-e az állítás ZFC tétel. (csak elfelejtettem hirtelen, hogy melyik állítás, de az a metás behelyettesítős)