Sunday, 1 May 2011

Roy's Fortnightly Puzzle: Volume 1

Intuitionism and "Unless"

Anyone who has taught an introductory logic course will be familiar with the difficulties students have regarding how to properly translate "unless" into propositional logic. The correct translation of "F unless G" is:

T1. F v G

(Athough it is surprising how many supposedly professional logic teachers get this wrong). We often motivate this translation in terms of various inferences we make with "unless", taking advantage of the fact that T1 is logically equivalent to both:

T2. ~ F -> G
T3. ~ G -> F

in classical logic. By DeMorgans, the disjunctive translation of "unless' is also classically equivalent to:

T4. ~ (~ F & ~ G)

Now, here is the puzzle: How should the intuitionistic logician translate "F unless G"? Note that each of the four options is intuitionistically distinct from the other three.

The initial temptation to go with the simplest (and 'strongest') translation (T1) conflicts with the thought that the "un" in "unless" suggests the presence of negation. A more sophisticated approach is to examine inferences that intuitionists make with "unless" and determine which translation is supported. Now, all four translations support the following inferences:

I1a. F unless G, not-F, therefore not-not-G.
I2a. F unless G, not-G, therefore not-not-F.

The question then becomes whether "unless" intuitionistically supports the following stronger inference rules:

I1b. F unless G, not-F, therefore G.
I2b. F unless G, not-G, therefore F.

T1 supports both inferences, T2 supports I1b but not I2b, T3 supports I2b but not I1b, and T4 supports neither I1b nor I2b.

So, how should intuitionists translate "unless"?

1. My two thoughts on "unless":

- The following inference seems reasonable: "F unless G, G: so not-F". So that suggests that FvG is not the right formalisation. "A wins unless B scores 10 points, B scores 10 points: so A doesn't win"

- "F unless G" also seems to be saying something different to "G unless F" which again suggests FvG is faulty.

Have I missed something?

2. Quick thoughts.
- Your first comment (taken alone) seems to suggest that "A unless B" should be translated as exclusive disjunction. But "A unless B" does, in general, seem to be consistent with both A and B being true. For example, telling a class that "You will pass the exam, unless you don't study" is compatible with the existence of the clever kid who passes but doesn't study.

- Of course, it might be the case that some instances of "A unless B" behave something like exclusive or (and presumably context would decide this). I don't know of any convincing examples (exclusive or is rather rare in and of itself in natural language). Even so, the same general worry arise. Do we translate "A unless B' as:

T1*: (A v B) & ~ (A & B)
T2*: ( ~ A -> B) & ~ (A & B)
T3*: (~ B -> A) & ~ (A & B)
T4*: ~ ( ~ A & ~ B) & ~ (A & B)

The same issues arise.

- The second thought seems different from the first, and it might not be relevant. "A unless B" does seem to say something subtly different from "B unless A", but the difference could be more like the difference between "A and B" and "A yet B" which are both correctly translated as "A & B".

3. After some thought, I was a bit too quick to dismiss Seamus' second thought. This subtle difference between "A unless B" and "B unless A" could be merely the sort of non-synonymy that is (and ought to be) 'smoothed out' in the translation from natural language to formal language (along the same lines as the fact that "and" and "yet" are non-synonymous but both get translated as "&"). But it could also, within the intuitionistic context, be taken as evidence that the proper translation of "F unless G" is one of:

T2: ~ F -> G
T3: ~ G -> F

This would have a very interesting consequence, however: The intuitionist, unlike the classical logician, would fail to accept the commutativity of "unless"! That seems like kind of a big deal.

4. Maybe it depends on whether one should accept *introduction* rules of the form:

(R1) from A infer "A unless B"
(R2) from B, infer "A unless B".

E.g., the argument,

(P) Snow is white
---------
(C) Snow is white unless grass is purple

is valid if "unless" is formalized as "or", but it seems a bit weird!

5. I'd tend to interpret "F unless G" as shorthand for "if ~G then F" and go with T3.

The borderline case is when we have

~F & ~~G

but we don't have G. That is, (in the BHK interpretation), we know how to reduce any proof of F to a contradiction, and we know how to reduce any proof of ~G to a contradiction, but we don't know how to prove G itself.

I'd say that fits with "F unless G" being true, but it doesn't fit with T1: if we know how to prove ~F and we know how to prove (F v G), then we know how to prove G: intuitionistically (F v G) -> (~F -> G).

6. Jeff,

Actually, all four of the translations I suggested will support both introduction rules. So I suspect that we would be better off testing various elimination rules.

7. Hi Roy, right, classically; but intuitionism rejects the inference to F v G from ~G -> F. So, maybe, for the intuitionist, "F, unless G" should be translated as the weaker ~G -> F?
That's your (T3) - which is how I translate "F, unless G" in my logic teaching!

