Strategies of inquiry

Abstract

This paper examines critically the reconstruction of the ‘Sherlock Holmes sense of deduction’ proposed jointly by M.B. Hintikka (1939–1987) and J. Hintikka (1929–2016) in the 1980s, and its successor, the interrogative model of inquiry (imi) developed by J. Hintikka and his collaborators in the 1990s. The Hintikkas’ model explicitly used game theory in order to formalize a naturalistic approach to inquiry, but the imi abandoned both the game-theoretic formalism, and the naturalistic approach. It is argued that the latter better supports the claim that the imi provides a ‘logic of discovery’, and safeguards its empirical adequacy. Technical changes necessary to this interpretation are presented, and examples are discussed, both formal and informal, that are better analyzed when these changes are in place. The informal examples are borrowed from Conan Doyle’s The Case of Silver Blaze, a favorite of M.B. and J. Hintikka.

1 Introduction

In the 1920s, Popper (1959) and Reichenbach (1938) converged to the view that hypothesis making involves a psychological element that eludes rational reconstruction, formal or informal. Thus, in spite of their disagreement on the ‘logic of justification’ (deductive logic for Popper, probabilistic for Reichenbach), they agreed that there could be no ‘logic of discovery’. This view was opposed, in the 1950s, by Hanson, who maintained that “[if] establishing an hypothesis through its predictions has a logic, so has the conceiving of an hypothesis” (Hanson 1958, p. 71). But Hanson did not articulate a formal proposal, and his informal analysis was not received as a sufficient rebuttal to the Popper–Reichenbach view. Without stronger contender, the latter became the standard view of scientific inquiry among epistemologists and philosophers of science.

In the 1980s M.B. and J. Hintikka revived an early modern view of inquiry, first articulated by F. Bacon in his Novum Organum, and later defended by I. Kant in his Critique of Pure Reason. According to Bacon and Kant, inquiry is a process where an inquirer actively puts questions to Nature, not only to test conjectures, but also to make new ones. The Hintikkas proposed to capture inquiry as a two-player game between Nature and Inquirer, and emphasized the strategic role of logical reasoning, formally reconstructing the “Sherlock Holmes sense of deduction” (Hintikka and Hintikka 1983). They laid down logical foundations for their model and specified constraints on Inquirer’s strategies resulting from bounded cognitive resources (memory Hintikka and Hintikka 1983; attention Hintikka and Hintikka 1989). As the interrogative model of inquiry (hereafter imi), the model received its final form in the late 1990s, a decade after M.B. Hintikka’s demise, when Hintikka et al. (1999) characterized interrogative reasoning with the resources of the meta-theory of standard first-order logic alone. By their own admission, their results were straightforward consequences of elementary meta-theorems, but they argued that the results were conceptually fruitful, offering a strategic viewpoint on logical reasoning, and a basis for a logic of discovery.

This claim is disputable. Hintikka, Halonen and Mutanen have made formally precise arguments the Hintikkas had merely sketched, but their formalization has streamlined those arguments, leaving out the explicit cognitive interpretation of the original model. And yet, the parameters that reflected the naturalistic interpretation of the ‘Sherlock Holmes sense of deduction’ still play an implicit role in the imi. I will argue that the imi can benefit from making them explicit again. Section 2 presents the Hintikkas’ logical approach (Sect. 2.1), its game-theoretic treatment (Sect. 2.2), and some logical issues (Sect. 2.3). Section 3 shows how they were solved (Sect. 3.1), and how the informal approach to strategies superseded the earlier formal treatment (Sects. 3.2, 3.3). Section 4 discusses implicit assumptions underlying the results presented by Hintikka, Halonen and Mutanen (Sect. 4.1), how to make them explicit (Sect. 4.2), and how they relate to other formal models of discovery (Sect. 4.3). Section 5 provides an illustration with The Case of Silver Blaze, a favorite of the Hintikkas (Sect. 5.1), and returns to the naturalistic approach in the light of recent advances in the psychology of creative thought (Sect. 5.2). I conclude in favor of a modest revision of the imi. An appendix presents alternative proofs for the results discussed in the paper.

2 The ‘Sherlock Holmes sense of deduction’

2.1 Beth tableaux, deduction, and analysis

As logical foundations for their model of the ‘Sherlock Holmes of deduction’, the Hintikkas proposed a game-theoretic and naturalistic interpretation of a semantic proof procedure (Beth tableaux), extended to represent the posing of questions. The choice of Beth tableaux is more than a convenience:

Our use of Beth’s tableaux is in keeping with the best tradition of Sherlock Holmes, who speaks in connection with his “Science of Deduction” of analysis. As Beth pointed out in his very first paper on the subject, the tableau method is an excellent reconstruction of the old idea of analytical method. [...] What we are doing here can be thought of as an extension of Beth “Science of Deduction and Analysis” beyond its narrowly deductive applications. (Hintikka and Hintikka 1983, p. 166)

Beth tableaux formally capture semantic entailment between a premise set and a conclusion. Given a first-order language $\mathscr {L}$, a countable (possibly empty) premise set ${\varGamma }\subseteq \mathscr {L}$ and a conclusion $C\in \mathscr {L}$, ${\varGamma }$ entails C (${\varGamma }\models C$) iff all the models of ${\varGamma }$ are also models of C.¹ A two-column Beth tableau formalizes the reductio ad absurdum that ${\varGamma }\models C$. It features an enumeration of ${\varGamma }$ on the left, and C on the right; and then represents the analysis (decomposition) of ${\varGamma }$ and C according to the reductio hypothesis. When the semantics of $\mathscr {L}$ allows for alternative truth-values, subtableaux are created for each alternative, on both sides. The rules for the left-hand side are represented in tree form in Fig. 1 omitting material conditional (more on this form soon). They reflect the reductio assumption that all formulas on the left-hand side of the tableau are true. They also push negation in, which prevents traffic between columns (this is desirable for the interrogative extension of Beth tableaux, cf. Sect. 2.3).

Rules for the right-hand side are mirror-images of those of the left-hand side, and reflect the reductio interpretation that all the formulas on the right-hand side are false. They are displayed in Fig. 2. The tree form allows for a representation of the left- and right-hand sides of a subtableau on a single branch, by simply switching labels and is thus easier to read.²

A subtableau yields an impossible distribution of truth-values when: (1) a sentence S and its negation $\lnot S$ occur on the same subtableau with the same label; or: (2) a formula S appears in the same subtableau with different labels. If this happens, the subtableau is declared closed, and no further application of the rules is necessary. Otherwise, it remains open, and yields a model of ${\varGamma }$ in which C is interpreted as false. The tableau is declared closed iff all the branches are. Beth tableaux are sound and complete for entailment: if there is a closed tableau proof with premises ${\varGamma }$ and conclusion C (abbreviated ${\varGamma }\vdash C$), then ${\varGamma }\models C$ (soundness); and if ${\varGamma }\models C$, then ${\varGamma }\vdash C$ (completeness).

Fig. 1

Left column rules for Beth tableaux (tree form)

Fig. 2

Right column rules for Beth tableaux (tree form)

A proof procedure is analytic if it proceeds without auxiliary constructions (lemmas). Beth tableaux are analytic because they comply with the subformula principle: every formula that occurs in a subtableau $\tau$ is a subformulas of some formula occurring $\tau$. Selective violations of this principle are possible via the the Cut rule, represented Fig. 3. The construction of a Cut-free tableau is always possible in principle, but the Cut rule is critical for the reconstruction of Holmesian deduction, to which I will now turn.

Fig. 3

Cut rule for tableaux

2.2 Interrogative tableaux and interrogative games

