1. The work of providing solid foundations to analysis was initiated by Augustin Cauchy (1789–1857).

2. For references to uses of the device ‘depends on…but not on…’ in actual mathematical literature, see Dechesne (2005), Hintikka (1996), Hintikka & Kulas (1983), Hodges (1997a, 1997b), Mann et al. (2011), Mostowski & Krynicki (1995), Pietarinen (2001); for dependent quantifiers, see also Quine (1970). Bazzoni (2015) criticizes Hintikka’s remarks about the expressibility of uniformity concepts in IF logic, arguing that such remarks cannot show the relevance of IF logic to mathematical theorizing.

3. In order to properly assess the origins of IF first-order logic in light of available documents, also the following should be noted. Hintikka writes (1991: 7): “IF first-order languages are introduced and studied in my paper, ‘What is Elementary Logic?’ (forthcoming).” This paper appeared as Hintikka (1995). Hintikka (1991: 8,67) refers to the papers published in Sandu’s Ph.D. thesis, saying that in them Sandu has also studied independence friendly languages; he mentions specifically Sandu’s study of informationally independent connectives in Sandu & Väänänen (1992), as well as Hintikka & Sandu (1989). In Hintikka & Sandu (1997: 368) it is stated that IF languages were introduced in Hintikka & Sandu (1989) – contradicting what is said in Hintikka (1991). Hintikka (1996: 52) mentions Sandu (1993) and Hintikka (1995) as sources for earlier discussions on IF first-order logic; Hintikka & Sandu (1989) is not mentioned. In Sandu & Hyttinen (2001: 37) it is said that IF first-order languages were introduced in Hintikka (1996), but on the next page it is affirmed that these languages were introduced in Hintikka & Sandu (1989).

The slash notation used for indicating quantifier independence appears already in Hintikka (1988: 22). A general notation for separately indicating those preceding operators of which a given one is independent – more general than the notation of partially ordered quantifiers – was proposed in connection with epistemic logic even earlier, in Hintikka (1982: 164).

4. Thoralf Skolem (1887–1963) introduced Skolem functions in Skolem (1920). For uses of Skolem functions in model theory, see e.g. Hodges (1993). They have also found use in automated theorem proving; cf. the entry on automated reasoning. On how they are employed in linguistics, cf. footnote 90.

5. I.e., a function with zero arguments.

6. Here and henceforth, ‘iff’ abbreviates ‘if and only if.’

7. The function \(f\) yields a witness for \(\exists y\) depending on the interpretation of \(\forall x\), and similarly \(g\) provides a witness for \(\exists w\) depending on the interpretation of \(\forall z\).

8. Henkin introduced the general idea of dependent quantifier \(Q_{m, n, d}\), which in effect leads to the notion of (arbitrary) partially ordered quantifier (p.o.q.) with \(m\) universal quantifiers and \(n\) existential quantifiers, where \(d\) is a function that determines for each existential quantifier on which universal quantifiers it depends; \(m\) and \(n\) may be any cardinal numbers. The notion of finite p.o.q. results by letting \(m\) and \(n\) be finite. Well-known papers on finite p.o.q.s include Enderton (1970), Walkoe (1970), Barwise (1979), Krynicki & Lachlan (1979), Blass & Gurevich (1986), Krynicki (1993); for an overview, see Krynicki & Mostowski (1995). In Barwise (1979) generalized partially ordered quantifiers were also studied.

9. \(\mathbf{FPO}\) is not syntactically closed under negation, conjunction, or disjunction.

10. For a critique, see Hodges (2013), Marion (2009).

11. Let us agree that player 1 is male (‘he’) and player 2 female (‘she’). In the literature, the players have been called by many names: Myself (or \(I)\) and Nature, \(\exists\) and \(\forall\), Eloise and Abelard, as well as the initial Verifier and the initial Falsifier (by reference to the players’ initial roles).

12. Henceforth, whenever \(M\) is a model, M is its domain.

13. Note that while quantifier moves pertain to ‘objects out there’ (elements of the domain), moves for conjunction and disjunction concern syntactic items (conjuncts and disjuncts).

