Stanford Encyclopedia of Philosophy

Notes to Independence Friendly Logic

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), Mostowski & Krynicki (1995), Pietarinen (2001); for dependent quantifiers, see also Quine (1970).

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. Portoraro's entry on Automated Reasoning in this encyclopedia. On how they are employed in linguistics, cf. footnote 107.

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 ∃y depending on the interpretation of ∀x, and similarly g provides a witness for ∃w depending on the interpretation of ∀z.

8. Henkin introduced the general idea of dependent quantifier Qm, 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. FPO is not syntactically closed under negation, conjunction, or disjunction.

10. For a critique, see Hodges (2006a).

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, ∃ and ∀, 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. There are also significant differences between the Skolem functions and strategy functions of player 2, cf. Hodges (2006b: 527–528). Under the general game-theoretical definition, strategy functions are allowed to make use of all previous moves of either player (not merely moves by the opponent), and even to employ information from other sources.

14. 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).

15. 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 (2007); Hintikka & Sandu (1997) offers an overview.

16. 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.

17. Excluding slash logic still underdetermines the choice between several proposed formulations of IF first-order logic. However, all these formulations use in their semantics Skolem functions, or strategy functions all of whose arguments are moves by the opponent. Publications where 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, Dechesne & Janssen (2009). Virtually all attempts to formulate IF versions of logics other than first-order logic have resulted in slash logics (even if called IF logics). Cases in point are formulations of IF propositional logic in Sandu & Pietarinen (2001), Sevenster (2006b); IF modal logic in Bradfield & Fröschle (2002), Tulenheimo (2003), Hyttinen & Tulenheimo (2005), Tulenheimo & Sevenster (2006), Sevenster (2006a); and IF fixpoint logic, Bradfield (2004).

18. The logical symbols of first-order logic considered here are negation (~), disjunction (∨), conjunction (∧), existential quantifier (∃), universal quantifier (∀), and parentheses. A vocabulary (signature, non-logical terminology) is any countable set τ of relation symbols (each of which carries a fixed arity), function symbols (again each with a fixed arity) and constant symbols. See Shapiro's entry on Classical Logic in this encyclopedia for a detailed presentation of first-order logic.

Note that implication is not among the logical symbols of IF first-order logic. Material implication (φ → ψ) can be defined in so-called extended IF first-order logic (Subsect. 3.4) by the formula (¬φ ∨ ψ). In the special case that φ is ‘truth equivalent’ to a first-order formula (see Subsect. 4.2), it is possible to express (φ → ψ) in IF first-order logic by the formula (~φ ∨ ψ). For different ways of treating conditionals in GTS, including conditionals in natural language, see e.g. Hintikka & Kulas (1983; Ch. 3), Hintikka & Sandu (1991).

19. This is the syntax of what Hintikka (1991: 43) terms strong IF first-order logic. The syntax has been presented in Hintikka (1991), Hintikka & Sandu (1997), Sandu (1998).

20. In the literature, the syntax of IF first-order logic (as opposed to slash logic) 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.

21. The simpler syntax is considered in Hintikka (1991, 1996), Hintikka & Sandu (1996). In the terminology of Hintikka (1991: 43), it is the syntax of weak IF first-order logic.

22. In Sandu (1994), condition (1) is replaced by a condition admitting arbitrary first-order formulas, but clauses (2) to (5) are kept intact. Sandu (1993) and Hintikka (1995) consider the further rule allowing to replace a token of (∃x), occurring in a formula in the scope of a number of conjunction symbols which include ∧1,…,∧n, by (∃x/∧1,…,∧n), together with its dual rule. A conceptual problem with this suggestion was revealed by Hodges (1997a: 546–548); for a discussion see Sect. 6. In Hintikka (1990), Hintikka & Sandu (1989) and Sandu (1993), the idea was entertained that a quantifier (or a modal operator) could be marked as independent of a preceding negation symbol. The semantic implementation of this idea was not convincing, and has been left out from subsequent presentations of IF logic. Negation is game-theoretically interpreted in terms of role switch, and hence does not correspond to a choice made by a player. Therefore the expression (∀y/~) cannot be interpreted in a way analogous to ‘indepedence’ of an operator involving a choice by one of the players. This is not to say that one could not attach a meaning to the expression (∀y/~). However, whatever the interpretation, it will not be an instance of a universal quantifier being informationally independent of a negation sign.

