The Context of Inference

Abstract

There is an ambiguity in the concept of deductive validity that went unnoticed until the middle of the twentieth century. Sometimes an inference rule is called valid because its conclusion is a theorem whenever its premises are. But often something different is meant: The rule's conclusion follows from its premises even in the presence of other assumptions. In many logical environments, these two definitions pick out the same rules. But other environments are context-sensitive, and in these environments the second notion is stronger. Sorting out this ambiguity has led to profound mathematical investigations with applications in complexity theory and computer science. The origins of this ambiguity and the history of its resolution deserve philosophical attention, because our understanding of logic stands to benefit from their details.

I am eager to examine together with you, Crito, whether this argument will appear in any way different to me in my present circumstances, or whether it remains the same, whether we are to abandon it or believe in it.—Plato Crito, 46d

Notes

1 See Hakli and Negri, 2012 for documentation of a remarkably sustained debate about the validity of the Deduction Theorem in certain modal logics that turned on just this point.

2 I have heard Anand Pillay, Julia Knight, Yuri Gurevich, and other prominent logicians describe the ‘real meaning’ of the completeness theorems in these terms, typically to emphasize their own computational or model theoretic approach to logic. Gurevich (1984) provides an early remark in this vein: ‘The calculus-independent meaning of this theorem is that first-order logic is recursively axiomatizable, which boils down to the fact that valid formulas are recursively enumerable’ (p. 179).

3 Frege 1917, pp. 16–17.

4 Frege 1923, p. 402.

5 Frege 1906, p. 318.

6 Frege 1918, p. 375.

7 Frege 1910, p. 82.

8 Brouwer 1928, p. 1181.

9 In his 2005, van Dalen observes that Brouwer once expressed gratitude that Heyting produced his calculus so that Brouwer did not have to do so himself (p. 676). Compare van Atten's observation (in his 2009) that Brouwer thought Heyting's axiomatization of ipc was more important than Gödel's incompleteness theorem.

10 The conclusion of this last sentence (Аксиома 5-ая употребляется только в символическом изложениилогики суждений, поэтому критика Brouwer’a не коснулась ее, тем не менее она также не имеетинтуитивных оснований) is mistranslated by van Heijenoort as ‘especially since it has no intuitive foundation either’, suggesting that Kolmogorov thought that the acceptability of the principle in part derives from its lack of an intuitive foundation! The sentence is better translated as ‘Axiom 5 is used in only the symbolic rendering of the logic of judgments; therefore, Brouwer's criticism does not apply to it. Nevertheless, it, too [i.e. like the law of double negation], does not have intuitive foundations’, expressing Kolmogorov's opinion that the principle could be used despite its lack of intuitive meaning. Thanks to Melissa Miller for verifying the translation.

11 Heyting 1956, p. 102.

12 These letters were brought to the author's attention by Tim van der Molen's analysis of them in his 2016. The reader is encouraged to consult that paper for further details.

13 In his first letter to Heyting, he focussed instead on the formula (.

14 Because they each put forward their logical systems as candidate formalizations of Brouwer's intuitionistic thought, it is anachronistic, in a discussion of the exchange between them, to refer to Johannson's system as ‘the minimal calculus’ and to Heyting's as ‘the intuitionistic calculus’. However, it is so standard nowadays to refer to Johannson's system, Heyting's system, and classical sentence logic respectively as mpc, ipc, and cpc, so that ipc = mpc + and cpc = mpc + = ipc + that for the sake of reference it makes sense to use these labels.

15 The disjunction property was proved for Heyting's intuitionistic calculus independently by Gödel (1932) and Gentzen. Gentzen's 1934 proof is an elegant consequence of the cut-elimination theorem for his sequent calculus presentation of intuitionistic logic and the one that Johansson adapts for his minimal calculus.

16 See Schroeder-Heister 2008, p. 217–18 for discussion of this point.

17 In a later section we will have occasion to observe more precise measures of the complexity of admissibility relative to derivability.

18 This rule was identified by Kreisel and Putnam (1957) as the characteristic axiom of a system that extends ipc but still has the disjunction property. Łukasiewicz (1952) had conjectured that the disjunction property characterizes ipc in the sense that it fails in any stronger logic. In light of Kriesel and Putnam's refutation of Łukasiewicz's conjecture and the association of the disjunction property with the BHK interpretation of intuitionistic logic, de Jongh (1968) indicated a related property that does so characterize ipc. Iemhoff (2001, p. 137), indicated another that is close to the heart of the present paper: ipc is the only intermediate logic with the disjunction property for which all the Visser rules are admissible (see Section 7.5).

19 This is not to say that the admissibility of Harrop's rule is in any sense equivalent to the disjunction property. Harrop's rule is derivable, and therefore admissible, in cpc, although the disjunction property obviously fails in cpc.

20 For Gentzen, these conditions provided the structural framework of the sequent calculus, with transitivity called ‘cut’, monotonicity called ‘thinning’, and reflexivity expressed as a condition on ‘initial formulas’. A detailed analysis of Gentzen's result and its relevance both to his unique conception of logic and to his more well-known logical achievements can be found in Franks 2010.

21 One also finds studies about consequence relations whose elements are, rather than formulas, sequents—a framework in which one can observe, depending on how one formulates the relevant calculi, that the cut rule is admissible but not derivable. A discussion of the several additional complexities presented by such a framework can be found in Iemhoff 2016. We consider only the simplest case of single-conclusion consequence relations, whose elements are formulas.

22 For an elegant exception, see Koslow 1992.

23 For precise definitions and a verification that this strategy works, see Iemhoff 2016, Proposition 3.6.

24 See, for example, Iemhoff 2016, Corollary 4.3.

25 See especially Rybakov 1997. Similarly Iemhoff 2016 remarks that whether or not a logic is structurally complete ‘depends very much on the particular consequence relation one uses for a logic’, whereas ‘admissibility solely depends on the [logic's] theorems’ which is invariant for all such consequence relations.

26 Koslow (1992) provides a full elaboration of this point of view, which is also implicit in the category-theoretic work on topoi in for example Lawvere 1964.

27 This theorem is an instance of Iemhoff's (2001) general observation that ipc is the maximal logic that both has the disjunction property and admits Visser's rules, but the direct verification of this particular instance is instructive. The customary label ‘kp’ used here refers to Kreisel and Putnam, whose 1957 featured the rule (see note 18).

28 The rules are named after Albert Visser who devised them and conjectured that they form a basis, over ipc, for ipc-admissibility. Iemhoff verified this in 2001.

29 This simple example was suggested by Rosalie Iemhoff, discussions with whom have been instructive and inspirational for many aspects of this project.

30 Terwijn 2004 provides a vivid history of these evasions.