The first step for an extension of Beth tableaux beyond “narrowly deductive applications” is to interpret tableau construction as a game. One player, Inquirer, is trying to establish C, as the potential answer to some overarching ‘big question’ that may be represented by the disjunction $C\vee \lnot C$. Inquirer’s background knowledge is represented by ${\varGamma }$. It is assumed that simply asking whether C is not an option, so that C (or its negation $\lnot C$) must be established with the help of ‘instrumental’ questions. The other player, who answers, is Nature. Relations between moves in the game and tableau rules are as follow:

There are moves of three different kinds: (1) deductive moves; (2) interrogative moves; (3) definitory moves.

• (1) The rules for making deductive moves are the same as in any usual formulation of the tableau method. [...] The instantiation rules of tableau construction [introduce] dummy names (indefinite individuals) [...].

• (2) An interrogative move is relative to a subtableau $\sigma _j$. It consists in a question addressed by me to Nature. The presupposition of the question must occur in the left column. [...] Substituting terms [in Nature’s answers] must be individual constants (in the case of wh- questions). [...]

• (3) A definitory move is also relative to a subtableau $\sigma _i$. It consists in the introduction of a new predicate symbol, say P(x). It is introduced by means of an explicit definition, that is, by adding to the left column of $\sigma _j$ either:

$$\begin{aligned} (x) (P(x) \longleftrightarrow f (x)) \end{aligned}$$

or

$$\begin{aligned} (x) (P(x) (x=a_1 \vee x=a_2\dots \vee x=a_k)) \end{aligned}$$

where f is an expression in the vocabulary that has been used in $\sigma _i$ and has one free variable, and where $a_1, a_2,\dots ,a_k$ are individual constants. (Hintikka and Hintikka 1983, pp. 166–167)

Summing up, deductive moves (1) are represented by standard tableaux rules, and the addition of interrogative moves introduces no other change than a distinction between definite and indefinite individuals. Presuppositions for interrogative moves (2) are, for whether-questions, formulas that would split a tableau in subtableaux; and for other wh-question, formulas that would introduce a new individual. Definitory moves (3) allow for extending the vocabulary available in the proof, beyond that of ${\varGamma }$ and C, for instance when Inquirer’s own vocabulary is richer.

Whenever Nature fails to answer a whether question, Inquirer must reason by cases; and when Nature fails to answer a wh-question, she must keep track of an indefinite individual, and remember not to make any special assumption about it. Conversely, Nature’s answers reduce the number of alternatives and the number of indefinite individuals in a proof. The Hintikkas express the strategic problem that arises from this situation as follows:

As the case usually in game theory, players’ strategic considerations are determined essentially by the payoffs. We shall no try to specify them fully here. The following general principles are nevertheless important:

• (1) An interrogative move involving a wh- question is the more expensive the more layers of quantifiers there are in the question [...] the ‘price’ of a question being equal to the same number of units as there are layers of quantifiers in the question. [...]

• (2) A definitory move is the more expansive the more layers of quantifiers there are in the definiens [...] each additional layer [...] costing a unit.

• (3) Of deductive moves, each of those introducing new dummy names cost a unit. (Hintikka and Hintikka 1983, p. 167)

Rationale for (1)–(3) are straightforward. The cost of propositional whether questions is indirect only: if successful, they do not introduce new individuals; otherwise, they open subtableaux with their own cost. A successful wh-question introduces a constant naming a denizen of the state of Nature, improving Inquirer’s knowledge. If the move is unsuccessful, Inquirer must herself introduce the ‘dummy name’ of an indefinite individual that she may have to identify at a later stage. This may in turn require additional moves, with the risk of inflating the number of subtableaux and individuals (definite and indefinite) to consider, and increasing the load on Inquirer’s memory and reasoning abilities. The payoffs therefore translate explicitly, in game-theoretic terms, naturalistic constraints. Notice that (1)–(3) entail that the cost of a given strategy (in a given subtableau) has an upper bound, namely the cost incurred by the strategy if Nature does not answer any of Inquirer’s questions.

The Hintikkas later introduced another parameter, the range of attention (Hintikka and Hintikka 1989), which explicitly specifies the range of yes–no questions accessible to Inquirer in a given inquiry. Since the presupposition of a yes–no is an instance of the Excluded Middle, all such instances follow (trivially) from any set of premises ${\varGamma }$. Thus, in principle, Inquirer could ask any yes–no question of her choosing (equivalent to an application of the Cut rule). Restricting these questions reflects, again, the naturalistic interpretation of the model, where Inquirer’s reasoning abilities fall short of logical omniscience. Since a yes–no question is a propositional question, its cost is indirect, and no alteration of the 1983 payoff scheme is necessary.

2.3 Model consequence and pure discovery

In Beth tableaux, counter-models to C are generated from each open subtableau by constructive methods. By contrast, in interrogative tableaux, which are relative to the state of Nature, a counter-model generated from an open subtableau is a state description compatible with what is known about that state. A consequence of this, initially overlooked, is that interrogative tableaux define implicitly a consequence relation that differs from semantic entailment. Characterizing this relation became a major endeavor in the late 1980s, and proof-theoretic considerations then took precedence over naturalistic motivations. Reference to the state of Nature, and its formal representation as a model of $\mathscr {L}$, becomes explicit in the presentations of the interrogative model in the late 1980s, such as this one:

The basic idea on which the model is based is simplicity itself. It can be expressed most easily in the jargon of game theory. A player, called the Inquirer, is trying to prove a predetermined conclusion C from a given theoretical premise T. [...] Inquirer may address questions to a source of information and use the answers (when available) as additional premises, in short, may carry out interrogative moves. The answerer is called Nature. [...] The questions must of course pertain to a given model M of the language of T. [...] The deductive moves are restricted to those stages of tableau construction that satisfy the subformula principle, except for a given set of tautologies $(S \vee \lnot S)$ that may be inserted as extra premises. (It is also assumed that the tableau rules do not move sentences from one column to the other.) (Hintikka 1988, p. 173)

The passage calls for a few clarifications. First, T is simply a conjunction $T_1\wedge \dots \wedge T_n$ where $T_i\in {\varGamma }$, since in the imi, ${\varGamma }$ is assumed to be finite (because Inquirer’s memory is). Second, if one assumes that C is expressed in the same vocabulary as T, an underlying model that interprets T eo ipso interprets C, and definitory moves become redundant. The assumption is implicit in the passage, and these moves are thus omitted. Hence, the only difference between the above description, and the one from 1983, is the addition of an underlying model. The underlying state of Nature is initially unknown to Inquirer, and her questions aim at identifying its structure, that is, its denizens, and the relations they stand in.

Let $\mathscr {S}$ denote the underlying structure standing for the state of Nature. The interpretation of the vocabulary of T relative to $\mathscr {S}$ is assumed to be fixed during inquiry, guaranteeing that the answers are informative about $\mathscr {S}$. In the simplest case, it is assumed that $\mathscr {S}\models {\varGamma }$, but the assumption can be relaxed. Now, if this assumption holds, and if Nature’s answers are truthful, there are two limit cases: (1) when no interrogative move is used, or they are all unsuccessful; and: (2) when ${\varGamma }$ is empty, but all questions about $\mathscr {S}$ can be answered. In case (1) the interrogative tableau is identical with a Beth tableau, and closes iff ${\varGamma }\vdash C$. Case (2) reduces to model-checking procedure via an oracle (Nature) and the tableau closes iff $\mathscr {S}\models C$. From this, it is easily seen that interrogative tableaux capture a notion of consequence that holds the middle ground between derivability and truth-in-a-model.