23. See, e.g., Hintikka (1991, 1995, 1996), Sandu (1993, 1994); for defining GTS for FO in this way, see e.g. Hintikka & Kulas (1983), cf. Hintikka (1968, 1973a). The semantics of IF first-order logic 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 IF first-order logic as well.

24. Janssen (2002) and Janssen & Dechesne (2006) address the issue of whether the game-theoretical semantics of IF first-order logic does justice to the idea of ‘informational independence’ among logical operators.

25. Models (τ structures) are termed interpretations in Shapiro's entry on Classical Logic in this encyclopedia. Recall that in the degenerate case that n = 0, the expression (∃x/∀y1,…,∀yn) equals by stipulation (∃x), and similarly in the case of the other connectives followed by a slash. This is why we need not give separate clauses for (∃x), ∨, (∀x), and ∧. If g is a variable assignment, g[x/a] is the variable assignment which is otherwise like g but maps the variable x to the object a.

26. 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 {F1, F2}, where each Fi itself is a set, namely a set of strategy functions of player i.

27. 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 framework by speaking of ‘trumps’ and ‘cotrumps.’

28. To be precise, below game G(φ, M) equals by definition game G(φ, M, g0), where g0 is an arbitrarily chosen variable assignment.

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

30. No third truth-value is stipulated in the semantics of IF first-order logic. 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.

31. For ‘truth equivalence’ Hintikka uses the term ‘weak equivalence’ and for ‘equivalence’ the term ‘strong equivalence’ (cf. Hintikka 1996: 150). He characterizes strong equivalence as the preservation of truth and falsity. Thus if ψ and χ are strongly equivalent, nothing prevents ψ from being non-determined in a model, as long as χ also is. (On other occasions, e.g. in Hintikka 1991: 20, Hintikka defines ‘strong equivalence’ differently, by the requirement that either ψ and χ 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 ‘equivalence’.

32. If ψ is a sentence that is non-determined in at least one model, ψ is not a strong consequence of itself – but is its own logical consequence. For notions of consequence, cf., e.g., Hintikka (1991: 20; 1996: 161). In Subsect. 3.4, extended IF first-order logic with a new negation symbol ¬ is introduced. Using both negations ¬ and ~, the several notions of equivalence and consequence can be explicated. Sentences ψ and χ are truth equivalent if the sentence (¬ψ ∨ χ) ∧ (¬χ ∨ ψ) of extended IF first-order logic is valid, and they are equivalent if the sentence (¬ψ ∨ χ) ∧ (¬χ ∨ ψ) ∧ (¬~ψ ∨ ~χ) ∧ (¬~χ ∨ ~ψ) is valid. Further, χ is a logical consequence of ψ if the sentence (¬ψ ∨ χ) is valid, and χ is a strong consequence of ψ if (~ψ ∨ χ) is valid. While both truth equivalence and equivalence are analyzable in terms of logical consequence, neither is analyzable in terms of strong consequence.

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

34. Following Hintikka (1991: 43), the sentences φ+ and φ– can be called the positive and negative reduct of the sentence φ, respectively. These notions are readily generalizable to arbitrary IF first-order formulas. For explicitly separating the truth-condition and falsity-condition of an IF sentence, cf. Dechesne (2005). Concentrating on the restricted syntax (cf. Subsect. 3.1) is not restrictive from the viewpoint of expressiveness. For an arbitrary sentence φ of the official syntax there is a truth equivalent sentence φ+ of the restricted syntax. Furthermore, an arbitrary sentence φ of the official syntax is false iff the sentence ~φ of the liberalized syntax is true iff a negation normal form [~φ]* of ~φ (which is a sentence of the official syntax) is true iff the sentence ([~φ]*)+ of the restricted syntax is true.

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

36. 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 of IF first-order formulas, only formulas ¬φ, where φ is an IF first-order formula (or sentence). The considerations that motivate the introduction of ¬ 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). For the crucial restriction that ¬ may not occur in the scope of a quantifier, see Hintikka (1991: 49; 1996: 148). For counterexamples to this restriction see, however, Hintikka (1996: 148; 2002c).

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

