Why can't we embed Tarski's truth in PA? 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.
 A: First-order logic does not provide for definitions of functions by recursion. For example, the transitive closure of a binary relation $R$, though definable from $R$ by recursion, is not in general first-order definable from $R$.
Peano Arithmetic, though formulated in first-order logic, does have enough axioms to support some definitions by recursion. Specifically, thanks to the availability in PA of sequence coding, a recursive definition can be reformulated as an explicit definition provided each step in the recursion depends on only finitely many previous results. For example, the natural definition of the factorial function ($0!=1$ and $(n+1)!=n!\cdot (n+1)$) can be rewritten as "$x!=y$ iff there is a sequence $a_0,a_1,\dots,a_x$ of length $x+1$ with $a_0=1$, $a_{n+1}=a_n\cdot(n+1)$ for all $n<x$, and $a_x=y$." This reformulation is expressible in PA because coding allows us to replace "there is a sequence" with "there is a number". But it's crucial here that all the "predecessors" of "$x!=y$" in this recursion can be coded into a single number, which requires that there be only finitely many of these predecessors. There's no way to code an infinite sequence of natural numbers into a single natural number.
In your recursive definition of $eval$, the clause for a universally quantified formula unfortunately involves infinitely many predecessors, namely the values for all the alternative assignments $e[i\mapsto n]$. This one clause prevents your recursion from being expressible in PA.
(Any extension of PA that would allow expressing this recursion  --- whether by adding more axioms or by strengthening the logic --- and allow proofs by induction of formulas containing such an expression would also prove the consistency of PA along the lines you indicated. So it's a good thing that PA can't express this recursion; if it could, then it would prove its own consistency and therefore would be inconsistent by Gödel's second incompleteness theorem.)
