We begin with the observation that 2nd-order logic is ridiculously powerful. It turns out that we can embed higher-order logic within 2nd-order logic:
Thus the set of validities of seventeenth-order logic is computably reducible to V²(=), the set of second-order validities in the language of equality. (In fact, these two sets are computably isomorphic.) So in this aspect, the complexity of higher-order logic does not increase with the order. (Stanford Encyclopedia)
If we could agree on a semantics for set theory, we could probably embed that into 2nd-order logic too, following an approach similar to NBG set theory. (For example, we could formalize the iterative conception of set as construed by Boolos; though, we could not formalize the iterative conception as originally described by Goedel... that subject would be worthy of its own post.)
In short, if 2nd-order logic is referentially incomplete, it's not obvious how. Whereas with a theory of truth, you have the feeling of an immediate gap (something which you used to describe the system but don't seem to be able to discuss within the system), 2nd-order logic seems capable of discussing anything we can think of. Sure, we know that undefinability must still apply: 2nd-order logic can't define its own truth predicate. Bear with me, though. It would still be nice to have a theory of truth with expressive power similar to 2nd-order logic. Most theories of truth can't compete, because 2nd-order logic requires impredicative comprehension.
So, how might we go about that?
First, we need to talk about "satisfaction" rather than truth. We can render the application of a predicate to a first-order entity P(x) as Sat("P(_)",x). Like the truth predicate, the satisfaction relation takes sentences in quoted form; that is, it takes Goedel numbers, or (probably) some more convenient representation of the syntax of the sentence. However, it takes the 1st-order variables directly, rather than quoted.
This allows us to keep 2nd-order variables (which range over syntactic representations) separate from 1st-order variables (which range over actual entities). This is a type distinction: quoted representations are not first-order entities, and are not allowed to occur in the right-hand side of the satisfaction relation. Separate quantifiers range over the two types of variables.
Notice that there needs to be a way of detailing a "blank", "_", which the first-order entity gets substituted in. We will also want to work with multiple blanks, to represent relations, but we can introduce lists as 1st-order entities to avoid the need... there are details to work out here.
We give the language enough tools to build up complex expressions to discuss the satisfaction of; similar to this excellent post. So, for example, we provide a negation function which returns the compliment of a 2nd-order entity, a conjunction function which returns the intersection, disjunction which returns the union, and so on for all the elements of our syntax. (It does not matter too much whether we provide these as functions or as existence axioms.) Critically, this includes a quotation function which takes the 2nd-order entity corresponding to an expression in the language and returns a 2nd-order entity corresponding to the 2nd-order entity corresponding to the expression. In other words, the function takes quoted entities and returns doubly quoted entities. This allows us to talk about quotation within the quoted portion of the language. That's critical to the impredicative self-reference.
In any case, True("S") is simply a special case of satisfaction. One plausible definition would be that S is true iff All x: Sat("S",x). (We may want to be a bit stricter, requiring that S has no free variables; whether we are able to require this will depend on some details of the logic.)
Wait. What happened? Didn't I say just a few paragraphs ago that 2nd-order logic can't define its own truth predicate? And now we're looking at a truth predicate as a special case of the 2nd-order satisfaction predicate?
The trick is that undefinability applies to a truth predicate at the level of first-order entities, because 2nd-order logic is strong enough to satisfy the diagonal lemma with respect to predicates on first-order entities.[citation needed] However, at the 2nd-order level, the logic is nowhere near that strong. So, we can put a self-referential truth predicate at that level without the problem.
In what sense is this a "self-referential" truth predicate? In the sense that it is a truth predicate which exists within the language it predicates on. We can assert or deny the truth of any sentence, including those which use the truth predicate.
It is not a self-referential truth predicate in the sense provided by the diagonal lemma: we can't construct self-referential sentences like the Liar sentence. This might make the theory sound a little boring, but it seems practical.
Besides: we get to have our cake and eat it too. With this approach, we are defining a sensible truth predicate by giving up the diagonal lemma at the 2nd-order level; yet, when talking about first-order entities, we still get the benefit of a strong language. We don't have to give up logical power after all!
Still, it is tempting to reach for a little more. As described, the 2nd level of the language is very weak. However, all I need is that it doesn't satisfy the diagonal lemma. Might it be possible for the 2nd level to be a self-verifying logic? Because... that would be awesome.
This post may or may not conclude the short series on this theory of truth. I have definitely not done it justice. I would like to formalize it properly, read up on Fregean studies to see how similar this is, read more background material about the diagonal lemma and 2nd-order logic to make sure I'm not just crazy here, read up on self-verifying logics, and so on. However, I don't really have the time to dive into this. So, there may not be any more posts on the topic for a while.
Update: next in the sequence is here.