The relation was characterized by Hintikka et al. (1999) in the late 1990 s under the name model consequence, and abbreviated $\mathscr {S}: {\varGamma }\vdash S$. This characterization substituted cognitive considerations and game-theoretic formalism with an informal game-theoretic interpretation of tableau construction, and an equally informal notion of strategy. More explicitly, Hintikka, Halonen and Mutanen assumed that the construction of an interrogative tableau represents formally the reasoning processes of Inquirer in a game with asymmetric information against Nature, who chooses $\mathscr {S}$ and a set of oracles. In simplest case, there is a single oracle, identical with Nature, so that information available about $\mathscr {S}$ can be represented by a set $\textsf {Ans}(\mathscr {S})\subseteq \mathscr {L}$ (initially unknown to Inquirer), and $\mathscr {S}$ is such that $\mathscr {S}\models S$ for any $S\in {\varGamma }\cup \textsf {Ans}(\mathscr {S})$. In that case, no additional justification is in fact needed for either ${\varGamma }$ or any answer in $\textsf {Ans}(\mathscr {S})$, and this case is referred to as Pure Discovery. Of course, due to the information asymmetry, Inquirer cannot know that she is playing a game of Pure Discovery, but she can play ‘as if’ she were, until revision becomes necessary.³ In this special case, standard first-order theorems have interesting consequences relative to interrogative reasoning.

3 The strategic viewpoint

3.1 Interrogative logic and its strategic interpretation

This section presents three of the main results of the logic of model consequence, called interrogative logic by Hintikka, Halonen and Mutanen. These results are the Deductive Completeness Theorem, the Yes–No Theorem, and the Strategy Theorem. I will leave out two other results, the Covering Law Theorem and the Extended Beth Theorem, for which they do not offer a strategic interpretation. All of the above also have modal extensions, where modal operators formalize the notion that, in Pure Discovery, premises and answers are known, and that reasoning is closed under an implicit knowledge operator. However, no semantics for this operator is provided, and I will therefore leave the modal extension out of the discussion. The Deductive Completeness theorem and the Yes–No Theorem are proved in extended interrogative logic (eil), in which Inquirer is allowed to introduce arbitrary yes–no questions. The Strategy Theorem requires only interrogative logic simpliciter, where she is not allowed to do so. The Deductive Completeness Theorem expresses that Nature’s answers function as additional premises:

Theorem 1

(Deductive Completeness, Hintikka et al. (1999, pp. 53–54)) Let $\textsf {Ans}(\mathscr {S})$ and ${\varGamma }$ be given. Then: $\mathscr {S}:{\varGamma }\vdash C$ iff ${\varGamma }\cup \textsf {Ans}(\mathscr {S})\vdash C$.

The proof given in Hintikka et al. (1999, p. 54) abstracts from the details of transformations of Beth tableaux into interrogative tableaux, by representing tableaux in sequent form. An alternative proof making the transformation explicit is given in “Appendix: Formal proofs”. The Yes–No Theorem, is stated as follows:

Theorem 2

(Yes–No Theorem, Hintikka et al. (1999, p. 55)) Let $\textsf {Ans}(\mathscr {S})$ and ${\varGamma }$ be given. If $\mathscr {S}:{\varGamma }\vdash C$, then C can be established using only yes–no questions.

Again, the proof abstracts from the details of the transformation of strategies, and an alternative proof is given in appendix. If one abstracts from these details, the results are straightforward consequences of meta-theorems of first-order logic. Hintikka, Halonen and Mutanen acknowledge the point, but at the same time appeal to a “strategic viewpoint” illustrated for instance with their gloss on the Yes–No Theorem:

The strategic viewpoint [...] put[s] into the proper perspective the Yes–No Theorem. It is virtually trivial technically and yet it seems to have sweeping implications. What are other kinds of questions good for, anyway, if their job could equally well be done by the simplest of all questions, yes–no questions? The answer is that the inferential job of other kinds of questions can be done by yes–no questions, but that their strategic job cannot be so done. [...] Hence, the “can” in the Yes–No Theorem means a definitory “can”, not a strategic “can”. Its import can perhaps be best expressed by saying that any argument can in the light of hindsight be subsequently replaced (in extended interrogative logic) by an argument where all questions used are yes–no questions. (Hintikka et al. 1999, p. 59)

In the light of this passage, what actually matters is the transformation of a deductive strategy into an interrogative one. The point is further illustrated by the Strategy Theorem, which borrows its notion of strategy from proof theory, rather than game theory. The proof-theoretic notion is for instance illustrated by R. Smullyan’s discussion of recursive procedures for systematic constructions of tableau proofs which can be bested by “clever strategies” studied in theorem-proving.⁴ Hintikka, Halonen and Mutanen in turn mention those studies, as the formal basis for the Strategy Theorem:

From studies of strategies of theorem-proving it is known that the crucial strategic question in deduction is which of [the existentially quantified] sentences to apply [the rule of existential instantiation] to first. (Thus, we can disregard the choice of propositional questions.) Obviously, in interrogative reasoning the crucial question is which of them to use first as the presupposition of a wh-question. With certain qualifications, it can be seen that not only is the range of choice the same [...]. What is crucial, the optimal choice is the same in both cases. (Hintikka et al. 1999, p. 58)

The theorem itself expresses slightly more formally the conclusion of the above argument:

Theorem 3

(Strategy Theorem Hintikka et al. (1999, p. 58)) “The optimal choice of the wh-question to ask is the same as the optimal choice of the rule [of existential instantiation] to apply, assuming that the question is answerable.”

The restriction to the case where the question is answerable is straightforward: if a question is not answerable, Inquirer must introduce ad hoc explicit definitions to rephrase the question. A second, implicit, restriction, is that the theorem applies to the case of Pure Discovery: otherwise, Inquirer’s strategy may have to include revisions of her past inferences when a contradiction between ${\varGamma }$ and $\textsf {Ans}(\mathscr {S})$ obtains. Within the limits of those restrictions, the consequence of the Strategy Theorem is that deduction guides question selection in the case of Pure Discovery: since the best interrogative proof of C from ${\varGamma }$ and $\textsf {Ans}(\mathscr {S})$ parallels the best deductive proof of C from ${\varGamma }\cup \textsf {Ans}(\mathscr {S})$, insights into the latter are eo ipso insights into the former, and the theorem vindicates the ‘Sherlock Holmes sense of deduction’:

[I]n the case of pure discovery [...] the choice of the optimal question to be asked is essentially the same as the choice of the optimal premise to draw an inference from in a purely deductive situation. Thus, Sherlock Holmes was right: Strategically speaking, all good reasoning consists of “deductions,” if only in the case of pure discovery. (Hintikka 2007, p. 8)

In fact, the Strategy theorem extends beyond Pure Discovery, as long as Inquirer can behave ‘as if’ the game is one of Pure Discovery, that is, as long as taking ${\varGamma }$ and $\textsf {Ans}(\mathscr {S})$ at face value does not induce any contradiction.⁵

Whenever, to the best of Inquirer’s knowledge, no revision of any of her previous inferences is needed, strategies that optimize deductive tableau construction, also limit the number of alternatives (subtableaux) to consider, or the number of individuals to keep track of in each alternative. Although Inquirer may reach an incorrect conclusion, because $\mathscr {S}$ is not in fact a model of ${\varGamma }$, the Strategy Theorem holds for her, as long as she lacks any evidence that $\mathscr {S}\not \models {\varGamma }$.

3.2 Definitory rules, strategic rules, and strategies