14. For abstract and strategic meaning, cf. also Hintikka & Sandu (1997: 397–398). For research on GTS and natural language, see Saarinen (1979), Hintikka & Sandu (1991), Sandu (1991), Pietarinen (2001), Clark (2012); Hintikka & Sandu (1997) offers an overview. Cf. also Janssen (2013).

15. In any event, this is the way in which Hintikka uses the word ‘Skolem function,’ see, e.g., Hintikka (1996: 31; 2002). Cf. Sandu (2001), where ‘two ways of Skolemizing’ are discussed. One of the two ways corresponds to Hintikka’s notion of Skolem function, the other corresponding to a generalized notion of strategy function. What results from the latter choice is, in Hodges’s terminology, a slash logic, not an IF logic; cf. the quote below.

16. Excluding slash logic still underdetermines the choice between several proposed formulations of IF first-order logic. Apart from formulations that use in their semantics Skolem functions, or strategy functions all of whose arguments are moves by the opponent, even different ‘epistemic interpretations’ can be considered; see Barbero (2017). Publications in which a slash logic is actually formulated – yet referred to as an IF logic – include Hyttinen & Sandu (2000), Pietarinen (2001), Väänänen (2002), Sandu (2007), Caicedo et al. (2009), Mann et al. (2011), Barbero (2013), Kontinen et al. (2014), Sevenster (2014), Barbero et al. (2021), and Barbero (2021).

17. For the term ‘regular formula,’ see Caicedo et al. (2009). The logical symbols of first-order logic considered here are negation \(({\sim})\), disjunction \((\vee)\), conjunction \((\wedge)\), existential quantifier \((\exists)\), universal quantifier \((\forall)\), identity symbol \((=)\), and parentheses. See the entry on classical logic for a detailed presentation of first-order logic.

Note that implication is not among the logical symbols of IF first-order logic. Material implication \((\phi \rightarrow \psi)\) can be defined in the so-called extended \(\mathbf{IFL}\) (Subsect. 3.4) by the formula \((\neg \phi \vee \psi)\). In the special case that \(\phi\) is ‘truth equivalent’ to a first-order formula (see Subsect. 4.2), it is possible to express \((\phi \rightarrow \psi)\) in \(\mathbf{IFL}\) by the formula \(({\sim}\phi \vee \psi)\). For different ways of treating conditionals in GTS, including conditionals in natural language, see e.g. Hintikka & Kulas (1983; Ch. 3), Hintikka & Sandu (1991).

18. In the literature, the syntax of \(\mathbf{IFL}\) is invariably given for formulas. By contrast, the semantics is often formulated for sentences only (see Hintikka 1991, 1995, 1996; Hintikka & Sandu 1996, 1997; Sandu 1993, 1994). In Sandu (1996, 1998), the semantics is given for arbitrary formulas.

19. See, e.g., Hintikka (1991, 1995, 1996), Sandu (1993, 1994); for defining GTS for \(\mathbf{FO}\) in this way, see e.g. Hintikka & Kulas (1983), cf. Hintikka (1968, 1973a). The semantics of \(\mathbf{IFL}\) to be presented will be its game-theoretical semantics, sketched in Hintikka & Sandu (1989) and Hintikka (1991) and presented in a more detailed fashion e.g. in Hintikka (1995, 1996), Sandu (1993, 1994). The semantics is defined explicitly to arbitrary formulas and variable assignments in Sandu (1996, 1998). The original approach to the GTS of first-order logic in Hintikka (1968) avoided variable assignments by letting the players name the objects they had chosen; this approach could be adapted to \(\mathbf{IFL}\) as well. Janssen (2002) and Janssen & Dechesne (2006) address the issue of whether the game-theoretical semantics of \(\mathbf{IFL}\) does justice to the idea of ‘informational independence’ among logical operators.

20. A model of vocabulary \(\tau\) is a structure comprising two components: a non-empty set \(D\) of objects termed ‘individuals’ (the domain of the model) and an interpretation function that associates each element of the vocabulary \(\tau\) with a suitable entity based on the domain (each constant symbol is mapped to an element of \(D\), each \(n\)-ary relation symbol is mapped to a subset of \(D^n\), and each \(n\)-ary function symbol is mapped to a function of type of \(D^n \rightarrow D\)). A variable assignment is a function whose domain is a given set of variables and whose values are elements of the domain of the model being considered. Models themselves are termed interpretations in the entry on classical logic. Recall that in the degenerate case that \(n = 0\), the expression \((\exists x/\forall y_1 ,\ldots ,\forall y_n)\) equals by stipulation \((\exists x)\), and similarly in the case of the other connectives followed by a slash. This is why we need not give separate clauses for \((\exists x), \vee , (\forall x)\), and \(\wedge\).

