Some musings on interpretations

(Originally posted to this logic mailing list I'm trying to get started. All are welcome! Except if you know nothing about logic and aren't willing to learn. Then you're not welcome. Sorry.)

An interpretation is a translation of a statement from one logic into
another. I was looking at interpretations recently because they appear
to be a way to show that semantically stronger logics (specifically,
logics formed by adding a truth predicate) really are stronger in
practice. The stronger logic can interpret the weaker, but the weaker
cannot interpret the stronger. (This is one type of proof-theoretic
strength.)

Normally, one does not allow just *any* interpretation... for example,
we wouldn't want a universal quantifier in the first logic to be
interpreted as an existential one in the new logic. It is typical (so
far as I have seen) to require the logical connectives to remain
unchanged, and only allow minimal changes to the quantifiers (such as
translating them to be restricted quantifiers).

Yet, all we care about is structure in these interpretations. For
example, if we're interpreting talk about numbers into a logic that
talks about sets, we don't really care if the resulting translated
sentences don't have anything to do with sizes of sets-- all we're
supposed to worry about is relationships. For example, our new
translated notion of "addition" should tell is that "5" and "6" makes
"11". (Usually when people do construct interpretations, of course,
they try to find ones that make some intuitive sense.)

So if all we care about is structure, why constrain the way logical
connectives and quantifiers are translated? What happens if we get rid
of these constraints?

Well... we can't get rid of *all* the constraints: we still need to
capture what we mean by "interpretation". Not every function from one
language to the other counts! The way I see it, we want to keep the
following minimal constraint:

C1: If A |- B in L1, then f(A) |- f(B) in L2

Where f(X) is the translation function, "X |- Y" means Y can be proven
from X, L1 is the language being translated, L2 is the language being
translated into, and A and B are statements in L1.

I've also thought of the following:

C2: A |- B in L1 if and only if f(A) |- f(B) in L2

But, that is not much like the standard notion of interpretation.
Essentially it means that the interpretation into L2 adds no extra
knowledge about the entities in L1. But, if we're looking for strong
languages, extra knowledge is a good thing (as long as it is true
knowledge). (One could argue that this justification doesn't apply if
we're only worrying about structure, though, I think. Specifically, of
when we say "structure" we mean not just structures of what's provable
but also structures of what isn't, we should take C2 as the proper
constraint. I'll proceed with C1 since it is the more standard-looking
constraint.)

Anyway. What now happens to the earlier assertion, that semantically
stronger languages are also proof-theoretically stronger, because they
can interpret more logics?

Answer: plain first-order logic can interpret any logic L with a
computable notion of provability.

Proof: Arbitrarily declare that some of the function symbols represent
the operations necessary to build up statements in L (for example, one
function might be chosen for each character in the alphabet of L, so
that composing those functions in a particular sequence would
represent writing down characters in that sequence). For an
L-statement X, call the first-order version of X built just from these
function symbols h(X). Write down some statements describing
L-provability. Writing down the rules of L like this is possible
because first-order logic is Turing-complete. Take the conjunction of
the statements about L and call it R (for "rules"). The interpretation
of an L-statement X will simply be R->h(X), where "->" is material
implication. This will satisfy C1 because wherever L proves A from B,
first-order logic will prove that if the rules of L-provability hold,
then A is L-provable from B. (This proof is still pretty messy, but
nonetheless I'm guessing I'm going into more detail here than needed,
so I'll leave it messy for now.)

What does this mean? To me this means that proof-theoretic strength is
not a very justifiable way of enticing people over to the side of
logics with strong semantics. First-order logic is in some sense
proof-theoretically all-powerful (if we allow arbitrary
interpretations, and if we're dealing with computable provability). If
someone is set in their path of using just first-order logic, I cannot
convince them just by talking about first-order truth; first-order
logic doesn't have a strong enough semantics to talk about first-order
truth, but they can interpret what I am saying by just listening to
the computable inference rules of my more-powerful logic. Every time I
say X, they can interpret me as meaning "The rules I've laid out imply
X". They will then be able to assert that first-order reasoning can
justify all the reasoning I'm doing, without even needing any new
axioms.

I'll then try to argue that I'm actually asserting X, not just
asserting that X follows from the rules I've laid out... but if
they're *really* applying the interpretation properly, they'll tell me
that I'm making a meaningless distinction, since they'll think
R->(R->h(X)) is the same as R->h(X). (If they make this reasoning
explicit, though, I have them: I can assert that I'm not saying
R->h(X), I'm saying h(X).)