Recall the standard cartoon sketch of the proof of Gödel's first incompleteness theorem. We start by defining a predicate,
Suppose instead we define a predicate
But what exactly stops us defining
Note
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
(Ultimately with propositional calculus we hit the leaves which are atomic propositions like
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:

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
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
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
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,
Conclusion
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.
Acknowledgement
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.
This is a very good explanation, I've never been able to even coherently ask the question of how truth is defined in math. I stopped at the incompleteness theorem when I learned that Provable=>True, but not necessarily the converse.
ReplyDeleteTo see how recursion works here, or rather it does not, it is interesting to consider a truth predicate for a limited collection of formulas. For instance, suppose we want to define the truth predicate for all formulas in which there are at most n occurrences of the quantifiers, for some fixed n. Then this can be done (because no recursion is needed). So we can in fact have a collection of truth predicates which cover all formulas, but there is no way to put them together into a single one.
ReplyDeleteAndrej, yes, "there is no way to put them together into a single one" is usually the problem stopping us, ok, that was the premise already, no?
ReplyDeleteI'd say that its an unrecognized problem of domains, ontology and unstable/foldable coordinate systems that stops our descent here.
Whatever the input, both Alice and Box have a 0.5 chance ...
ReplyDeletePresumably you meant "Bob"? :)
FZ I guess that comment was intended for the next post.
ReplyDelete