"Nem tudom, mi a szokásos "kétvonalas" definíció."

Amit Te is mondtál (egy elméletben valamit pontosan akkor mondunk igaznak, ha az összes elméletet kielégítő modelben igaz). Ha az elméletben levezethető valami az az "egyvonalas" igazság. (És persze teljesség miatt a kettő egybeesik)

Szerencsésebb lett volna az elmélet szemantikai illetve szintaktikai következményeinek mondanom.

"hiszen előfordulhat, hogy a "minden n eleme omega: P(n)" állítás nem tétel annak ellenére, hogy P(0), P(1), P(2), stb. mindegyike az"

Ez ahhoz hasonló, hogy a halmazelmélet bármely véges része esetén tétel, hogy az konzisztens, de az nem tétel, hogy minden véges része konzisztens. Mindenesetre a fenti inkonzisztencia elég zavaró lenne.

Ami még érdekes dolog, hogy ZFC nem tudja eldönteni a saját konzisztenciáját. Itt is úgy érezheti az ember mint a Turing gépes esetben: ha le tudnánk vezetni belőle ellentmondást az rögtön eldöntené a kérdést. Persze ha ellentmondásos, akkor úgyis mindegy, hogy miket bizonyítottak belőle.