Why isn't this a truth predicate? According to Tarski's undefinability theorem, there is no arithmetical formula that defines truth in arithmetic (i.e., there is no predicate $T$ such that $g \iff T("g")$).
I will know define a predicate $T$, which appears to be a truth predicate. My question will be, how does it fail?
I will consider arithmetic formulas involving the $\lor, \lnot, \exists, =, +, *, -, S$ (the $S$, $+$, and $*$ will be considered relations instead of functions).
$F(s,v)$ is a function on two variables, where $s$ is a formula, and $v$ is variable assignments, defined as follows, recursively:


*

*If $s$ is a disjunction of the form $A \lor B$, and then $F(s)=1$ if $F(A,v)=1$ or $F(B,v)=1$. Otherwise $F(s)=0$

*If $s$ is a negation of the form $\lnot A$, then $F(s,v)=1-F(A,v)$

*If $s$ is an existential statement of the form $\exists x.A$, then $F(s,v)=1$, if there is an number $n$ such that $F(A,v')=1$, where $v'$ is $v$ with the added assignment that $x=n$. Otherwise $F(s,v)=0$.

*If $s$ is a statement of the form $x=y$, $S(x,y)$, $+(x,y,z)$, $*(x,y,z)$, then $F(s,v)=1$ if the respective statements are true using the variable assignments from $v$. Otherwise $F(s,v)=0$.


This function is well defined, since the length of formulas are finite.
Then a statement $s$ is true if $F(s,e)=1$, where $e$ is no free variable assignments, and $s$ is false otherwise. My question is, what doesn't this define a truth predicate? It appears to satisfy Tarski's definition of truth.
I tried applying Tarski's theorem directly to this predicate, simplifying it until I found the error, but this would've resulted in a huge statement (since it would involve Goedel numbering) and would be very hard to simplify by hand. Is there any simpler way to find the error in $T$?
 A: Your proposed definition cannot be carried out in the first-order language of arithmetic.  Recall that we can recursively define a function $G:\mathbb{N}\to\mathbb{N}$ by saying $G(n)$ is the unique $m$ such that there exists a finite sequence $(a_0,\dots,a_n)$ of length $n$ satisfying the desired recursion with $m=a_n$.  We can do this in the language of arithmetic since finite sequences of natural numbers can be encoded using single natural numbers using Gödel's beta function.
However, in your case, you are defining not just a sequence of numbers but a sequence of functions.  That is, each $a_i$ in the sequence $(a_0,\dots,a_n)$ for your recursion needs to be an entire function $v\mapsto F(s_i,v)$ which sends a variable assigment to the truth value of the $i$th formula $s_i$ under that variable assigment.  You really need this entire function and not just finitely many values of it, since for your recursion in the case that $s$ is $\exists x.A$ you need to use the values of $F(A,v')$ for all appropriate choices of $v'$.  So in order to recursively define your $F$, you would need to quantify over functions on the natural numbers and not just individual natural numbers.
