Maximally Structured Theory

The proof-theoretic concept of a theory's "strength" has little to do with the sorts of considerations in the previous two posts. Proof theory normally worries about how much a system proves, while I've been worried about how much a system can say.

The sort of proof-theoretic strength I've read about (I admit there are at least two, and I don't know much about the other one, known as ordinal strength) is defined in terms of interpretations. One system can be interpreted in another if, roughly, we can "translate" the provable statements in one into provable statements in the other, and the translation preserves the basic logical operators (so and -> and, or -> or...). There is no requirement that the translation of an unprovable statement be likewise unprovable, which means that the logic we're translating into may add more provable statements. This is, of course, the point: of two systems A and B, B is stronger than A if B interprets A but A does not interpret B. This indicates that B proves more statements than A.

Now suppose that system C is also stronger than A. It may be the case that system C is not comparable to system B: neither can interpret the other, so there is no way to say that one is more powerful than another. We can think of this as a disagreement between the two systems; both prove more than A proves, but B might prove some statement where C instead proves the negation of that statement.

Is one system right and the other system wrong? Well, if both systems are supposed to be talking about the same mathematical entity, then yes. (Or they could both be wrong!) But if not, we can instead think of the different systems as describing separate mathematical entities. It is then natural (in my opinion) to assert that the proper foundation of mathematics should interpret both. This would mean that it contained both structures within it.

I am somewhat surprised that this is not the current approach. Instead, people seem to be concerned with whether or not the axiom of choice is actually true or not. I suppose this is my first deviation from the classical 'platonist' view :).

So, suppose we restrict ourselves to finite first-order theories. How much structure do we get?

First, just because we restrict ourselves to finite theories doesn't mean we can't interpret an infinite theory. Peano arithmetic, which I've been talking about for the last two posts, is a perfect example; it has an infinite number of axioms, but they are computably enumerable, so we can create an axiom system that enumerates them by allowing the use of extra function symbols.

Second, we can interpret far more than first-order theories; higher-order theories can be interpreted as first-order theories with restricted quantifiers.

What we can't interpret is a fundamentally infinite theory, such as... well, the truths of arithmetic. No finite theory will interpret the infinite theory containing all those truths. (Notice, now I'm being Platonist, and claiming that there actually is a fact of the matter.)

What will the maximal theory look like, the theory that can interpret any others? Will it be finite?

Let's first construct an infinite theory that interprets all finite theories. We can't interpret inconsistent theories without being inconsistent, so let's throw those out... then, we enumerate all the consistent theories (in order of size, let's say, using some other rule to break ties), but using a new set of function symbols for each theory, so that they don't interfere with eachother. (Each finite theory can only use a finite set of function symbols, so there is no trouble here.) Using different function symbols allows us to simply take the union, forming an infinite theory.

This infinite theory cannot be converted into a finite form, unfortunately, because the enumeration is not computable: we can't simply distinguish between theories that are consistent and theories that are not.

Now... if we take a logic wich lacks the rule of explosion, ie, a paraconsistent logic, we wouldn't need to worry so much about avoiding inconsistent theories. The inconsistent theories would be isolated, and wouldn't "infect" the others. In this case we could computably enumerate all theories (still making sure to take different function names for each), and therefore we could make a finite theory which performed the enumeration. (The finite theory would use only a finite number of function symbols, but it would provide an interpretation for an infinite number of them, via some encoding.)

This provides an interesting argument in favor of paraconsistent logic. But, not necessarily a definitive one. It seems to me that one could claim that the paraconsistent logic is not really interpreting the classical theories, since it is putting them into a logic with a nonclassical semantics. Perhaps one could define what the paraconsistent logic is really doing, and construct a classical theory that does that much. I don't know.

[edit]
postscript--

Don't think that it ends here, with one infinite (unspecifiable) theory to rule over all finite theories. We can talk about other such infinite theories, such as the theory containing all the truths of first-order arithmetc, the theory containing all the truths of second-order arithmetic, et cetera, the truths of set theory... (Actually, I don't think just "the truths of set theory" is well specified. "The truths of set theory under the iterative conception of set" is one way of being more specific.) So, we'll want to talk about whether these infinite theories can interpret eachother, and hence we'll have an increasing chain of "maximally structured" systems with respect to particular reference sets... the maximally structured theory with respect to finite theories is countably infinite; so is the set of truths of first-order arithmetic; the max. struct. theory w.r.t countably infinite theories will be uncountably infinite; and so it goes.

Alternatively, the paraconsistant version of this hierarchy appears to stop right away, with a finite theory that interprets all finite theories. This might be taken as a strength or a weakness...