38. 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); recall Hodges's distinction between independence friendly logic and slash logic (see 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).

39. For (existential) second-order logic, see Enderton's entry on Second-order and Higher-order Logic in this encyclopedia.

40. For the Axiom of Choice (AC), see Jech's entry on Set Theory in this encyclopedia.

41. In Hodges (2006a, 2006b: 527), 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 2006: 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 2006a) Let τ be any vocabulary, M any τ structure, g any variable assignment and φ any FO[τ] formula. Then M, g ⊨ φ holds in the standard sense iff there is a nondeterministic winning strategy for player 2 in game G(φ, M, g).

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

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

43. Recall that if φ contains disjunction symbols, the skolemization sk[φ] uses a fresh constant symbol 0 (not appearing in φ) when explicating the dependence of disjunctions on the preceding universal quantifiers. (Cf. the supplementary document.)

44. If φ is a formula, the xi and variables, and the ti are terms, by stipulation φ[x1/t1,…, xn/tn] stands for the formula obtained from φ by replacing all free occurrences of xi in φ by ti. This use of the slash sign must not be confused with its use to mark quantifier independence as in IF logic.

45. For the proof, see also Krynicki & Mostowski (1995: 215–216).

46. A Hamiltonian path on a graph is a path visiting every node exactly once. For Fagin's theorem and references to NP-complete problems, see e.g. Ebbinghaus & Flum (1999), Grädel et al. (2007), Papadimitriou (1994). For partially ordered quantifiers, partially ordered connectives, and NP-complete problems, see Blass & Gurevich (1986), Hella & Sandu (1995). In Sandu (1997) it is shown how to express in IF first-order terms NP-complete problems known to be expressible using partially ordered quantifiers and connectives.

47. If φ and ψ are IF first-order formulas, let us write (φ → ψ) for (~φ ∨ ψ), and (φ ↔ ψ) for ((φ → ψ) ∧ (ψ → φ)); cf. footnote 18.

48. 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 IF first-order logic on the basis of Väänänen's results concerning his dependence logic (Väänänen 2007). Likewise Sandu's survey of results for (what in substance is) slash logic can be compared to the analogous results concerning IF first-order logic (Sandu 2007).

49. Here ‘↔’ is defined as explained in footnote 47; cf. footnote 18.

50. For Beth's definability theorem, and explicit and implicit definability, see, e.g., Hodges (1993), Smullyan (1995).

51. 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’).

52. For the fact that ESO is not closed under negation, cf. e.g. Odifreddi (1989: 381).

53. For a proof phrased in terms of FPO, see Barwise (1979: 56, 73–74).

54. In Hintikka & Kulas (1983; Ch. 4) it is similarly argued that negation formation in natural languages is an essentially semantic operation and that no complete and effective syntactic rules for negation formation exist.

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

56. Fragments of ESO are 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), Gottlob (1997), Hella, Sevenster & Tulenheimo (2008).

57. For the distinction between verbal and sentential negation, see, e.g., Klima (1964), Jackendoff (1969), Sandu (1994). For a discussion on the connection between that distinction and the distinction between dual and contradictory negation, see Hintikka (1991, 2002c), Sandu (1994).

