Had $\sf Con(ZFC)$ been explicitly written in first order language?

104 Views Asked by At

One always hear of $\sf Con(ZFC)$ and what is meant by that is an arithmetical sentence that is equivalent to $\sf ZFC \text { is consistent }$ that is written in the language of first order $\sf ZFC$. However, I've never seen an actual first order sentence expressing this? Had this statement been explicitly written in the first order language of set theory before? and where can I find examples of such write-ups