Opiniatrety

Intelim Rules for Truth and Names

(If you didn't fall asleep during the post title, I'm taking that as license to be as technical as I wanna be.)

Gillian Russell considers the possibility that the truth predicate is like 'tonk' in that introducing it into the language makes it possible to derive contradictions. [tonkis the connective governed by the following rules: from P, you can deduce P tonk Q; from P tonk Q, you can infer Q.] Yet, given her intelim rules for the truth-predicate, 'true' has the local reduction property, so that any proof whose premises and conclusion don't contain 'true' can be normalized. (Background in these two posts of Gillian's; basically, local reduction means that if you use the result of the introduction rule as input to the elimination rule, you can get the same result without that introduction-elimination pair.)

I have a suggestion. Namely: When we introduce the truth-predicate, we have to do it in conjunction with an apparatus for naming propositions. Relatively intuitive intelim rules will then allow us to derive the liar paradox. But I'm not exactly clear on the relevance to the local reduction property.

First, a bit of handwaving about why we want different intelim rules than the ones Gillian has.

Gillian looks at "a truth predicate governed by simple disquotational rules like these ('T' is our truth predicate):

A
T(A) [TI]

T(A)
A [TE]

But at least on some views of quotation, this isn't actually disquotational, and our truth predicate shouldn't be a predicate of sentences. Take the view on which this expression, quotes included:

"Snow is white"

names this sentence:

Snow is white

which expresses the proposition that snow is white. On that view (which I don't think I believe, but which will support my handwaving), when we say

"Snow is white" is true

we're predicating truth of the sentence

Snow is white

rather than the proposition that snow is white. So we want our truth predicate to take as input expressions that name sentences--and we want our notation of the truth-predicate, 'T', to be followed by a bit of notation that denotes a name rather than a bit of notation that denotes a proposition.

In very short: T(n) rather than T(A).

And we need to be able to express the fact that a proposition has a name, which I will do with the following notation:

n: A

which means that A occurs at this step, and A has name n.

The intelim rules for the naming convention are simple. If you have a premise, you can give it any name you like, so long as the name isn't already in use; if you have a named premise, you can stop calling it that. (You can assume A merely in order to name it, if you like that sort of thing.)

A
n: A [nI]

so long as n has not already been used in a previous step of the proof.

n: A
A [nE]

Now, I'm going to make the intelim rules for the truth predicate very strong. I could probably make them weaker, but the very strong rules will make it easy to derive the things I want.

n: A
φ(A)
φ(T(n)) [TI]

where--I'm not sure how to show this--the conclusion is under the scope of the same assumptions as φ(A), but not necessarily as n: A.

(Turns out I don't actually need the φ business, but I'm going to leave it in anyway.)

What this means, basically, is that if n names A, you can drop T(n) into a formula in place of A. If Fred is the name for "Snow is white," you can replace "Snow is white" with "Fred is true." "If snow is white then grass is green" becomes "If Fred is true then grass is green."

Elimination rule is the same in reverse:

n: A
φ(T(n))
φ(A)[TE]

with, again, the conclusion under the same assumptions as the second line, but not necessarily the first.

This will let you derive bits of the Liar Paradox like so (the assumption a line is under is in square brackets at the end of the line):

1 ~T(n) Assp [~T(n)]
2 n: ~T(n) nI 1 [~T(n)]
3 T(n) TI 2,2 [~T(n)]

4 ~T(n) Assp [~T(n)]
5 n: ~T(n) nI 4 [~T(n)]
6 T(n) Assp [T(n)]
7 ~T(n) TE 5, 6 [T(n)]

So we've derived ~T(n) from T(n) and vice versa. This is good enough for a paradox. And it should let us derive Q from P for any P, Q, by a process I don't have the nous to type up right now.

But these proofs don't show anything in particular about the local reduction property. For one thing, the premises and conclusions both involve T and n, so these proofs are in principle unnormalizable. For another thing, they don't involve any lines that are product of an I rule and input to an E rule for the same sign (or vice versa); 2 is the product of nI and the input to TI, whereas 5 is the product of nI and the input to TE. For a third thing, negation is involved here, and negation itself violates the local reduction property.

One thing is that these properties are sensitive to the way the intelim rules are formulated. And I probably formulated my rules in an eccentric fashion. But I offer these rules up as a contribution to the discussion, anywise.

Posted by Matt Weiner at April 5, 2005 01:56 PM