58. Cf. footnote 36. For the argument that there are no recursive formation rules for contradictory sentential negation in English, see Hintikka & Kulas (1983). For contradictory negation, IF logic, and natural language, see Hintikka (1991, 1996, 2002c), Hintikka & Sandu (1989, 1997), Sandu (1994). Among further phenomena of interest in connection with GTS and the analysis of negation in natural languages is contradictory negation functioning as a barrier to anaphora (cf. Heim 1982; Hintikka 1991, 1996, 2002; Hintikka & Sandu 1997). The analysis of anaphora in GTS was introduced in Hintikka & Kulas (1985); see also Hintikka & Sandu (1991).

59. That there is a sound and complete proof procedure for 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.

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

61. 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 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.

62. The fact that FPO fails to have a sound and complete proof procedure can be seen by reference to Trakhtenbrot's theorem. In 1958 Ehrenfeucht showed that φinf can be expressed in FPO; see Henkin (1961). From this he concluded – making use of Mostowski's result mentioned in footnote 61 – that the Boolean closure of FPO (i.e., its closure under the operations ¬, ∧, and ∨) is not axiomatizable. From Mostowski's result the non-axiomatizability of FPO itself does not follow (since the finiteness of an extension is not expressible in FPO).

63. See e.g. Hintikka (2006: 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 IF first-order logic, see Hintikka (1996), Sandu & Hintikka (2001). Cf. also Szabó's entry on Compositionality in this encyclopedia.

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

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

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

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

68. Barwise (1979) suggested that a compositional semantics must satisfy the condition that the relation ‘M ⊨ φ’ be an inductive verifiability relation in the sense of Barwise & Moschovakis (1978). He proved that 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 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 IF first-order 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). Slashed quantifiers appear in the form (∃x/y) rather than (∃x/∀x), and the variable ‘y’ in the quantifier (∃x/y) may be bound by an existential quantifier ∃y, not necessarily by a universal quantifier ∀y. The result of replacing any number of existential quantifiers (∃x) in an FO formula by the expression (∃x/y1,…, yn), for any variables y1,…, yn, is a formula of slash logic. So even expressions such as (∃x/y)P(x, y) are formulas. Since Hodges considers variants of slash logic, his results are not, strictly speaking, about IF first-order logic. However, it is clear that the framework of Hodges (1997b) can be adapted to the syntax of IF first-order logic proper. For semantics of slash logic, see also Väänänen (2002).

69. Like Hodges (1997a,b), Väänänen (2002) also considers slash logic. Väänänen's semantic games of perfect information could, however, be adapted so as to apply to IF first-order logic.

In Hodges's semantics, evaluation is relative to sets of variable assignments. Similarly, in Väänänen's semantic games the players operate with such higher-order objects when making moves. E.g., a move corresponding to an existential quantifier is a function mapping sets of variable assignments to sets of variable assignments, subject to suitable further constraints. In Hintikka's semantic games of imperfect information, quantifier independence is modeled by restrictions on winning strategies. In Väänänen's games of perfect information, again, it is implemented directly on the level of plays, this being possible due to the higher-order setting Väänänen assumes.

70. 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).

71. Note that (N, TRUEN) is an expansion of N to the vocabulary τ ∪ {TRUE}.

72. For details about truth-definitions of FO, see Hodges's entry on Tarski's Truth Definitions in this encyclopedia; further, see e.g. Kaye (1991), Sandu (1998), Väänänen (2007).

73. 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 Σn formulas in Azriel Levy's set-theoretical hierarchy (Hodges's entry on Tarski's Truth Definitions in this encyclopedia); see also de Rouilhan and Bozon's (2006: 700) comments about John Myhill's and Craig Smorynski's similar results.

74. If one attempts to construct Liar's paradox for IF first-order logic, 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).

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

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

77. See Hintikka (1996: 12–13,129,198). As Hintikka sees it, the set existence problems would arise from the need of ascending to the metalanguage level when defining the truth predicate – not from the need of theorizing in terms of notions like logical truth, which for its meaning requires considering the totality of all models of a given vocabulary. Cf. footnote 78.

78. Actually de Rouilhan & Bozon (2006) go further and argue that Hintikka has not only failed to show that one can use IF first-order languages to define their own model theory; they suggest that in order for a language to be properly self-sufficient for truth theory, the model-theoretical criterion of adequacy should be expressible internally to that language.

