Compactness and Arithmetic Confusion

Question

Let $T$ be some theory capable of arithmetic and construct a provability predicate (which we will call $Prb_T$). Let $\mathbb{N} \models T$. Expand our language to include a new constant symbol $c$. Define $$\varphi_n \equiv (S^n(0)<c) \wedge (Prb_{T}(c))$$ Let $\Phi = \bigcup_{n\in \mathbb{N}}\varphi_n$. Clearly, $\Phi \cup T$ is finitely satisfiable and so there exists $\mathbb{M}$ such that $\mathbb{M} \models \Phi \cup T$. Now, my question is, what exactly does $Prb_T(c)$ mean when $c$ is a non-standard natural number? Is $c$ the Gödel number of some non-standard formula? An infinitary sentence? What are some standard interpretations for $Prv_T(c)$.

Answer 1

Recall that provability predicate are not "really" what you have expect them to be, just almost. It really just says that there is a number which encodes a proof sequence from statements which satisfy the condition "axiom of $T$" using particular inferences rules.

This extends to non-standard models as well, only now the condition "axiom of $T$" as well the number of free variables in the language, as well the length of the proofs, are all different.

$T$ is a theory in the abstract, meta-theory, at least when we think about things like $\sf ZFC$ or $\sf PA$ or whatever. But $Prb_T$ is a formula $\varphi(x)$ which states that there is a code for a proof from statements which satisfy some predicate defined by $\psi_T(x)$.

In a non-standard model, you are likely to have non-standard integers satisfying $\psi_T$, so now $T$ is interpreted as a theory with new axioms. Non-standard axioms. This means that we can really prove "more" in this model.

Now $c$ is a non-standard integer, this means that it encodes a statement which is non-standard (well, under reasonable assumptions anyway, that standard integers are closed under the basic encoding process). The proof of $c$ might be of non-standard length, or it might use non-standard axioms, or both.

But in either case it is important to remember that the internal interpretation of $T$ probably includes non-standard integers. So $c$ might be in fact an axiom from $T$, or it might be a statement whose proof has non-standard length.

Some examples:

1. $c$ could be code of a tautology, for example $\exists x_d(x_d=x_d)$ where $d$ is a non-standard integer.
2. $c$ could be a code of a new axiom from $T$.
3. $c$ could be a code just a non-standardly long conjunction of a standard axiom.