As question arise from answer on discussion in this:
Theorems in MK would imply theorems in ZFC
'consistency of ZF can't prove consistency of MK because consistency of MK proves consistency of ZF'. Does 'MK proves Con(ZF)' where Con(ZF) is particular formula used by Godel.
As in wikipedia page:
https://en.m.wikipedia.org/wiki/Von_Neumann–Bernays–Gödel_set_theory
'NBG—and hence ZFC—can be proved consistent in MK.'
What formula MK proves for consistency of these theories.
And linking this to my another question: Clarification about Godel Second Incompleteness theorem
Does Con(ST) in second incompleteness theorem is kind of formula which had to be true if ST is consistent. i.e. (It is not obviously of type that if it is not true, then ST is not consistent)