In order to express the model-theoretical criterion of adequacy one must be able to express the notion of logical truth (validity); de Rouilhan & Bozon (2006) show that the notion of logical truth for IF first-order logic is not definable in IF first-order logic itself. Hintikka (2006: 710–711) agrees that de Rouilhan and Bozon are ‘technically right when they say that their results show that not all metatheory of an IF language can be done in that same language.’ However, he maintains that results about a metatheoretical notion such as validity do not belong to the theory of truth to begin with. (Instead, he says that validity can be viewed as an archetypal modal notion, and that its study belongs to the theory of modal logic.) Hintikka therefore disagrees with de Rouilhan and Bozon about internal expressibility of adequacy as a criterion for a successful truth theory. By contrast Hintikka (2006) does not explicitly respond to de Rouilhan and Bozon's attack on the possibility of using IF first-order languages to develop their own model theory. For Hintikka's line of thought concerning his ‘declaration of independence of model theory,’ cf. footnote 77. (For related issues, see Subsections 5.1 and 5.3.)

79. By a result of Enderton (1970), it follows that the Boolean closure of all formulas of ESO (i.e., its closure under the operations ¬, ∧, and ∨) can be translated into the so-called Δ12 fragment of second-order logic. (For this fragment, see, e.g., Ebbinhaus & Flum 1999 or Odifreddi 1989.) By a result of Marcin Mostowski (1991) it further follows that the Boolean closure of ESO does not suffice to cover Δ12; cf. Krynicki & Mostowski (1995: 217). It may be concluded that extended IF first-order logic is strictly weaker than the Δ12 fragment of second-order logic.

80. 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 M is a domain, then under the standard interpretation of second-order logic, the second-order quantifiers (∃R) and (∀R) range over all (extensionally possible) subsets of Mn, and the second-order quantifiers (∃f) and (∀f) range over all (extensionally possible) functions from Mn to M.

81. Similar requirements need be expressed concerning eventual second-order quantifiers (∃f).

82. See Hintikka (1955; 1991: 47–48; 1995: 12–13; 2006: 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 ESO, see e.g. Leivant (1994).

83. For an algebraic study of IF first-order logic, see Mann (2007). For a comparison with partial logics, see Sandu (1996, 1998), Hintikka & Sandu (1997), Sandu & Pietarinen (2001). Cf. also Sect. 6 (IF propositional logic) and especially footnote 111.

84. For the relation of Jónsson and Tarski's Theorem 3.14 to modal logic, cf. Copeland's entry on Arthur Prior in this encyclopedia.

85. For these observations relating the propositional part of extended IF first-order logic, the modal logic S4, and intuitionistic propositional logic, see Hintikka (2004b; 2006: 471).

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

87. See Westerståhl's entry on Generalized Quantifiers in this encyclopedia. Cf. also Gärdenfors (1987), Peters & Westerståhl (2006).

88. For, in a play of the semantic game for the formula Q≥κz P(z) and the model M, player 2 would choose a function f : κ → M, whereafter player 1 would choose distinct ordinals α, β < κ. Player 2 would win iff f(α) ≠ f(β) and the individual f(α) satisfies the predicate P.

89. Cf. Subsect. 4.6. For details, see e.g. Leivant (1994).

90. Both sets are Π2 complete; for Π2 completeness, see, e.g., Väänänen (2007; Ch. 7).

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

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

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

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

95. For limited formal truth definitions for set theory, see Hodges's entry on Tarski's Truth Definitions in this encyclopedia.

96. 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).

97. See e.g. Hintikka (1996: 172–177; 1998: 319–323, 326–32; 2006: 74). For the continuum hypothesis, and Gödel's and Cohen's independence results, see Jech's entry on Set Theory in this encyclopedia.

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

99. 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.

100. 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).

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

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

