How can arithmetic express claims of the form $\Sigma \vdash \sigma$ when $\Sigma$ is infinite?

Question

As an example, let $\Sigma$ denote the axioms of ZFC (an infinite set). It is my understanding that the language of arithmetic can be used to express claims of the form $$\Sigma \vdash \sigma$$

where $\vdash$ denotes first-order deducibility. Given that $\Sigma$ is infinite, how is this actually done?

Note that I am not claiming that: "since arithmetic is about finite entities, this cannot be done."

Answer 1

We can do that using Gödel numbering. The language of set theory only has one binary relation, and no constants or function symbols. So Gödel numbering is quite simple.

It's not hard to show that the encoding of the schema of replacement is recursive. We can identify whenever $n=\#\varphi$ and therefore we can recognize when an integer encodes the replacement axiom for $\varphi$.

So the Gödel numbers of $\Sigma$ is a recursive set. Now we can talk about sequences of numbers in a recursive fashion, and we can ask when $k$ encodes a finite sequence of sentences which are a proof-sequence (i.e. each number encodes either an axiom from $\Sigma$ or something which was deduced from previous steps using modus ponens, or other previously agreed upon inference rules). Therefore the relation $\operatorname{Pr}(n,k)$ which states that $n=\#\varphi$ and $k$ encodes a proof sequence for $\varphi$ from $\Sigma$ is recursive.

Therefore the statement $\Sigma\vdash\sigma$ is really just saying that there exists a proof sequence whose initial axioms are from $\Sigma$ and its last point is $\sigma$. All in all, this relation is recursively enumerable, as the statement is $\exists k\operatorname{Pr}(\#\sigma,k)$.

Answer 2

The infinitude of $\Sigma$ comes from the Axiom Schemas of Replacement and Comprehension, so one has to look into the recursive nature of predicates and formulas. So fortunately $\Sigma$ is not an arbitrary infinite set, but it is recursively enumerable using a finite set of rules. And as such it is possible to express "$\phi$ is an axiom of ZFC" (or rather "$n$ is the Gödel number of an axiom of ZFC") in essentially the same way as "$n$ is a prime number" or "$n$ is a power of $10$" are representable.