21. The notion of the strategy of a player must not be confused with the game-theoretical notion of strategy profile. The latter means a set of strategies, one strategy for each player. For semantic games, a strategy profile would be a set \(\{F_1, F_2\}\), where each \(F_i\) itself is a set, namely a set of strategy functions of player \(i\).

22. The term ‘dissatisfaction’ is used as a dual of ‘satisfaction.’ The distinction between these notions generalizes the distinction between ‘truth’ and ‘falsity.’ Hodges (1997a) conceptualizes a related distinction in his compositional framework by speaking of ‘trumps’ and ‘cotrumps.’ Hintikka (1996, Ch. 10) proposed that a ‘constructive’ interpretation could be given to IF logic by requiring that winning strategies be composed of recursive strategy functions. This idea is developed in detail in Odintsov et al. (2018).

23. To be precise, below game \(G(\phi , M)\) equals by definition game \(G(\phi , M, g_0)\), where \(g_0\) is an arbitrarily chosen variable assignment.

24. When negation symbol is allowed to appear in arbitrary syntactic positions in \(\mathbf{FO}\) formulas, it is no longer the case that universal quantifiers and conjunction symbols are automatically of universal force while existential quantifiers and disjunction symbols are of existential force. The force of an operator depends on the number of negation signs in whose syntactic scope it lies. If we wish to retain in the general setting the characteristic feature distinguishing \(\mathbf{IFL}\) from slash logic – namely the requirement that strategy functions of a player only take as arguments moves made by the adversary – the syntax must be formulated paying attention to the force that each quantifier has (cf. however Sandu 1993, 1994; Hintikka & Sandu 1997: 373). In the general formulation of \(\mathbf{IFL}\), hence formulated, an operator O can be marked as independent from any preceding quantifiers of the opposite force, but not from any preceding quantifier having the same force as O. For example \((\forall x){\sim}(\exists y)(\forall z/\forall x,\exists y) S(x, y, z)\) would be well formed, unlike \({\sim}(\forall x){\sim}(\exists y/\forall x) R(x, y)\).

25. See e.g. Hintikka (1991: 147, 2002: 409), Hodges (1997a: 546), Sandu (1993, 1994).

26. For non-determinacy and IF logic, see Hintikka (1996), Burgess (2003), Väänänen (2006).

27. No third truth-value is stipulated in the semantics of \(\mathbf{IFL}\). Truth-value gaps may arise when neither truth nor falsity can be meaningfully ascribed to a sentence (because a presupposition of the sentence is not satisfied). This is not what non-determinacy means. Non-determinacy is a model-relative complex negative property, which can be ascribed to a sentence. A sentence has this property iff neither of the simple positive properties of truth and falsity can be correctly ascribed to the sentence. An ascription of non-determinacy is correct or incorrect depending exclusively on the model relative to which the ascription is effected.

28. For ‘truth equivalence’ Hintikka uses the term ‘weak equivalence’ and for ‘logical equivalence’ the term ‘strong equivalence’ (cf. Hintikka 1996: 150). He characterizes strong equivalence as the preservation of truth and falsity. Thus if \(\psi\) and \(\chi\) are strongly equivalent, nothing prevents \(\psi\) from being non-determined in a model, as long as \(\chi\) also is. (On other occasions, e.g. in Hintikka 1991: 20, Hintikka defines ‘strong equivalence’ differently, by the requirement that either \(\psi\) and \(\chi\) are both true or both false; this precludes the possibility that one or both of two strongly equivalent sentences would be non-determined.) The term ‘truth equivalence’ used by Dechesne (2005: 32) is more descriptive. The term ‘falsity equivalence’ also stems from Dechesne. She follows Hintikka in terming ‘strong equivalence’ what is here for simplicity referred to as ‘logical equivalence’.

