I recently learned that ZFC can prove $Con(PA)$ because it can give a model of PA, but I'm not given the technical details. (My teacher thinks it is too obvious to even mention.) What plagues me is that my naïve intuition tells me that the modeling procedures can be imitated in PA, exactly in the same way.

Here is my attempt: Let $eval_F$ and $eval_T$ be evaluation functions for Formulas and Terms. Let $e$ denote any variable assignment. We can define these functions recursively, exploiting Tarski's lemma. Explicitly,

\begin{align} eval_T(\ulcorner v_i\urcorner,e) &= e[i] \\ eval_T(\ulcorner o\urcorner,e) &= 0 \\ eval_T(\ulcorner s\tau \urcorner,e) &=eval_T(\ulcorner\tau\urcorner,e)+1 \\ eval_T(\ulcorner \tau_1 + \tau_2 \urcorner,e) &=eval_T(\ulcorner\tau_1\urcorner,e)+eval_T(\ulcorner\tau_2\urcorner,e) \\ eval_T(\ulcorner \tau_1 \cdot \tau_2 \urcorner,e) &=eval_T(\ulcorner\tau_1\urcorner,e) \cdot eval_T(\ulcorner\tau_2\urcorner,e) \end{align}

and

\begin{align} eval_F(\ulcorner \bot \urcorner,e) &=0 \\ eval_F(\ulcorner \tau_1 = \tau_2 \urcorner,e) &= \chi_=(eval_T(\ulcorner\tau_1\urcorner,e),eval_T(\ulcorner\tau_2\urcorner,e)) \\ eval_F(\ulcorner \Phi\to\Psi \urcorner,e) &= \mathrm{sgn}((1-eval_F(\ulcorner \Phi \urcorner,e))+eval_F(\ulcorner \Psi \urcorner,e)) \\ eval_F(\ulcorner \forall v_i.\Phi \urcorner,e) &=\begin{cases} 1 & (\forall n.eval_F (\ulcorner\Phi\urcorner,e[i\mapsto n]) = 1) \\ 0 & (\mathrm{otherwise})\\ \end{cases} \end{align}

Then $eval_T$ and $eval_F$ are $\Sigma_1^0$- and $\Sigma_2^0$-defined function respectively. Although $eval_F$ is not decidable, at least we know that $eval_F$ is total over coded PA-formulas and the value is either $0$ or $1$. If we show that every axiom in PA evaluates to $1$ and the inference rules are truth-preserving, then we can show the soundness of the model: $$ \forall \phi:\mathrm{Form}. (Provable(\phi) \to \forall e. (eval_F(\phi,e)=1)) $$ If so, we can conclude $Con(PA)$, which is $\neg Provable(\ulcorner \bot \urcorner)$, because $\bot$ evaluates to $0$.

Of course, this violates Gödel's second incompleteness theorem, so I must be wrong somewhere - but I couldn't find where. I am now suspecting three possibilities:

- We cannot in fact well-define $eval_T$ and $eval_F$ in PA.
- We cannot prove that $eval_F$ models the axioms of PA.
- The inference rules does not preserve truth generated by $eval_F$.

I want to know where my argument fails. Thanks in advance.

P.S. The most suspicious one for me is the second one, especially induction scheme. Nonetheless I am convinced that induction scheme is provably evaluated to 1, since it reduces to \begin{align} \forall \phi:\mathrm{Form}.\forall e. &\forall i. \bigl( eval_F(\phi,e[i\mapsto 0])=1 \to \\ &\forall n. (eval_F(\phi,e[i\mapsto n])=1 \to eval_F(\phi,e[i\mapsto n+1])=1) \to \\ &\forall n. (eval_F(\phi,e[i\mapsto n])=1 )\bigr) \end{align}

which is an instance of induction scheme of outer PA.

formulasby recursion like you do like that. If you want to define a formula $A$, then you have to define using symbols which donotinvolve $A$ itself. The way this can be done in ZFC is by constructing not a singleformula$eval_F$, but rather aset, call it $e_F$, which contains all the formulas. Sets can be defined iteratively like that, and we can say that $e_F$ is the set which satsifies the inductive properties you list. $\endgroup$explicitizerecursively defined predicates or functions even in PA, without any notions about sets, is the significant result of metamathematics from Gödel's famous paper. $\endgroup$1more comment