The distinction between “definitory can” and “strategic can” in the discussion of the Yes–No Theorem echoes Hintikka’s distinction between ‘definitory’ and ‘strategic’ rules (Hintikka 1989), which is easily illustrated. Consider a case where ${\varGamma }\vdash C$, so that there is a strategy that suffices to establish $\mathscr {S}:{\varGamma }\vdash C$ using only deductive moves; and assume that there is an optimal strategy to prove deductively C from some finite ${\varGamma }'\subset {\varGamma }$, using the premises in ${\varGamma }'$ in some definite order, and minimizing the subtableaux and the number of individuals that occur in each of them. Let us furthermore assume that Inquirer’s memory is a source for ${\varGamma }$, that is, that ${\varGamma }'\subset \textsf {Ans}(\mathscr {S})$ and that ${\varGamma }'$ can be generated by a sequence of yes–no questions (representing as many memory recalls). These questions can be asked to obtain elements of ${\varGamma }'$ in the order of appearance in the shortest deductive tableau proof that ${\varGamma }\vdash C$. The Cut rule, which allows to introduce presuppositions in any order, is definitory. A higher-order rule specifying the optimal order of application the Cut rule to obtain ${\varGamma }'$, would be an example of strategic rule. Hintikka expresses the same idea informally when he writes that Socrates demonstrates ‘strategic knowledge’ (Hintikka 2007, p. 95). Socrates, who seemingly reasons from answers to yes–no questions alone, knows in fact which yes–no questions to put to his audience, so as to obtain the premises he needs, and infer from answers he obtains the conclusions he wants his audience to accept.

More generally, the tableaux-building rules of Figs. 1 and 2, are definitory, while rules for systematic tableaux constructions are strategic. But as Smullyan points out, some clever strategies disregard those strategic rules. A paraphrase of Smullyan’s point is that systematic procedures offer baseline strategic rules, that can be improved upon. Therefore, unlike definitory rules, strategic rules are not unique. According to Hintikka, Halonen and Mutanen, the conceptual fruitfulness of these insight into deductive strategies and their role in interrogative inquiry, trumps the relative technical triviality of the results of eil. Their argument extends to other logical analyses of questions that establish reduction theorems. For instance, it can be established within Wisniewski’s erotetic logic that any question of arbitrary complexity can be reduced to a set of atomic yes–no questions (Wisniewski 1994), and the result also allows for a logical characterization of strategic reasoning in question selection (Wisniewski 2003). The notion of strategic rule is also an informal counterpart of the game-theoretic notion of strategy. A strategy for player I in a game in extensive (move-by-move) form, is a function assigning a move to every position at which it is I’s turn to play. The construction of a Beth tableau is akin to a game of solitaire, and a systematic procedure, as a set of strategic rules, specifies recursively a strategy in that game (which move to play at each step of the tableau construction). The Strategy Theorem, extending the proof-theoretic notion from the purely deductive case to the interrogative-deductive case, makes redundant an explicit game-theoretic analysis.

3.3 Abandoning game theory

J. Hintikka still held the view that explicit game-theoretic concepts (such as payoffs) had their place in the imi in the late 1980s.⁶

It is thus surprising that the Strategy Theorem did not receive an explicit game-theoretic expression, for instance refining the 1983 payoff scheme. Since Hintikka, Halonen and Mutanen do not explain why they chose not to do so, we are left with educated guesses. Clearly, once model consequence and Pure Discovery are defined explicitly, the preferences that govern the construction of shorter deductive proofs transfer almost immediately to interrogative proofs, and specifying costs for strategies would be redundant. But the redundancy could have been interesting. For instance, via the 1983 payoff scheme, shorter proofs reward lower cognitive loads, and an overlay of game theory would have preserved this naturalistic interpretation. Why is there none?

A rather obvious reason is that game theory is not necessary. A ‘game against Nature’ is a 1-player sequential decision problem where no strategic interaction actually takes place between the player and Nature. But decision theory is absent as well. In fact, the standard model of sequential decision-making is the same whether the decision-maker takes into account alternative courses of action of other agents (n-player games) or alternative states of Nature (1-player games). In a nutshell, the agent is assumed to consider, at any given position where she has to make a choice, all the possible end-states that could result from her next decision, given what she currently knows about the state of Nature (and, in a n-player game, about other players’ strategies). Then, she chooses her next move by eliminating those moves that would bring about end-states with lower payoffs, a process called elimination of dominated strategies.

Consider now a Beth tableau proof as a 1-player game, and assume that the single player, Eloise, wins iff she stabilizes on the correct answer to the question whether ${\varGamma }$ entails C. By completeness of Beth tableaux, Eloise has a winning strategy, corresponding to a reductio argument: conjecture that ${\varGamma }\not \models C$ and execute a systematic procedure to build the tableau, with a commitment to change her mind if the tableau closes. If ${\varGamma }\models C$, Eloise will win after finitely many iterations of the (strategic) rules for building the systematic tableau. As Smullyan remarks, there are alternatives to this brute-force strategy. But the semi-decidability of first-order logic entails that Eloise cannot in general reason to those alternatives by eliminating dominated strategies. Otherwise, she would have to anticipate and prevent losses that resulting from building infinite subtableaux.⁷ If ${\varGamma }\not \models C$, Eloise’s reductio strategy may not even be finite, but she is still guaranteed to win. Again, she cannot in general eliminate dominated strategies (for instance, those including redundant moves) because this would sometimes require comparison between infinite strategies. Summing up, in order to reason by elimination of dominated strategies, Eloise would have to be able, in general, to solve uncomputable problems.

Since the Strategy Theorem entails that Inquirer’s strategic problem is essentially the same as Eloise’s strategic problem, Inquirer can solve her strategic problem by elimination of dominated strategies iff Eloise can. Unlike game theorists, proof theorists cannot accept idealizations to the effect that strategic reasoning manipulates strategies that are not effectively computable. This is why Hintikka, Halonen and Mutanen claim that the parallelism between interrogative reasoning and deductive reasoning warrants only conclusions about how proof heuristics inform interrogative inquiry. In particular, they justify the informal phrasing of the Strategy Theorem by the fact that it applies to tableau construction in general (whether it will close or not) but there are no recursive rules for building an optimal open tableau. With elimination of dominated strategies off the table, there is not need to specify payoffs explicitly, and preferences for shorter proofs can still be interpreted informally as preferences for lower computational loads.

4 Question evocation

4.1 A hidden parameter in eil

Unlike payoffs, ranges of attention are not redundant in eil. Results of eil hold for an Inquirer who is: (1) capable of deriving presuppositions from her premises, and using them to ask questions; and: (2) capable of introducing presuppositions of yes–no questions when necessary. Assuming that tableaux rules represent reasoning takes care of (1), although it must also be assumed that Inquirer knows a presupposition when she sees one (this can be taken care of by generalizing the notion of range of attention). Given the range of yes–no questions expressible in $\mathscr {L}$, (2) may seem more elusive, but in practice, the range of attention required for the main results of eil to hold is rather limited. It is useful to relativize the range of attention, hereafter RA, to a given interrogative tableau $\mathfrak {T}$, hereafter $\textsf {RA}(\mathfrak {T})$.

Some auxiliary definitions will be useful to characterize Inquirer’s competence. Let $\textsf {Sub}(S)\subseteq \mathscr {L}$ denote the set of subformulas of $S\in \mathscr {L}$, construed in the usual way, and define $\textsf {Sub}({\varGamma })=\bigcup \{ \textsf {Sub}(S): S\in {\varGamma } \}$ for any ${\varGamma }\subseteq \mathscr {L}$. Next, let ${\textsf {Pres}}(\mathscr {L})$ denote the set of formulas of $\mathscr {L}$ that can serve as presuppositions of questions; in particular, the set of instances of the Excluded Middle expressible in $\mathscr {L}$ is a subset of ${\textsf {Pres}}(\mathscr {L})$, denoted $\textsf {Pres}^{\textsf {yes-no}}(\mathscr {L})$. Finally, let $\textsf {Ans}(\mathscr {S},\mathfrak {T})\subseteq \textsf {Ans}(\mathscr {S})$ denote answers from $\textsf {Ans}(\mathscr {S})$ that actually occur in some tableau $\mathfrak {T}$, and let ${\mathbf {\mathsf{{Q}}}}\subseteq \mathscr {L}$ denote the set of potential answers to the principal question under investigation. For some $\mathfrak {T}$ with premises ${\varGamma }$ and conclusion C, it is simply assumed that ${\mathbf {\mathsf{{Q}}}}= \{ C,\lnot C \}$. With the above abbreviations, the meta-theorems of eil of Sect. 3.1 hold when the following hold:

(RA1) translates formally the notion that Inquirer knows the presupposition of a question when it occurs in $\mathfrak {T}$, and thus always knows when she can play an interrogative move in $\mathfrak {T}$. (RA2) imposes weak constraints on the set $\textsf {RA}(\mathfrak {T})\cap \textsf {Pres}^{\textsf {yes-no}}(\mathscr {L})$, or equivalently, singles out the minimal applications of the Cut rule that any Inquirer should be capable of using.⁸

Postulates (RA1) and (RA2) can be commissioned to re-formulate formally Hintikka’s defense of the Yes–No Theorem. Indeed, the existence of a ‘yes–no strategy’ for the construction of a closed interrogative tableau $\mathfrak {T}$ depends on the existence of another closed interrogative tableau $\mathfrak {T}'$, such that $\textsf {RA}(\mathfrak {T})$ is obtained from $\textsf {RA}(\mathfrak {T}')$. By (RA1) and (RA2), for every $S\in \textsf {Ans}(\mathscr {S},\mathfrak {T}')$, $(S\vee \lnot S)\in \textsf {RA}(\mathfrak {T}')$ as well. The non-trivial consequence of the Yes–No Theorem, according to Hintikka, is that the availability of the ‘yes–no strategy’ in $\mathfrak {T}$ is only guaranteed for a particular Inquirer when the strategy to close $\mathfrak {T}'$ is available already to that Inquirer. Formally, it is any strategy such that $\textsf {RA}(\mathfrak {T})\supseteq \textsf {Pres}^{\textsf {yes-no}}(\mathscr {L})\cap \textsf {RA}(\mathfrak {T}')$, which generates a closed tableau. The proof of the Yes–No Theorem given in “Appendix: Formal proofs” illustrates this transfer of strategies.

Some non-trivial consequences of the Deductive Completeness Theorem become more conspicuous with (RA1) and (RA2) in mind. For instance, the theorem holds in general provided that sometimes, at least some of the answers that are necessary to close $\mathfrak {T}$, are obtained using yes–no questions, or equivalently, the Cut rule. Tableaux systems admits of Cut elimination, that is, for every deductive proof using the Cut rule, there is a deductive Cut-free proof of the same conclusion. But relative to an interrogative tableau $\mathfrak {T}$ with premises ${\varGamma }$, this only guarantees that there is a Cut-free deductive tableau $\mathfrak {T}'$ with premises ${\varGamma }\cup \textsf {Ans}(\mathscr {S},\mathfrak {T})$. Still, it may be so that the construction of $\mathfrak {T}$ has required ineliminable yes–no questions. Equivalently, some answers in $\textsf {Ans}(\mathscr {S},\mathfrak {T})$ may remain inaccessible without the Cut rule.

4.2 Heuristics for yes–no questions

The Strategy Theorem establishes a parallel between the construction of Cut-free deductive proof strategies, and interrogative strategies, and as such, does not account for the introduction of yes–no questions. Hintikka, Halonen and Mutanen offer the following comment about a possible extension of the theorem:

[T]he Strategy Theorem applies in the first place to unextended interrogative logic. It can be extended further by noting that [the Cut rule] can be used in ordinary first-order logic to shorten proofs. In interrogative logic, [it] open[s] the possibility of raising new yes–no questions and thereby facilitating new lines of reasoning. How closely parallel the principles for choosing tautology for the two purposes are remains to be studied (Hintikka et al. 1999, p. 59).

We have already seen that interrogative proofs may sometimes require ineliminable yes–no questions. Therefore, the selection of applications of the Cut rule in interrogative tableaux cannot be explained by preferences governing proof optimization alone. This in turn makes conspicuous a possible limitation of the current proof-theoretic approach of the imi. Let me illustrate this with some examples. First, consider an interrogative tableau $\mathfrak {T}$ with premise ${\varGamma }= \{ S\rightarrow C \}$, where the principal question is whether C holds in $\mathscr {S}$, with C being investigated first. The root of the tableau is thus:

Assume that, unbeknownst to Inquirer, $\mathscr {S}\models C$ and $S\in \textsf {Ans}(\mathscr {S})$. As usual, it is assumed that $C\notin \textsf {Ans}(\mathscr {S})$, and that this is known to Inquirer (perhaps from a previous unsuccessful inquiry), so that a direct question about C is not an option. If S is obtained in $\mathfrak {T}$, closing the set $\{ S,(S\rightarrow C) \}$ under modus ponens entails a conclusive answer to the question whether C holds. In the terminology of J. Hintikka’s analysis of questions, the conditional $(S\rightarrow C)$ is a conclusiveness condition for that question, reducing it to the question whether S hold. Assuming (RA2), $(S\vee \lnot S)$ is in $\textsf {RA}(\mathfrak {T})$, and can be used to ask a yes–no question marked ‘?’:

Since, ex hypothesis $S\in \textsf {Ans}(\mathscr {S})$, an answer (marked ‘!’) is obtained and no branching occurs. The tableau rule for conditionals—which treats $(S\rightarrow C)$ as $(\lnot S\vee C)$—is then applied, resulting in two closed tableaux:

In spite of its simplicity, this example illustrates how strategic rules can be defined relative to Inquirer’s range of attention. The strategic rule above can be expressed informally as: look for conclusiveness conditions first. Consider now an interrogative tableau $\mathfrak {T}'$ with conclusion C and premise ${\varGamma }'= \{ S \}$. Assume again that $\mathscr {S}\models C$, that $C\notin \textsf {Ans}(\mathscr {S})$, and that only the latter is known (from some former inquiry). Finally, assume that, unbeknowst to Inquirer, $(S\rightarrow C)\in \textsf {Ans}(\mathscr {S})$. It would be possible to close $\mathfrak {T}'$ if $(S\rightarrow C)\vee \lnot (S\rightarrow C)$ is in $\textsf {RA}(\mathfrak {T})$, as shown below:

While (RA1) and (RA2) suffice to generate the appropriate range of attention in the first example, they are too weak in the second, since neither $(S\rightarrow C)$ nor $\lnot (S\rightarrow C)$ are subformulas of elements of ${\varGamma }$. Nevertheless, the appropriate question can be generated mechanically. Consider, for instance, the following procedure: (1) define $\textsf {Sub}({\varGamma }'\cup \{ {\mathbf {\mathsf{{Q}}}} \} )$ in extension; (2) generate inductively combinations of elements listed at step (1), with the propositional operators of $\mathscr {L}$; (3) for any sentence $S\in \mathscr {L}$ obtained at step (2), add $(S\vee \lnot S)$ to $\textsf {RA}(\mathfrak {T}')$. Since ${\varGamma }'$ is finite, (1) can be executed before (2). Step (2) cannot be fully executed before (3), but both can be executed as an iterated loop, adding a yes–no question to $\textsf {RA}(\mathfrak {T}')$ (and therefore, to $\mathfrak {T}'$) after its presupposition has been generated. Assuming for simplicity that S and C are Boolean atoms, the output of step (1) is $\{ S,C \}$. Step (2) generates combinations of S and C with propositional operators $\lnot$, $\wedge$, $\vee$, and $\rightarrow$, and could run indefinitely, but will generate $S\rightarrow C$ after finitely many steps. As soon as this happens, (3) generates $(S\rightarrow C)\vee \lnot (S\rightarrow C)$, and closes $\mathfrak {T}'$. Notice also that the same procedure would also output $S\vee \lnot S$ after finitely many iterations, and close $\mathfrak {T}$. This procedure does not so far prioritize conclusiveness conditions, but may be refined to generate pairs of sentences that can be closed under modus ponens. With such a refinement, the 3-step procedure would output $S\vee \lnot S$ from $\mathfrak {T}$, and $(S\rightarrow C)\vee \lnot (S\rightarrow C)$ from $\mathfrak {T}'$, at the first iteration.

4.3 Another logic of scientific discovery

Algorithms for the discovery of instrumental questions of the sort just described relate the imi to N.R. Hanson’s logic of discovery, via its formal reconstruction in H. Simon’s ‘normative theory of law-discovery processes’ (Simon 1973). Simon construed literally Hanson’s notion of pattern of discovery (from the title of Hanson’s seminal book), formalizing discovery by means of pattern-recognition algorithms. These algorithms scan a finite data sequence, and when they detect a pattern, output an encoding for that pattern. This encoding becomes a candidate ‘law’ for the sequence, that can be tested via its prediction for the next data point. The theory is, according to Simon, a ‘logic’, because it supports normative claims. In particular, it ranks algorithms relative to how fast they detect and encode a given pattern. Simon argues that the logic of discovery is decoupled from the logic of justification, but his partial agreement with Reichenbach rests on different reasons than Reichenbach’s own. Simon contends that law-discovery algorithms should not be evaluated relative to how likely a candidate law is to be true: otherwise, evaluating discovery algorithms would require a solution to the problem of induction. Rather, evaluation has to remain relative to the efficiency at discovering a pattern (be it a genuine law or an artifact). A law-like generalization based on a discovered pattern must then be tested with the procedures of a ‘logic of justification’.

Simon discussed algorithms which, despite their simplicity, are surprisingly powerful. For instance, unsophisticated algorithms could have hypothesized Mendeleev Periodic Table from the data available at the time, with heuristic search converging faster than brute-force. The algorithms that Simon describes are not limited to the discovery of law-like regularities, and can capture formally the procedures for generating questions outlined in the previous section. Specifically, the data sequence over which discovery supervenes is a finite a string of sentences of $\mathscr {L}$, since ${\varGamma }$ is in, in practical applications, finite. The 3-steps procedure described in the previous section is a brute-force algorithm for generating yes–no questions: it detects well-formed formulas of $\mathscr {L}$ (subformulas of sentences in ${\varGamma }$) and generates yes–no questions from them. Its refinement is an example of heuristic search. It looks for pairs of sentence to which modus ponens can be applied, and outputs yes–no questions to complete incomplete pairs with a missing antecedent (when ${\varGamma }= \{ S\rightarrow C \}$) or a missing conditional (when ${\varGamma }'= \{ S \}$).

Again, there is more to those procedure, than mere proof optimization. The reason is, quite obviously, that the set $\textsf {Ans}(\mathscr {S})$ of answers available in $\mathscr {S}$ is in general not known at the time yes–no questions are raised. But another reason is that, in real-life cases, ${\varGamma }$ represents inquirer’s explicit background knowledge (working memory), while establishing complex chains of conclusiveness conditions involves additional recall of information stored in long-term memory, in particular through associations with the content of perception. This does not preclude the possibility of algorithmic or heuristic search, that could mimic a human inquirer, assuming a more complete model of an inquirer’s perception and memory.

5 The ‘Sherlock Holmes sense of deduction’ revisited

5.1 The Holmesian logician

M.B. and J. Hintikka do not mention either Hanson or Simon, but express ambitions that are strikingly similar to theirs, as conspicuous in this passage:

The crucial part of the task of the Holmesian “logician”, we are suggesting, is not so much to carry out logical deductions as to elicit or to make explicit tacit information. This task is left unacknowledged in virtually all philosophical expositions of logical reasoning, of deductive heuristics, and of the methodology of logic and mathematics. For this neglect the excuse is often offered that such processes of elucidations and explication cannot be systematized and subjected to rules. It may indeed be true that we cannot usually give effective rules for heuristic processes. It does not follow, however, that they cannot be discussed and evaluated, given a suitable conceptual framework.” (Hintikka and Hintikka 1983, pp. 156–157)

Deductive moves in interrogative tableaux are means to “make explicit tacit information”, and interrogative moves, means to “elicit [...] information”. Strategic rules for using those moves are thus strategies for Holmesian deduction. The Strategy Theorem shows the relevance of proof theory, and the argument in the previous section, the relevance of Simon’s logic of discovery, to acquisition of information through interrogation. Let me now turn to an informal example, namely Sherlock Holmes’ problem in The Case of Silver Blaze, one of the Hintikkas’ favorite (see Hintikka and Hintikka 1983; Hintikka and Halonen 2005; Hintikka 2007, among others), to further illustrate the point.

In The Case of Silver Blaze, Sherlock Holmes must identify the thief of a race-horse, Silver Blase, and find the horse before an upcoming race, in which it is favorite. The thief is also believed to be responsible for the death of the horse’s trainer, John Straker. Holmes has learned from the newspapers that a suspicious individual, Fitzroy Simpson, visited the stables on the evening before the crime, on the pretense of asking tips about the race. His untimely visit frightened a maid, who called a stable-boy for help, and the stable-boy let his watchdog on Simpson. Inspector Gregory, in charge of the inquiry, believes Straker suspected that Simpson would return, acted upon the suspicion, and met his end at Simpson’s hand. Evidence against Simpson is circumstantial: his scarf was found near Straker’s body, but he claims to have lost it during the evening; and his walking stick could have been the murder weapon, but the killing blow could have been dealt with any blunt instrument. Holmes remains unconvinced, and describes the case as one where “[t]he difficulty is to detach the framework of fact [...] from the embellishments of theorists and reporters” (Doyle 2003, p. 522).

The differences between the inquiry strategies of Gregory and Holmes illustrate informally the role of deduction in “eliciting [...] information” and “making explicit implicit information”, as well as the interplay of discovery and justification. Gregory relies on routine questions (whether Simpson had a motive, an opportunity, could be placed at the crime scene, or possessed a possible murder weapon) to which he obtains positive answers, forming the kind of pattern policemen are trained to discover. The ‘law’ for that pattern predicts that any question whose answer depends on whether Simpson is guilty, will receive an answer consistent with Simpson’s guilt. However, Gregory fails to include the presence of a watchdog in relevant data, and thus to predict that the dog would have barked at Simpson, again, during the night. By contrast, the presence of the dog and its silence remind Holmes of the general truth that trained watchdogs only remain silent when ordered to by their masters. From this, Holmes concludes that “the midnight visitor was someone whom the dog knew well” (Doyle 2003, p. 544), that is, implicit information that Gregory has failed to make explicit.

More interesting even is how Holmes solves the case, for Holmes’ thought process could be reconstructed as an attempt to discern new patterns, after Gregory’s hypothesis has been eliminated. Holmes pays attention to unusual circumstances, whose relevance was so far overlooked. For instance, Straker carried a knife, but it was “[a] very delicate blade devised for very delicate work [and a] strange thing for a man to carry with him upon a rough expedition, especially as it would not shut in his pocket ” (Doyle 2003, p. 532). Also, a bill for an expensive dress, addressed to a William Derbyshire, was found on Straker’s body, but “men do not carry other people’s bills about in their pockets ” (Doyle 2003, p. 545). Holmes inquires whether Straker’s widow owns the dress (she does not) and hypothesizes that Straker had a mistress and bought a dress under an assumed name. The cost of a double life provides a motive to rig the upcoming race, and the means to do so is suggested when Watson identifies Straker’s knife as a scalpel. Holmes then suspects that Straker tried to cripple the horse, and was accidentally killed in the process. Holmes reasons to the consequences of that hypothesis—Straker, lacking medical expertise, would have practiced first—and inquires about animals Straker could have practiced on, finding out that, among the sheep that keep company to the horses, several have inexplicably gone lame.

5.2 Analysis, guesses, and associations

In the Case of Silver Blaze, Holmes selects his questions—whether the dog had barked during the night, whether Straker’s widow owns a dress, and whether some sheep have gone lame—based on the expected consequences of their answers. These questions, and the lines of reasoning they belong to, are suggested by associations between circumstances of the case—Simpson’s first visit, the bill in Straker’s pocket, or the inadequacy of Straker’s knife for self-defense—and the content of Holmes’ memory relative to watchdogs, gentlemen, and how to rigg races. Hence, a reconstruction of Holmesian deduction would be incomplete without an account of the evolution of Holmes’ range of attention, and the relation between attention and memory. Reasoning to consequences, Holmes also anticipates (correctly, as it turns out) the answers to all his questions. Hence, a reconstruction of Holmesian deduction must also account for the strategic importance of guesses. Holmes’ guesses are more easily explained in strategic terms than his associations. To see why, let me quote J. Hintikka on Peirce’s view that abduction involves an element of guessing:

Strategically, there is little difference between selecting a question to ask in preference to others and guessing what its answer will be—and guessing how it compares with the expected answers to other questions that could be asked. [...] [I]n interrogative inquiry, the crucial consideration is to anticipate the epistemic situation brought about by the answer—which in practice typically amounts to anticipating the answer. And such anticipation is hard to characterize in any terms other than guessing. What is especially interesting—and especially reminiscent of Peirce—is that such an element of guessing in abductive questioning is completely compatible with the strategic analogy between deduction and interrogation. (Hintikka 2007, p. 56)

Holmes’ guesses can therefore be characterized as strategic anticipations, under the umbrella of the “strategic analogy between deduction and interrogation”, that is, by the Strategy Theorem.⁹ There remains that these strategic anticipations are formed after associations between facts (the watchdog’s silence and the content of Straker’s pockets) and the content of Holmes’ memory (general truths about watchdogs, gentlemen’s habits, and knives). This brings us back to the first remark, which echoes the ambitions that M.B. and J. Hintikka expressed for their model:

Eliciting tacit information by questioning can be viewed as one possible recall procedure. [...] This partially shared model for recall and intelligent inquiry may perhaps serve as an explication for the link between memory and intelligence [and] should not surprise any Sherlock Holmes fan. In some cases, the great detective has to carry out an observation or even an experiment to answer the question. More frequently, all he has to do is to perform an anamnesis and recall certain items of information which he already had been given and which typically had been recorded in the story or novel for the use of the readers, too, or which are so elementary that any intelligent reader is expected to know them. (Hintikka and Hintikka 1983, p. 159)

The Hintikkas’ example in support for this remark, is Holmes’ reasoning from the silence of the dog in the Case of Silver Blaze. But how can we follow up on their suggestion that it illustrates a relation between recall and intelligent inquiry? One possibility is to extend the strategic viewpoint to both analytic and associative thought processes. The idea of ‘strategic associations’ may, at first, sound somewhat contradictory. And yet it has an illustration in the psychology of creative thought. Creative thought processes involve both associative and analytic sub-processes, and in recent years, L. Gabora has proposed that this integration is made possible by the architecture of memory (Gabora 2010). Gabora’s model synthesizes earlier findings from cognitive psychology, neuroscience, and computational modeling of memory processes, and reconstructs creative insight as the outcome of recruiting specific neural cliques, that Gabora calls neurds, as a result of an interplay of analytic and associative thought:

[A]nalytic thought requires a state of focused attention, and associative thought requires a state of defocused attention. Creativity involves not just the capacity for both [analytic and associative thought] but the capacity to spontaneously shift between them according to the situation, referred to as contextual focus. [C]contextual focus is explicable at the level of cell assemblies [...] composed of neural cliques, some of which respond to situation-specific aspects of an experience, and others of which respond to general or abstract aspects. [...] Leakage of information from outside the problem domain occurs in a manner that is a priori unpredictable because it involves unearthing associations that exist due to overlap of items in memory that may not have been previously noticed. Because memory is distributed, coarse-coded, and content-addressable, items encoded previously to neurds are superficially different from the present situation yet share aspects of its deep structure. Therefore, the recruitment of neurds may foster associations that are seemingly irrelevant yet potentially vital to the creative idea. (Gabora 2010, p. 13)

In Gabora’s model, recall is described in probabilistic terms, and defocused attention alters the probability that specific memory-encoding cell assemblies are activated. In strategic terms, defocusing is tantamount to selecting a particular mixed strategy for recall. A mixed strategy is a lottery (mixture) over deterministic strategies, and both contextual focus and defocused attention represent different mixtures of deterministic strategies that would activate particular cell assemblies: focused attention lowers the probability that neurds are activated, while defocused attention raises it, allowing for strategic associations. Interestingly, Sherlock Holmes is often pictured as seemingly distracted and daydreaming, and at least once in the Case of Silver Blaze.¹⁰ It invariably turns out that he is in fact engaging in “associations [...] seemingly irrelevant yet potentially vital” to the solution of the current case. It is thus fitting for a model of the ‘Sherlock Holmes sense of deduction’ to feature parameters such as the range of attention, that can be used to describe associative processes, if one’s ambition is to understand the strategic role of these processes. Models of the architecture of memory, such as Gabora’s, suggest that the imi could be developed in a direction faithful to the Hintikkas’ original vision, provided that these parameters are reinstated in the model.

6 Concluding remarks

When M.B. and J. Hintikka laid down the logical foundations of the ‘Sherlock Holmes sense of deduction’, they appealed explicitly to game theory, in order to support a naturalistic interpretation of their model. This interpretation was reflected in how they set the payoffs for interrogative strategies (rewarding lower memory loads) or how they dealt with logical omniscience (with the range of attention). After the demise of M.B. Hintikka, the interrogative model was progressively streamlined, leaving explicit only its logical architecture. An informal strategic viewpoint was substituted to the explicit formalization of strategies, that J. Hintikka deemed sufficient to capture the ‘Sherlock Holmes sense of deduction’, vindicate the Bacon-Kant view of inquiry, and serve as a foundation for a logic of discovery (Hintikka 2007, ch. 1, 4 and 10).

In this paper, I have examined this streamlining process critically, and I have concluded that parameters with an explicitly cognitive interpretation are necessary to support the claim that the imi captures the logic of discovery, as well as to safeguard its empirical adequacy. Those parameters bridge the imi with other models of the logic of discovery, such as Simon’s. They can capture the strategic role of memory in Holmesian deduction, and more generally of associative processes. As for the choice of those parameters, payoffs and utilities cannot shed much light on proof-theoretic results, as long standard models of strategic reasoning are assumed. Fortunately, the imi needs little more than an explicit range of attention, indexed on positions where Inquirer can move. Transitions between ranges of attention can indeed be interpreted as the outcome of perceptual or mnemic processes, or a combination thereof, and as the result of either analytic or associative modes of thought. The imi could in fact remain agnostic about those processes, but it may also seek compatibility with extant models of the architecture of memory, in order to account for creative processes in strategic terms. This convergence would offer a strong alternative to the Popper-Reichenbach view of scientific inquiry, and a rebuttal of the premise upon which it is built, that creative thought processes cannot be reconstructed within a logic of discovery.

Appendix: Formal proofs

1.1 Deductive completeness theorem

Proof

[$\Rightarrow$] Assume that $\mathscr {S}:{\varGamma }\vdash C$. Then, there is a closed interrogative tableau $\mathfrak {T}_0$ with premises ${\varGamma }$ and conclusion C where some answers $S_1,\dots ,S_n \in \textsf {Ans}(\mathscr {S})$ are used. Hence, every answer $S_i$ appears at a node of some subtableau $\tau _0$ of $\mathfrak {T}_0$ as ${\textsf {L-}}S_i!$ after its presupposition $P_i$ has appeared at a node as ${\textsf {L-}}P_i?$ in the same subtableau. Then, $\mathfrak {T}_0$ is identical to a Beth tableau $\mathfrak {T}_1$ with premises ${\varGamma }$ and conclusion C, in which, for every $S_i$, $P_i$ and $S_i$ appear in some subtableau $\tau _1$ of $\mathfrak {T}_1$ identical to $\tau _0$ save for the omission of ‘?’ and ‘!’, and where no tableau rule is applied to ${\textsf {L-}}P_i$ in $\tau _1$. This, in turn, is equivalent to assume that $S_i$ has been added to the premise set ${\varGamma }$ during the construction of $\mathfrak {T}_1$. Therefore, there is a closed Beth Tableau $\mathfrak {T}_2$ with premises ${\varGamma }\cup \{ S_1,\dots ,S_n \}$, conclusion C, and where, for every $S_i$ that appears in some subtableau $\tau _2$, such that $\tau _2$ is identical to $\tau _1$ save for the omission of the node ${\textsf {L-}}P_i$. By construction, to every closed subtableau $\tau _0$ in $\mathfrak {T}_0$, corresponds a closed subtableau $\tau _1$ in $\mathfrak {T}_1$, and a closed subtableau $\tau _2$ in $\mathfrak {T}_2$; and there are no subtableaux in either $\mathfrak {T}_1$ or $\mathfrak {T}_2$ that are not obtained from some subtableau of $\mathfrak {T}_0$. Therefore, by construction also, all subtableau of $\mathfrak {T}_1$ and $\mathfrak {T}_2$ are closed; and by completeness of Beth Tableaux, ${\varGamma }\cup \{ S_1,\dots ,S_n \} \vdash C$. Since, by assumption, $S_1,\dots ,S_n \in \textsf {Ans}(\mathscr {S})$, then ${\varGamma }\cup \textsf {Ans}(\mathscr {S})\vdash C$, as desired. $\square$

Below is represented the construction of subtableaux for cases where $P_i=(S_i\vee S_j)$ and $P_i=\exists x S_i[x]$ (other cases are left to the reader). Since $\mathfrak {T}_0$ is finitely generated and has finitely many branches, the construction can be iterated, yielding a closed tableau.

Proof

[$\Leftarrow$] Assume that ${\varGamma }\cup \textsf {Ans}(\mathscr {S})\vdash C$. Then, there is a closed Beth tableau $\mathfrak {T}_0$ with premises ${\varGamma }\cup \textsf {Ans}(\mathscr {S})$. Since closed Beth tableaux are always finite, there is a finite subset ${\varDelta }= \{ S_1,\dots , S_n \} \subseteq \textsf {Ans}(\mathscr {S})$ such that ${\varGamma }\cup {\varDelta }\vdash C$. Let ${\varDelta }^yes--no = \{ (S_i\vee \lnot S_i): S_i\in {\varDelta } \}$. Then, there is a closed Beth tableau $\mathfrak {T}_1$ identical to $\mathfrak {T}_0$, save that any occurrence of $S_i$ in a given branch $\tau _0$ is preceded by an application of the Cut rule introducing $(S_i\vee \lnot S_i)$, where the application is incomplete, that is, no tableau rule is applied to $(S_i\vee \lnot S_i)$. Then there is an interrogative tableau $\mathfrak {T}_2$ with $\textsf {RA}(\mathfrak {T}_2)={\varDelta }^yes--no$, such that $\mathfrak {T}_2$ is identical to Beth tableau $\mathfrak {T}_1$, save that every occurrence of ${\textsf {L-}}(S_i\vee \lnot S_i)$ and of ${\textsf {L-}}S_i$ in some subtableau $\tau _1$ of $\mathfrak {T}_1$, are substituted, respectively, with ${\textsf {L-}}(S_i\vee \lnot S_i)?$ and ${\textsf {L-}}S_i!$ in $\tau _2$. Since by construction ${\varDelta }\subseteq \textsf {Ans}(s)$, $\mathfrak {T}_2$ is a closed interrogative tableau, and therefore $\mathscr {S}: {\varGamma }\vdash C$, as desired. $\square$

Below is represented the transformation of a (closed) deductive Beth tableau with premises ${\varGamma }\cup {\varDelta }$ into an interrogative tableau with one less premise. Again, the procedure can be iterated so as to obtain a closed interrogative tableau with premises ${\varGamma }$.

Alternatively, ${\varDelta }$ can represent a set of guesses (cf. Sect. 5.2), and the transformation, how an interrogative strategy substitutes guesses with questions. Lastly, the procedure can be iterated to eliminate every $T_i\in {\varGamma }$, representing formally Socratic “strategic knowledge”.

1.2 Yes–no theorem

Proof

Assume that C can be established interrogatively from ${\varGamma }$ in $\mathscr {S}$, i.e. that $\mathscr {S}:{\varGamma }\vdash C$. Then, there is a closed interrogative tableau $\mathfrak {T}_0$ with premises ${\varGamma }$ and conclusion C, for an Inquirer with the appropriate range of attention. Since $\mathfrak {T}_0$ is finitely generated, there is a finite subset ${\varDelta }\subseteq \textsf {Ans}(\mathscr {S})$ such that every $S_i\in {\varDelta }$ occurs in $T_0$, and that answers in ${\varDelta }$ suffice to establish C interrogatively, given ${\varGamma }$. Let ${\varDelta }^yes--no = \{ (S_i\vee \lnot S_i): S_i\in {\varDelta } \}$. By (RA2), ${\varDelta }^yes--no \subseteq \textsf {RA}(\mathfrak {T}_0)$. Let now $\mathfrak {T}_1$ be an interrogative tableau with premises ${\varGamma }$ and conclusion C, such that $\textsf {RA}(\mathfrak {T}_1)={\varDelta }^yes--no$, identical to $\mathfrak {T}_0$ save that an application of the Cut rule is interpolated between every interrogative move and its answer, as represented below:

By construction, for every subtableau $t_0$ of $\mathfrak {T}_0$, there is a subtableau $\tau _1$ of $\mathfrak {T}_1$ that closes iff $\tau _0$ closes. Since, ex hypothesis $\mathfrak {T}_0$ is closed, then all subtableaux of $\mathfrak {T}_0$ close, and so do all subtableaux of $\mathfrak {T}_1$. Since, by construction, $\textsf {RA}(\mathfrak {T}_1)$ only includes yes–no question, C can be established interrogatively in $\mathscr {S}$ using yes–no questions only, as desired. $\square$

Remark that, in the above proof, subtableaux $\tau _1$ and $\tau _1'$ of $\mathfrak {T}_1$ can be further streamlined, by removing the (now) redundant moves having lead from ${\varGamma }$ to the redundant presuppositions ${\textsf {L-}}S_i\vee S_j$ and ${\textsf {L-}}\exists x S_i[x]$. Again, this process represents formally Socratic strategic knowledge, and yields the right-to-left Deductive Completeness Theorem as a corollary.