29. Cf. Hintikka (1996: 147), Hodges (1997a: 546), Sandu (1993, 1994).

30. In Hintikka (1996: 149) this logic is termed truth-functionally extended IF first-order logic – in contradistinction to ‘extended IF first-order logic,’ which in Hintikka (1991: 47, 1996: 149) and Hintikka & Sandu (1997) is defined as containing, in addition to \(\mathbf{IFL}\) formulas, only formulas \(\neg \phi\), where \(\phi\) is an \(\mathbf{IFL}\) formula (or sentence). The considerations that motivate the introduction of \(\neg\) in the first place, actually call for the more general syntax (witness Hintikka 1996: 149, 195–196), which is why it is natural to define extended IF first-order logic as it is done here. For extended IF first-order logic, see also Hintikka (1991: 49; 1997; 2004).

31. Cf. Hintikka (1991: 49; 1996: 147–149; 2002), Hintikka & Sandu (1997: 375), Sandu (1993, 1994).

32. Cf. Hintikka (1991, 1995, 1996, 1997), Hintikka & Sandu (1996), Sandu (1993, 1996, 1998). Analogous properties of (what on substantial criteria is) slash logic are discussed in Sandu (2007) and Mann et al. (2011); recall Hodges’s distinction between independence friendly logic and slash logic (see the beginning of Sect. 3). Properties of another related logic, Väänänen’s dependence logic, are in a mathematically detailed fashion covered in Väänänen (2007). For more information on dependence logic, see the entry on dependence logic.

33. For (existential) second-order logic, see the entry on second-order and higher-order Logic. See also van Benthem and Doets (2001).

34. Cf. the entry on the axiom of choice.

35. In Hodges (2006: 527; 2013), it is pointed out that a strengthened version of this theorem can be proven if a weakened notion of strategy is applied (cf. also Hintikka 2006a: 536). Related observations are made in Forster (2006). Namely, the standard notion of strategy employed in GTS is that of deterministic strategy: a set of single-valued functions yielding for any given tuple of arguments a unique move. A nondeterministic strategy of player 2 consists of a set of instructions, each instruction yielding a set of moves for any tuple of earlier moves by player 1. A nondeterministic strategy of player 2 is winning if it guarantees a win for player 2, regardless of which move, among those given by the strategy, player 2 makes in each case when it is her turn to move.

Theorem (without AC). (Hodges 2013) Let \(\tau\) be any vocabulary, \(M\) any \(\tau\) structure, \(g\) any variable assignment and \(\phi\) any \(\mathbf{FO}[\tau\)] formula. Then \(M, g \vDash \phi\) holds in the standard sense iff there is a nondeterministic winning strategy for player 2 in game \(G(\phi , M, g)\).

For finite partially ordered quantifiers and AC, see Krynicki & Mostowski (1995; Sect. 2).

36. The intertranslatability of the two logics is discussed in Hintikka (1991, 1996, 1997), Hintikka & Sandu (1997), Sandu (1998).

37. If \(\phi\) and \(\psi\) are atomic \(\mathbf{IFL}\) formulas, let us write \((\phi \rightarrow \psi)\) for \(({\sim}\phi \vee \psi)\), and \((\phi \leftrightarrow \psi)\) for \(((\phi \rightarrow \psi) \wedge(\psi \rightarrow \phi))\); cf. footnote 17. Further, \(x \ne y\) is used as an abbreviation of \({\sim}x=y\).

38. A Hamiltonian path on a graph is a path visiting every node exactly once. For Fagin’s theorem and references to \(\mathbf{NP}\)-complete problems, see e.g. Ebbinghaus & Flum (1999), Grädel et al. (2007), Papadimitriou (1994). For partially ordered quantifiers, partially ordered connectives, and \(\mathbf{NP}\)-complete problems, see Blass & Gurevich (1986), Hella & Sandu (1995).

39. For a discussion, see Hintikka (1991, 1995, 1996), Hintikka & Sandu (1997), Sandu (1993). Paying due attention to Hodges’s warning against confusing slash logic and IF logic, one may reconstruct proofs for various properties of \(\mathbf{IFL}\) on the basis of Väänänen’s results concerning his dependence logic (Väänänen 2007). The results pertaining to (what in substance is) slash logic discussed in (Sandu 2007) and in (Mann et al. 2011) can likewise be compared with the analogous results concerning \(\mathbf{IFL}\).