8. Jeff,

Sorry, I am still not seeing the point. Regardless of whether we translate A unless B as (T1), (T2), (T3), or (T4), we will get:

A, therefore A unless B.
B, therefore A unless B.

Am I missing something? If not, then those rules don't give us any reason to prefer a weaker to a stronger reading.

The elimination rules, however, might. Would the following inference be valid for an intuitionist?

A entails C, B entails C. A unless B. Therefore C.

If (T1), then this inference should be fine. If we pick your preferred (T3), then the best we get is:

A entails C, B entails C, A unless B. Therefore ~ ~ C.

Also, some of those translations, but not others, support the analogues of disjunctive syllogism rules:

A unless B, not A, therefore B (T1, T2)
A unless B, not B, therefore A (T1, T3)

9. Roy, yes, you're right. I'm not thinking straight!

It must be the elimination rule. What's I think is happening is that there's some sort of conditional built in to "unless". I think the two competitors to translate "F unless G" are:

(T3): ~G -> F
(T1): F v G

Suppose introduction rules are:

(U-Intro-R) F implies "F unless G"
(U-Intro-L) G implies "F unless G"

And the elimination rule is:

(U-Elim): {F -> A, G -> A, F unless G} implies A

I think these fix "F unless" to be interderivable with "F v G" which is (T1) (classically equivalent to (T3)). Is that right? But, as you say, any of the translations supports the two introduction rules intuitionistically, it must be (U-Elim) that's disputed.

Maybe the rules should be set up analogously to a conditional (like Modus Ponens and CP),

U-Elim*: {"F unless G", ~G} implies F
U-Intro*: If D, ~G implies F, then D implies "F unless G".

I think this will then make "F unless G" intuitionisitcally interderivable with "~G -> F".

10. Your rules do give the interderivability. But I wonder if these rules are 'right' for "unless" (I'm just not sure). Is it possible that an intuitionist might accept:

U-Intro*2: If D, ~F implies G, then D implies "F unless G"

If so, then the translation of F could be something like:

(~ F -> G) v (~ G -> F)

which is weaker than your translation.

There are, of course, lots of other non-equivalent possible translations we haven't considered, including:

"F unless G" is ( ~ G -> F) & (~ F -> G)

or:

"F unless G" is ( ~ ~ F v ~ ~ G)

Both of these are stronger than your preferred translation, but weaker than F v G. I find the latter of these implausibly strong (for the same reasons I find F v G implausibly strong as a translation of "unless"). The nice thing about the former is that it retains the commutativity of "unless" while not entailing that (to speak loosely in a classical metatheory for a moment) "F unless G" entails that one of ~ ~ F or ~ ~ G is true (and we can know which).

11. Hi Jeff and Roy, just discovered this blog!

I agree with angelweed and Jeff that 'F unless G' is most naturally heard as 'F if not-G'. Of course if everything is classical and 'if' is material, this is equivalent to 'F or G', but this equivalence inherits the problems of the material conditional (eg 'F unless grass is green' is true for arbitrary F).

In cases where the conditional clearly is not material, eg subjunctives, the 'not-if' treatment seems right - eg

Someone else would have shot Kennedy, unless Oswald had done so

seems equiv to

If Oswald had not shot Kennedy, someone else would have done

but not to either the disjunction or the contraposition of the conditional.

All this suggests that (T3) is the right way to go.

On the other hand, I've been thinking about the case where F is ~G. If (T3) is right, then an intuitionist ought to hear

~G unless G

as logically true, but

G unless ~G

as not logically true. But I confess I have some trouble hearing them that way; there seems some pull to hearing neither of them as intuitionistic logical truths, which would be right if 'unless' is 'or' after all (or if Roy's penultimate suggestion is correct)...hmmm, not sure what I think now.

12. Actually, I think Adam's acute observation might be evidence in favor of my:

"F unless G" = (~ F -> G) & (~ G -> F)

translation. This makes "G unless ~ G" equivalent to " ~ G unless G", which are then both equivalent to:

~ ~ G -> G

Not a logical truth, but also not as strong as:

G v ~ G.

This seems roughly right: an intuitionistic assertion of "G unless ~ G" does seem like it shouldn't be a logical truth, but should be weaker than "G v ~ G"

13. Hi Adam, good to hear from you.
Roy, your conjunctive translation would nicely satisfy an equivalence test:

"F unless G" is equivalent to "G unless F".

which makes "unless" commutative.
I wonder if it works with Adam's counterfactuals though:

(i) Someone would have shot Kennedy, unless Oswald had.
(ii) Oswald would have shot Kennedy, unless someone else had.

Or maybe there's something funny going on when we go subjunctive - it suggests some kind of contraposition for counterfactuals - which isn't right.