(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.

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).)

## No comments:

## Post a Comment