40. A complete disproof procedure is a procedure for recursively enumerating all inconsistent sentences. The term ‘complete proof procedure for inconsistency’ might involve a smaller risk of being misunderstood (cf., e.g., Quine 1970: 90). In any event, disproving must be understood as ‘establishing inconsistent,’ not as ‘establishing not provable’ (or ‘establishing not valid’).

41. For the fact that \(\mathbf{ESO}\) is not closed under negation, cf. e.g. Hinman (1978: 82).

42. For a proof phrased in terms of \(\mathbf{FPO}\), see Barwise (1979: 56, 73–74).

43. Actually, it is non-determined in all domains with at least two elements.

44. Fragments of \(\mathbf{ESO}\) have been subject to lively interest in finite model theory and complexity theory, see e.g. Ebbinghaus & Flum (1999), Grädel et al. (2007), Papadimitriou (1994). For related work on partially ordered quantifiers and connectives, see Blass & Gurevich (1986), Hella & Sandu (1995), Hella, Sevenster & Tulenheimo (2008). For the \(\mathbf{P} = \mathbf{NP}\) problem, see e.g. Fortnow (2009).

45. That there is a sound and complete proof procedure for \(\mathbf{FO}\) was first proven by Kurt Gödel (1930). There are different variants of axiomatizability. Let \(L\) be a logic, \(A\) a set of sentences of \(L\), and \(P\) a proof procedure for \(L\). Then \(A\) is an axiomatization of \(L\) relative to \(P\), if the sentences of \(L\) provable in \(P\) from the sentences of \(A\) are precisely the valid sentences of \(L\). The logic \(L\) is finitely axiomatizable (resp. recursively axiomatizable, resp. axiomatizable) relative to \(P\), if it has a finite (resp. recursive, resp. recursively enumerable) axiomatization \(A\) relative to \(P\).

46. See Hintikka (1991, 1995, 1996, 2000).

47. The theorem was proven by Boris Trakhtenbrot (1950). For Trakhtenbrot’s theorem, see Ebbinghaus, Flum & Thomas (1984). Andrzej Mostowski (1957) proved, without recourse to Trakhtenbrot’s theorem, that extending \(\mathbf{FO}\) with a quantifier capable of saying that a formula of one free variable is satisfied by finitely many elements only, results in a logic that is not axiomatizable.

48. The fact that \(\mathbf{FPO}\) fails to have a sound and complete proof procedure can be seen by reference to Trakhtenbrot’s theorem. In 1958 Ehrenfeucht showed that \(\phi_{inf}\) can be expressed in \(\mathbf{FPO}\); see Henkin (1961). From this he concluded – making use of Mostowski’s result mentioned in footnote 47 – that the Boolean closure of \(\mathbf{FPO}\) (i.e., its closure under the operations \(\neg , \wedge\), and \(\vee)\) is not axiomatizable. From Mostowski’s result the non-axiomatizability of \(\mathbf{FPO}\) itself does not follow (since the finiteness of an extension is not expressible in \(\mathbf{FPO})\).

49. See e.g. Hintikka (2006a: 65), Sandu & Hintikka (2001: 49). For compositionality and GTS, see Hintikka & Kulas (1983), Hintikka & Sandu (1997). For a discussion on different senses of compositionality and \(\mathbf{IFL}\), see Hintikka (1996), Sandu & Hintikka (2001). Cf. also the entry on compositionality.

50. See e.g. Hintikka & Kulas (1983), Hintikka (1988, 1996, 2000, 2006a).

51. See e.g. Hintikka & Kulas (1983), Hintikka (1988, 1996, 2000).

52. See e.g. Hintikka & Kulas (1983), Hintikka (1988, 1996, 2000), Hintikka & Sandu (1997).

53. See e.g. Hintikka & Kulas (1983), Hintikka (1988, 1995, 1996).

