Mmmmm... Según parece, hay diferencias muy importantes entre NBG y MK.
Más allá de mi torpeza, le voy a echar la culpa al mismo Ivorra, porque él da a entender que son más o menos lo mismo, y que las diferencias son mínimas.
Por ejemplo, en vez de introducir NBG en un breve artículo de él, se limita a decir que, en vez de eso, mejor introduce MK, que es más sencillo.
Ahí está dando la idea de que son cosas bastante "sustituibles" entre sí.
Pero estas diferencias que estás explicando van en contra de lo que uno intuiría en caso de que la sustitución de uno por otro fuera tan fácil.
En cuanto a lo que dijiste sobre el Teorema de Godel,
imagino que se trata de una sentencia G en particular, y no en general, porque a MK le afecta también el Teorema de Godel, y en él también hay sentencias indecidibles.
Por otro lado, olvidando eso, el Teorema del que estás hablando diría que, usando el formalismo de MK, es posible demostrar la consistencia de ZFC y NBG.
Otra vez, si la "distancia" entre MK y NBG es tan corta, como sugiere Ivorra, un Teorema como éste destruye la intuición del asunto. Las diferencias son muy sutiles, pero parecer que eso alcanza para lograr cosas que a mí me parecen sorprendentes.
¿Dónde puedo leer la demostración de ese Teorema?