Recall the standard cartoon sketch of the proof of Gödel's first incompleteness theorem.
We start by defining a predicate, , that is true if and only if its argument is provable. (Or more accurately, is true if is the Gödel number of a provable proposition.)
With some quining we can use this to construct the proposition which says . The proposition asserts its own unprovability.
Suppose instead we define a predicate which holds if its argument is true.
We can use this to construct the proposition which says . Then if is true it must also be false and if it's false then it must be true.
We seem to have a paradox.
The loophole is that we assumed the existence of the predicate .
So this argument demonstrates that there is actually no such predicate. This is Tarski's undefinability theorem.
But what exactly stops us defining ? What goes wrong if we attempt to define a predicate that analyses the parts of a proposition to tell us whether or not it is true?
This article is written in English. But as is standard in much of mathematics, unless I state otherwise, I'm using English largely as shorthand for an argument that could, in principle, be written in the formal language of Set Theory. So I will allow myself to use all of the usual reasoning methods that are available in ZF, even when talking about other formal systems such as Peano Arithmetic.
Defining Truth for Propositional Calculus
Suppose we're given a proposition from propositional calculus like .
We can use a syntactic approach to determining whether or not it is true.
whether or not is true, then whether or not is true, and then the whole proposition
is true if both and are true.
Similarly is true if either or is true.
Of course and might themselves be compound propositions using , and .
But that's fine, that simply means that to define truth for such propositions
we need to employ recursion.
In fact, we can straightforwardly turn such a definition into a recursive computer program.
(Ultimately with propositional calculus we hit the leaves which are atomic propositions like . Typically when we ask about the truth of a proposition in propositional calculus we've already made an assignment of truth values to the atomic propositions. So the base case for the recursion is straightforward.)
We can illustrate the process with a diagram:
The truth value of a node in the tree is determined by the truth of the propositions hanging underneath it. We have a parent-child relation between a proposition and its subexpressions.
Recursion allows us to make a definition by defining what happens on the leaves of such a tree, and by saying how the definition at a node is built from that of its children.
Defining truth for Peano Arithmetic
We can go further and attempt this approach with Peano Arithmetic (PA).
The catch is that we need to consider quantifiers.
For example, consider this proposition from Peano arithmetic: . This proposition is true if and only if is true whatever number we substitute for in the expression.
The proposition at the top of the tree above is true if all of the immediate children are true and their truth is in turn determined by the truth of the propositions immediately below them.
With some work this eventually leads to a perfectly good definition of truth for propositions in PA.
Because we have nodes with infinitely many children we don't get an algorithm guaranteed to terminate, but that's not a problem for a definition in ZF.
Note that we don't literally prove the infinitely many child propositions one at a time.
Instead what happens is that to define the truth of we define it in terms of the truth of some infinite family of propositions all based on .
ZF is perfectly good at dealing with such definitions without us having to list every element of our family explicitly.
Note how in this case the tree isn't the parse tree of the proposition.
It's much bigger with nodes that have infinite branching.
But that's fine, there's nothing about infinite branching that prevents us
making a recursive definition.
So we can ultimately extend the idea for defining truth in propositional calculus to include quanifiers and then all of Peano arithmetic.
Defining truth for ZF
But the approach used for PA looks like it might work perfectly well for ZF as well. For example, our definition of truth would say that is true if is true whatever set we substitute for .
In ZF there is no difficulty in defining a predicate that uses quantification over all sets.
So it seems we can define for ZF in ZF, contradicting Tarski's theorem.
What went wrong?
Recursive definitions typically rely on the parent-child relation I mentioned above.
To recursively define something we (1) define it for all leaves
and then (2) specify how the definition at a parent is given in terms of the value for all of its children.
We then invoke a recursion theorem of some sort to show how this uniquely defines our object for everything in our universe.
For example, one form of recursion in Peano arithmetic has as its leaf and the only child of is .
The induction axiom for PA can be used to show that definitions using this parent-child relation are valid.
Similarly in ZF we have the empty set as leaf and the children of a set are simply its elements.
But now we need to look closely at the recursion principle we need.
For ZF we need to invoke the Transfinite Recursion Theorem.
Transfinite recursion is very powerful.
It's not just limited to induction over sets.
It can also be used for induction over classes.
For example if you need to recursively define a function on the class of all
sets it can allow this.
(Strictly speaking it'll be a function class rather than a function.)
But now comes the catch.
If you take a look at the Wikipedia article it mentions that the parent-child relation, , needs to be set-like (though as the article is currently written it's almost an afterthought).
For this theorem to apply we need the collection of children of a proposition to form a set.
But to prove the truth of a proposition with a quantifier at the front we need to prove something is true for all children where there is one child for each set.
This means the children don't form a set.
So we can't use transfinite recursion.
And this means the informal definition of truth I gave above can't be turned into a rigorous definition.
I think this issue is quite subtle.
It's really easy to say in English "this thing is true if that thing is true for all sets".
Such a sentence in isolation can often be turned into a rigorous proposition in ZF.
But if that sentence is part of a collection of sentences that refer to each other forming an attempt at a mutually recursive definition, you need to check precisely what parent-child relation you're using.
Thanks to Sridar Ramesh for making clear to me why the attempted definition of truth in ZF doesn't work. But I've probably made some mistakes above and they have nothing to do with Sridar.