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"?