Axiomatizing ZFC+Con(ZFC) without adding a constant symbol

Question

I think ZFC+Con(ZFC) can be axiomatized in the following way.

Suppose our language is $(\in, w)$ where $w$ is a constant symbol.

1. Take every axiom of ZFC.
2. For every axiom of ZFC with parameters in $w$ called $\varphi(P)$, take $w \models \varphi(P)$ as an additional axiom.

Truth in a structure has a recursive definition on the structure of the formula with parameters $\varphi(P)$, so we can expand $w \models \varphi(P)$ to a sentence with parameters in the language $(\in, w)$.

There's no requirement that $\in$ in $w$ line up with the real $\in$, i.e. $w$ does not need to be a standard model or a transitive model, or anything like that.

This is intentional; I'm trying not to accidentally produce a stronger theory than ZFC+Con(ZFC).

Anyway this approach to producing a theory of ZFC+Con(ZFC) introduces a new constant symbol $w$. $w$ can't be removed in a naive way from this axiomatization because ZFC is not finitely axiomatizable and thus $[\exists w](\text{ZFC}(w))$ is not a finite sequence of symbols.

So, how does one axiomatize ZFC+Con(ZFC) without introducing a constant symbol?

Answer 1

Even though ZFC is not finitely axiomatizable, it is recursively axiomatizable: there is an algorithm to determine whether a given formula is an axiom of ZFC. Using this, we can define a predicate $\operatorname{IsAxiom}(\varphi)$ that asserts that $\varphi$ is a ZFC axiom. (More precisely, if $\varphi$ is a formula in the language $(\in)$, let $\overline{\varphi}$ be the object representing $\varphi$ in ZFC's formalization of first-order logic. Then $\operatorname{IsAxiom}(x)$ asserts that $x = \overline{\varphi}$ for some $\varphi$ and $\varphi$ is a ZFC axiom.) We can then define a predicate $\operatorname{Proves}(\varphi)$ that asserts $\mathrm{ZFC} \vdash \varphi$. Finally we can formalize $\operatorname{Con}(\mathrm{ZFC})$ as $\lnot\operatorname{Proves}(0 = 1)$.

Answer 2

Use compactness.

You get the existence of a model $w$ if every finite subset of ZFC is finitely satisfiable. That can be asserted without adding a constant symbol.

For concreteness, for all finite fragments $\Delta$ of ZFC, we assert that $[\exists z](\Delta(z))$.

Then, by compactness, we will end up with a model $w$ of ZFC as was present in the axiomatization in the question.