54. Barwise (1979) suggested that a compositional semantics must satisfy the condition that the relation ‘\(M \vDash \phi\)’ be an inductive verifiability relation in the sense of Barwise & Moschovakis (1978). He proved that \(\mathbf{FPO}\) does not admit of a compositional semantics subject to this condition. Hodges (1997a) finds the condition suggested by Barwise unmotivated. It rather begs the question: in order for a relation to be an inductive verifiability relation, the relevant inductive clauses must be first-order. That they cannot be first-order in connection with \(\mathbf{FPO}\) is hardly surprising; cf. Hodges (2007: 118). Hintikka had on many occasions stated that there is no realistic hope of formulating compositional truth-conditions for \(\mathbf{IFL}\) sentences (Hintikka 1991, 1995, 1996; see also Hintikka & Sandu 1997). Hodges (1997a,b) wanted to prove Hintikka’s statement wrong. The syntax Hodges opted for is that of slash logic (cf. Sect. 3 and Subsect. 6.1). Since Hodges considers variants of slash logic, his results are not, strictly speaking, about \(\mathbf{IFL}\). However, it is clear that the framework of Hodges (1997b) can be adapted to the syntax of \(\mathbf{IFL}\) proper.

55. It was pointed out already in Hintikka & Kulas (1983: 20) that at least in some cases compositionality can be restored by resorting to higher-order entities, specifically to functions embodying strategies of player 2. In the same connection it was noted that such higher-order entities are much less realistic philosophically and psycholinguistically than the original individuals. See also Zadrozny (1995), Janssen (1997), Hodges (1998); cf. Westerståhl (1998), Sandu & Hintikka (2001).

56. Note that \((N, \TRUE^N)\) is an expansion of \(N\) to the vocabulary \(\tau \cup \{\TRUE\}\). For the notion of expansion, see the supplementary document.

57. For details about truth-definitions of \(\mathbf{FO}\), see the entry on Tarski’s truth definitions; further, see e.g., Kaye (1991), Sandu (1998), Väänänen (2007).

58. The proof of this result is sketched in Hintikka (1991, 1996), and later in more detail in Sandu (1998). See also Hintikka (1998, 2001), Hyttinen & Sandu (2000), Sandu & Hyttinen (2001), Väänänen (2007). For a technically analogous result, see Hodges’s comments about self-applied truth-predicates for \(\Sigma_n\) formulas in Azriel Levy’s set-theoretical hierarchy (the entry on Tarski’s truth definitions); see also de Rouilhan and Bozon’s (2006: 700) comments about John Myhill’s and Craig Smorynski’s similar results.

59. If one attempts to construct Liar’s paradox for \(\mathbf{IFL}\), the assertion that the Liar sentence is true will itself be non-determined (Hintikka 1991: 44–51, 1996: 142; cf. Väänänen 2007: 108–109).

60. See also Hintikka (1996: 106–108; 2001: 23–24; 2006a: 65–66).

61. See Hintikka (1996: 123–125; 2001), Hintikka & Sandu (1997).

62. Enderton (1970) proved that the logic \(L^*\) obtained from \(\mathbf{FO}\) by closing it under arbitrary Henkin quantifiers, as well as under the operations \(\neg , \wedge\), and \(\vee\), can be translated into the so-called \(\Delta^1_2\) fragment of second-order logic. (For this fragment, see, e.g., Hinman 1978.) Marcin Mostowski (1991) showed that in fact \(L^*\) does not suffice to cover \(\Delta^1_2\); cf. Krynicki & Mostowski (1995: 217). Now, (1) \(\mathbf{EIFL}\) has the same expressive power as the Boolean closure of \(\mathbf{ESO}\) (i.e., its closure under \(\neg , \wedge\), and \(\vee)\), (2) the Boolean closure of \(\mathbf{ESO}\) has the same expressive power as the Boolean closure of \(\mathbf{FPO}\), and (3) the Boolean closure of \(\mathbf{FPO}\) is a fragment of \(L^*\). Therefore we may conclude that \(\mathbf{EIFL}\) is strictly weaker than the \(\Delta^1_2\) fragment of second-order logic.

63. The standard interpretation in the sense of Henkin (1950) construes second-order quantifiers as follows. If \(R\) is an \(n\)-ary relation symbol, \(f\) is an \(n\)-ary function symbol, and \(\rM\) is a domain, then under the standard interpretation of second-order logic, the second-order quantifiers \((\exists R)\) and \((\forall R)\) range over all (extensionally possible) subsets of \(\rM^n\), and the second-order quantifiers \((\exists f)\) and \((\forall f)\) range over all (extensionally possible) functions from \(\rM^n\) to \(\rM\).