103. This is because the set of valid FPO sentences is not recursively enumerable. As Hintikka himself recognizes, to produce a rigorous argument, it would be necessary to show for an arbitrary FPO sentence Qφ, 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 φ: whether the formula Qφ can be translated to FO crucially depends on the matrix φ.

104. 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.

105. In epistemic logic, the knowledge operator Ka is construed as a universal modal operator ranging over scenarios compatible with the knowledge of the agent a considered. For further information, see Hendricks & Symons's entry on Epistemic Logic in this encyclopedia.

106. This 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 it to be interpreted de dicto.

107. 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. Kratzer (1995), Reinhart (1997), Winter (1997), von Heusinger (2004), Schlenker (2006). 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.

108. 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); cf. the remarks on negation in footnote 22.

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

110. A precursor of a kind of IF propositional logic that results from Hodges's observations – one in which conjunctions and disjunctions are taken to be restricted quantifiers – is the logic of partially ordered connectives introduced in Sandu & Väänänen (1992) and anticipated by Blass & Gurevich (1986).

111. Let K be any class of two-valued truth-value distributions over a given class of propositional atoms. (a) Let f : K → {0,1,?} be any three-valued truth function. Then f is captured by a sentence φ of IF propositional logic (without contradictory negation), in the sense that for all M ∈ K, the truth-value of φ in M equals f(M). (b) Let f : K → {0,1,?,!} be any four-valued truth function. Then f is captured by a sentence φ of IF propositional logic (with contradictory negation): for all M ∈ K, the truth-value of φ in M equals f(M). For details, see Sandu & Pietarinen (2001). Here the object ? can be understood as the value undefined and the object ! as the value over-defined.

112. See Slogan 1 in Blackburn et al. (2001: xi). For different modal-like logics, see the following entries in this encyclopedia: Deontic Logic (McNamara), Epistemic Logic (Hendricks & Symons), Intensional Logic (Fitting), Modal Logic (Garson), Propositional Dynamic Logic (Balbiani), Provability Logic (Verbrugge), Temporal Logic (Galton).

113. See e.g. Hintikka (1976b, 1982, 1999, 2003), Hintikka & Halonen (1995).

114. The belief operator Ba is a universal modal operator, just like the knowledge operator Ka; 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 105).

115. According to the analysis of Hintikka & Sandu (1989), the de re reading of ‘Alice believes that the king of France is tall’ would be captured by the relevant IF logical formula. This is not quite correct, however, since there is nothing in the semantics of BAlice tall(k / BAlice) that forces the individual c functioning as the constant denotation of ‘k’ to exist in the actual world.

In Hintikka & Sandu (1989) the idea of marking predicates as independent of preceding modal operators is also explored; and an analysis of backwards-looking operators attempted. The suggestions related to backwards-looking operators are, however, misguided. To see this, recall what backwards-looking operators are. In standard modal logic, every modal operator is evaluated relative to the scenario that was used to interpret the immediately preceding modal operator (if any exists). Hence in O1O2O3 p the operator O3 is evaluated relative to the scenario w2 interpreting O2. A backwards-looking operator is a modal operator that refers back to some specific preceding modal operator; it is then evaluated relative to the scenario interpreting that operator (see e.g. Saarinen 1978, Hintikka & Kulas 1983). E.g., if B3 is a backwards-looking operator syntactically specified to refer back to the predecessor of its syntactic predecessor, then in O1O2B3 p it is evaluated relative to the scenario w1 interpreting O1. The combination of IF first-order logic and modal logic can study dependence relations between quantifiers, modal operators, and non-logical symbols (singular terms, predicates); however, this framework does not have a mechanism for switching to an earlier scenario introduced by modal evaluation. Such a mechanism is actually incorporated in hybrid logic; cf. Braüner's entry on Hybrid Logic in this encyclopedia.

116. See Tulenheimo (2003), Hyttinen & Tulenheimo (2005), Sevenster (2006a), Tulenheimo & Sevenster (2006, 2007).

117. The strategy functions corresponding to modal operators are invariably thought of as taking any previous moves as arguments: the arguments are not automatically restricted to the opponent's moves.