64. Similar requirements need be expressed concerning eventual second-order quantifiers \((\exists f)\).

65. See Hintikka (1955; 1991: 47–48; 1995: 12–13; 2006a: 476–477), and especially Hintikka (1996: 194–195). For details about the reduction of the validity problem of full second-order logic to that of \(\mathbf{ESO}\), see e.g. Leivant (1994: Subsect. 5.6).

66. For an algebraic study of slash logic, see Mann (2007).

67. For the relation of Jónsson and Tarski’s Theorem 3.14 to modal logic, cf. the entry on Arthur Prior.

68. For these observations relating the propositional part of \(\mathbf{EIFL}\), the modal logic \(\mathbf{S4}\), and intuitionistic propositional logic, see Hintikka (2004b; 2006a: 471).

69. See Hintikka (1991; 1995; 1996: 129,190,198,201,205; 2000: 133; 2002a: 409; 2006a: 472). It may be of interest to note that Quine (1970: 90) affirms without hesitation that \(\mathbf{FPO}\) formulas are not ontologically committed to higher-order entities (even if their expressive power goes beyond \(\mathbf{FO})\). On the same basis Quine would, no doubt, have accepted that \(\mathbf{IFL}\) is only committed to first-order entities. (Quine’s reasons for not considering \(\mathbf{FPO}\) as a logic were related to its non-axiomatizability; cf. Subsect. 4.3.) For ontological commitments of \(\mathbf{FPO}\) formulas, see also Patton (1991). For the status of \(\mathbf{FPO}\) as a first-order logic, cf. Hintikka & Kulas (1983: 50).

70. See the entry on generalized quantifiers.

71. For, in a play of the semantic game for the formula \(Q_{\ge \kappa}z P(z)\) and the model \(M\), player 2 would choose a function \(f : \kappa \rightarrow\) M, whereafter player 1 would choose ordinals \(\alpha\) and \(\beta\) with \(\alpha \lt \beta \lt \kappa\). Player 2 would win iff \(f(\alpha) \ne f(\beta)\) and the individuals \(f(\alpha)\) and \(f(\beta)\) satisfy the predicate \(P\). (In order to win, player 2 must select an injective function whose all values satisfy \(P\).)

72. Cf. Subsect. 4.6. For details, see e.g. Leivant (1994: Subsect. 5.6).

73. Both sets are \(\Pi_2\) complete; for \(\Pi_2\) completeness, see e.g. Väänänen (2007; Ch. 7).

74. Cf. Feferman (2006: 461,463), Hintikka (1996: 129,193,198).

75. Cf., e.g., Hintikka (1991; 1995; 2002: 407; 2006a: 40–41).

76. Together with witnesses for disjunction symbols, likewise depending in general on the values chosen for the preceding universal quantifiers.

77. For the argument, see Hintikka (1996; 1998; 2004a; 2006a: 74).

78. For limited formal truth definitions for set theory, see the entry on Tarski’s truth definitions.

79. These individuals are ‘sets’ only in the sense that they belong to a domain of a model of an axiomatic set theory; they are not sets in the sense in which the entities over which second-order quantifiers range are sets (namely sets of individuals of the domain considered).

80. See e.g. Hintikka (1996: 172–177; 1998: 319–323, 326–32; 2006a: 74). For the continuum hypothesis, and Gödel’s and Cohen’s independence results, see the entry on set theory.

81. See Hintikka (1991: 47–48; 1996: 192–193); see also Väänänen (2007: 139–141).

82. See Hintikka (1986; 1993; 1996: 208–209). The axiom of completeness appears in the second edition (1903) of Hilbert (1898). Saying that a model \(M\) is maximal requires, at least on the face of it, quantification over individuals (or sets) outside the domain of \(M.\)

83. Actually, Hintikka sees it as a conceptual confusion to speak of ‘axiomatizations’ in connection with logic as well as mathematical theories. In the former case, when possible, an axiomatization is simply a recursive enumeration of validities of the logic considered. By contrast, one can view an axiomatization of a mathematical theory as a way of compressing all the truths (not logical truths or validities) about the subject matter of the theory into a finite or recursively enumerable set of axioms (Hintikka 1996: 1–4).

84. Quantifiers occurring in conjoint constituents, quantifiers occurring in different nested \(of\) phrases, and relative clauses with several antecedents; see Hintikka (1973a, 1976a, 1979).

85. For a discussion, see e.g. Peters & Westerståhl (2006: 66–72) and the literature referred to there.

86. This is because the set of valid \(\mathbf{FPO}\) sentences is not recursively enumerable. As Hintikka himself recognizes, to produce a rigorous argument, it would be necessary to show for an arbitrary \(\mathbf{FPO}\) sentence \(Q\phi\), not only that there is an English sentence that is naturally represented using the prefix \(Q\), but also that the grammatical constructions used allow an English counterpart of \(\phi\): whether the formula \(Q\phi\) can be translated to \(\mathbf{FO}\) crucially depends on the matrix \(\phi\).

87. The example is from Hintikka (1982); in this paper Hintikka does not use the slash sign. By reference to Hintikka’s theory of the semantics of questions (Hintikka 1976b), Carlson and ter Meulen (1979) called attention to wh-questions formed out of suitable sentences with a branching quantifier reading, and argued that the desideratum of such a question will involve informational independence of the usual quantifiers from the intensional know-construction.

88. In epistemic logic, the knowledge operator \(K_a\) is construed as a universal modal operator ranging over scenarios compatible with the knowledge of the agent \(a\) considered. For further information, see the entry on epistemic logic.

89. The impossibility to express the condition \(K_I (\forall x)(\exists y/K_I)\) admires\((x, y)\) in \(\mathbf{FPO}\) is pointed out in both Carlson & ter Meulen (1979) and Hintikka (1982). Here the existential quantifier depends on the universal quantifier but not on the knowledge operator, while the knowledge operator must precede the universal quantifier in order for the formula to imply the presupposed de dicto sentence ‘I know that everybody admires someone.’ According to the formula \((\forall x) K_I (\exists y/K_I)\) admires\((x, y)\), the agent’s knowledge would pertain to all actual individuals and it would merely imply that the agent knows of all actually existing individuals that each of them admires someone. If it is compatible with the agent’s knowledge that there are further individuals beside those which happen to exist actually, this would not guarantee the truth of the de dicto sentence.

90. Cf. Hintikka (1982, 1987, 1990), Engdahl (1986). For the uses of Skolem functions and related ideas in linguistics – notably the so-called choice functions – see e.g. Reinhart (1997), von Heusinger (2004), Steedman (2012). In logical terms, a choice function is a function taking a formula of one free variable as its argument and returning as its value an individual that satisfies this formula – if at least one such individual exists.

91. In Hintikka & Sandu (1989: 575–576) it is said that informational independence is a relation between applications of game rules, but also that it is a relation that a move prompted by an expression in a semantic game bears to a number of earlier moves prompted by further expressions (cf. also Hintikka & Sandu 1997: 367). The latter construal complies with the way informational independence is understood in game theory, while the former led to some confused examples in Hintikka and Sandu’s paper (examples about neg-raising, pp. 577–580, see also Hintikka 1990, Sandu 1993).

92. The belief operator \(B_a\) is a universal modal operator, just like the knowledge operator \(K_a\); its range is the set of scenarios compatible with all that the agent \(a\) believes in the scenario relative to which the sentence is evaluated (cf. footnote 88).

93. Cf. Hintikka & Sandu (1989: 584–585, 587–589), Hintikka (1990). Some exceptions were noted in Hintikka (1973a), cf. footnote 84. However, even when informational independence can be syntactically indicated, the indicators are different from case to case.

94. Note that the slash-logical prefix \( (\forall x)(\exists u)(\forall y)(\exists v/x,u) \) can be expressed in IF logic simply by \( (\forall x)(\exists u)(\forall y)(\exists v/\forall x) \). By contrast, the identity symbol is needed to translate the slash-logical prefix \( (\forall u)(\exists v)(\exists w/u) \) into IF logic: a construction such as \( (\forall u)(\exists v)(\forall t)(\exists w/\forall u) (t=v \rightarrow \ldots)\) can be used.