## 1. Introduction: Quantifier Dependence



In mathematical prose, one can say things such as 'for all real
numbers \(a\) and for all positive real numbers \(\varepsilon\), there
exists a positive real number \(\delta\) depending on \(\varepsilon\)
but not on \(a\), such that...' What is important here is
quantifier dependence. The existential quantifier 'there exists
\(\delta\)' is said to depend on the universal quantifier
'for all \(\varepsilon\)' but not on the universal
quantifier 'for all \(a\).' It was an essential part of
Karl Weierstrass's (1815-1897) work in the foundations of
analysis that he defined the notions of limit, continuity, and
derivative in terms of quantifier
 dependence.[1]
 For a concrete example, a function \(f : D \rightarrow \mathbf{R}\)
is *continuous*, if for all \(a\) in the set \(D\) and for all
\(\varepsilon \gt 0\) there exists \(\delta \gt 0\) such that for all
\(x\) in \(D\), if \(|x - a| \lt \delta\), then \(|f(x) - f(a)| \lt
\varepsilon\). The definition of *uniform continuity* is
obtained from that of continuity by specifying that the quantifier
'there exists \(\delta\)' depends only on the quantifier
'for all \(\varepsilon\),' not on the quantifier
'for all
 \(a\).'[2]



*Independence friendly first-order logic* (a.k.a. *IF
first-order logic*, *IF logic*) was introduced by Jaakko
Hintikka and Gabriel Sandu in their article 'Informational
Independence as a Semantical Phenomenon' (1989); other early
sources are Hintikka's booklet *Defining Truth, the Whole
Truth, and Nothing but the Truth* (1991) and Sandu's Ph.D.
thesis
 (1991).[3]
 IF first-order logic is an extension of first-order logic, involving
a specific syntactic device '/' (slash, independence
indicator), which has at the object language level the same effect as
the meta-level modifier 'but does not depend on' has in
the example just considered. In the notation of IF logic, the logical
form of the statement that a function \(f\) is uniformly continuous
would be \((\forall a)(\forall \varepsilon)(\exists \delta /\forall
a)(\forall x) R\), to be contrasted with the form of the statement
that \(f\) merely is continuous, \((\forall a)(\forall
\varepsilon)(\exists \delta)(\forall x) R\).



In the introductory examples in the present and the following section,
let us confine attention to formulas in *prenex form*: a string
of quantifiers followed by a quantifier-free first-order formula. If
in a first-order sentence of such a form an existential quantifier
\(\exists y\) lies in the syntactic scope of a universal quantifier
\(\forall x\), then by the semantics \(\exists y\) automatically
depends on \(\forall x\). This is so *e.g.* with the sentence
\((\forall x)(\exists y) R(x, y)\). The dependence of \(\exists y\) on
\(\forall x\) means that the *witness* of \(\exists y\) may
vary with the value interpreting \(\forall x\). In order for the
sentence to be true in a model \(M\), it suffices that there be a
function \(f\) such that \(R(a, f(a))\) holds in \(M\), for any \(a\)
interpreting \(\forall x\). Such functions, spelling out the
dependencies of witnesses for existential quantifiers on
interpretations of universal quantifiers, are known in logical
literature as *Skolem
 functions*.[4]
 For comparison, in the sentence \((\exists y)(\forall x) R(x, y)\)
the quantifier \(\exists y\) does not depend on the quantifier
\(\forall x.\) For this sentence to be true in \(M\), one and the same
witness \(c\) for \(\exists y\) must be good against any
interpretation \(a\) of \(\forall x\), so that \(R(a, c)\) holds in
\(M\). The corresponding Skolem function is a
 constant.[5]



In IF first-order logic, syntactic scopes no longer determine the
semantic relation of dependence. In the sentence \((\forall x)(\forall
y)(\exists z/\forall y) R(x, y, z)\), for instance, \(\exists z\) is
syntactically subordinate to both \(\forall x\) and \(\forall y\), but
is marked as independent of \(\forall y\), and is hence dependent only
on \(\forall x\). Semantically this means that the witness of
\(\exists z\) must be given by a function taking as an argument the
interpretation of \(\forall x\), but not that of \(\forall y\). In
order for \((\forall x)(\forall y)(\exists z/\forall y) R(x, y, z)\)
to be true in \(M\), there must be a function \(f\) of one argument
such that \(R(a, b, f(a))\) holds in \(M\), for any \(a\) interpreting
\(\forall x\) and any \(b\) interpreting \(\forall y\).



What is gained with the slash notation? After all, clearly
*e.g.* \((\forall x)(\forall y)(\exists z/\forall y) R(x, y,
z)\) is true in a model \(M\)
 iff[6]
 the first-order sentence \((\forall x)(\exists z)(\forall y) R(x, y,
z)\) is true therein. As a matter of fact, the expressive power of IF
logic exceeds that of first-order logic. Consider the sentence
\((\forall x)(\exists y)(\forall z)(\exists w/\forall x) R(x, y, z,
w)\). Its truth-condition is of the following form: there are
one-argument functions \(f\) and \(g\) such that \(R(a, f(a), b,
g(b))\) holds in \(M\), for any \(a\) interpreting \(\forall x\) and
\(b\) interpreting \(\forall
 z\).[7]
 So the sentence is true iff the following sentence (\*) containing a
*finite partially ordered quantifier* is true:

 
\[\tag{\*}
\begin{matrix}
\forall x \exists y \\
\forall z \exists w
\end{matrix}
R(x,y,z,w)
\]


For, by definition (\*) is true in a model \(M\) iff the second-order
sentence \((\exists f)(\exists g)(\forall x)(\forall z) R(x, f(x), z,
g(z))\) is true therein. The latter may be termed the *Skolem
normal form* of (\*). It says that Skolem functions providing
witnesses for the quantifiers \(\exists y\) and \(\exists w\) in (\*)
exist. Finite partially ordered quantifiers - a.k.a. *Henkin
quantifiers* or *branching quantifiers* - were
proposed by Leon Henkin (1961) and have been subsequently studied
 extensively.[8]
 They are two-dimensional syntactic objects

 
\[\begin{matrix}
Q\_{11} \ldots Q\_{1n} \\
\vdots \\
Q\_{m1} \ldots Q\_{mn}
\end{matrix}\]


where each \(Q\_{ij}\) is either \(\exists x\_{ij}\) or \(\forall
x\_{ij}\). They are naturally interpreted by making systematic use of
Skolem functions.



Let us denote by \(\mathbf{FPO}\) the logic of finite partially
ordered quantifiers obtained from first-order logic as follows: if
\(\phi\) is a first-order formula and \(\mathbf{Q}\) is a finite
partially ordered quantifier, then \(\mathbf{Q}\phi\) is a formula of
 \(\mathbf{FPO}\).[9]
 With \(\mathbf{FPO}\) it is possible to express properties that are
not definable in first-order logic. The first example was provided by
Andrzej Ehrenfeucht (cf. Henkin 1961): a sentence that is true in a
model iff the size of its domain is infinite. It turns out that
\(\mathbf{FPO}\) can be translated into IF logic (see
*Subsect*. 4.1). Therefore IF logic is more expressive than
first-order logic.



The deepest reason for IF logic, as Hintikka saw it, is that the
relations of dependence and independence between *quantifiers*
are the only way of expressing relations of dependence and independence
between *variables* on the first-order level (Hintikka 1996:
34-35, 73-74; 2002a: 404-405; 2006a: 71, 515). To
understand this remark properly, recall that relations of quantifier
(in)dependence are *semantic* relations, but *syntactically
expressed*. More precisely, in IF logic the (in)dependence
relations are syntactically expressed by the interplay of two factors:
syntactic scope and the independence indicator '/'. In a
given sentence, an existential quantifier \(\exists x\), say, depends
on precisely those universal quantifiers within whose scope \(\exists
x\) lies, but of which \(\exists x\) is not marked as independent
using the slash sign. What Hintikka means when he speaks of
(in)dependence relations between variables, are *functional
dependencies* between quantities in a model. The kinetic energy of
a material body depends on its mass and its speed, but does not depend
on the particular material body being considered. This fact can be
expressed in IF logic by the sentence



\((\forall b)(\forall m)(\forall v)(\exists e/\forall b)\)(if \(b\) is
a material body which moves at the velocity \(v\) and has the mass
\(m\), then the kinetic energy \(e\) of \(b\) equals \(\frac{1}{2}
mv^2 )\). 



That this sentence states the existence of a functional dependence of
kinetic energy on mass and speed is particularly clearly seen from the
fact that if the sentence is true, the unique Skolem function for the
quantifier \(\exists e\) actually *is* the physical law
connecting masses, speeds and kinetic energies (cf. Hintikka 1996:
34-35).



While first-order logic can only express some relations between
variables, IF first-order logic with its greater expressive power can
express more. Actually, IF logic is calculated to capture all such
relations (Hintikka 1996: 75-77; 2002a: 404-405; 2002b:
197; 2006a: 72). This idea must, in its full generality, be seen as
programmatic. For a more general framework, cf. Hintikka (2006a: 515,
536, 752; 2008), Sandu & Sevenster (2010), Sandu (2013), Sandu
(2014).



Among philosophical issues that have been addressed in connection with
IF logic are the reconstruction of mathematical reasoning on the
first-order level (Hintikka 1996, 1997), definability of a
self-applied truth predicate (Hintikka 1991, 1996, 2001; Sandu 1998),
truth and axiomatic set theory (Hintikka 1996, 2004a), and insights
into the nature of negation (Hintikka 1991, 1996, 2002; Hintikka &
Sandu 1989; Sandu 1994). These issues will be discussed in
*Sections* 4 and 5.


## 2. The Background of IF Logic: Game-theoretical Semantics


### 2.1. Semantic games



Inspired by Ludwig Wittgenstein's idea of a language-game,
Hintikka (1968) introduced the basic framework of what came to be
known as *game-theoretical semantics* (a.k.a. GTS). The basic
lesson Hintikka adopts from Wittgenstein is that words - in
particular quantifiers - are associated with activities that
render them meaningful: words often have meaning only in the context
of certain types of action (Hintikka 1968: 55-56). Wittgenstein
said that by 'language-game' he means 'the whole,
consisting of language and the actions into which it is woven'
(Wittgenstein 1953: I, *Sect.* 7).



It becomes natural to ask which are the activities that go together
with quantifiers. As Hintikka explains (see Hintikka 2006a: 41, 67),
Wittgenstein had taken it as a criterion for something to be an object
that it can be looked for and found. Applying this idea to quantifiers
with such objects as values, Hintikka was led to formulate
*semantic games* for quantifiers. Crucially, these semantic
games can be formulated as games in the strict sense of game theory;
but at the same time they are exact codifications of language-games in
Wittgenstein's sense, at least if one accepts that the
activities associated with quantifiers are 'looking for'
and
 'finding.'[10]



Semantic games \(G(\phi , M)\) for first-order sentences \(\phi\) are
two-player zero-sum games of perfect information, played on a given
model \(M\). Let us call the two players simply player 1 and player
 2.[11]
 The games are most easily explained for sentences in prenex form.
Universal quantifiers mark a move of player 1, while existential
quantifiers prompt a move by player 2. In both cases, the relevant
player must choose an individual from the domain \(\rM\) of
 \(M\).[12]
 If

 
\[
\phi = (\forall x)(\exists y)(\forall z)(\exists w) R(x, y, z, w),
\]


the game is played as follows. First, player 1 picks out an individual
\(a\), whereafter player 2 chooses an individual \(b\). Then player 1
proceeds to choose a further individual \(c\), to which player 2
responds by picking out an individual \(d\). Thereby a play of the
game has come to an end. The tuple \((a, b, c, d)\) of individuals
chosen determines the winner of the play. If the quantifier-free
formula \(R(a, b, c, d)\) holds in \(M\), player 2 wins, if not,
player 1 wins.



The fact that one of the players wins a single play of game \(G(\phi ,
M)\) does not yet tell us anything about the truth-value of the
sentence \(\phi\). Truth and falsity are characterized in terms of the
notion of *winning strategy*. The sentence \((\forall
x)(\exists y)(\forall z)(\exists w) R(x, y, z, w)\) is *true*
in \(M\) if there is a winning strategy for player 2 in the game just
described: a recipe telling player 2 what to do, when (a specified
amount of) information about the opponent's earlier moves is
given. Technically, the requirement is that there be *strategy
functions* \(f\) and \(g\), such that for any choices \(a\) and
\(c\) by player \(1, R(a, f(a), c, g(a, c))\) holds in \(M\). Observe
that strategy function \(f\) is a Skolem function for the quantifier
\(\exists y\) in \(\phi\), and similarly \(g\) is a Skolem function
for the quantifier \(\exists w\). The sentence \(\phi\) is
*false* in \(M\) if there is a winning strategy (set of
strategy functions) for player 1 in the corresponding game: a constant
\(c\) and a function \(h\) such that for any choices \(b\) and \(d\)
by player \(2, R(c, b, h(b), d)\) fails to hold in \(M\).



Game-theoretical interpretation of quantifiers was already suggested by
Henkin (1961; cf. Hintikka 1968: 64). Henkin also pointed out, in
effect, the connection between a full set of Skolem functions and a
winning strategy for player 2. Hintikka (1968) noted that conjunctions
are naturally interpreted by a choice between the two conjuncts, made
by player 1; similarly, disjunctions can be interpreted by a choice by
player 2 between the two
 disjuncts.[13]
 Further, Hintikka proposed to interpret negation as a transposition
of the roles of 'verifier' and 'falsifier'
(for more details, see *Subsect.* 3.2). 



The game-theoretical description of semantic games does not mention
the activities of searching and finding; for such an abstract
description it suffices to speak of the players making a move. Also,
the characterization of truth and falsity as the existence of a
winning strategy for player 2 and player 1, respectively, does not
refer to efforts on the part of the players - say efforts to
establish truth or to find witnesses. The truth or falsity of a
sentence is a matter of 'combinatorics': it is an issue of
the existence of a set of functions with certain properties (cf.
Hintikka 1968, 1996; Hodges 2013). So what happened to the original
philosophical conception according to which the meanings of
quantifiers are tied to the activities of searching and finding?
Hintikka's idea is that asserting a sentence involving
quantifiers is to make a claim about what can and what cannot happen
when a certain language-game is played; using language involving
quantifiers requires mastering the rules of the corresponding semantic
games (Hintikka 1968: *Sect.* 8, 1996: 128, 2006a: 538). What
is the content of such a claim in connection with the sentence
\(\forall x\exists y R(x, y)\)? That whichever individual player 1
chooses from the domain for \(\forall x\), player 2 can find a witness
individual for \(\exists y\). In other words, given a value for
\(\forall x\) (which itself can be seen as the result of the search by
player 1), if player 2 is allowed to search free from any practical
constraints, she will find a value for \(\exists y\) so that player 2
wins the resulting play. Even though semantic games themselves can be
defined without recourse to activities such as looking for or finding,
these activities play an important conceptual role when the language
user reasons *about* these games.



Hintikka (1973a) initiated the application of GTS to the study of
natural language. This work was continued notably by Hintikka &
Kulas (1983, 1985), where game-theoretical rules for such items as
negation, anaphoric pronouns, genitives, tenses, intensional verbs,
certain prepositional constructions, and proper names were given, and
the distinction between abstract meaning and strategic meaning
 drawn.[14]



### 2.2. Imperfect information



The framework of GTS enables asking questions of a game-theoretical
nature about semantic evaluation. Hintikka (1973a) observed that
semantic games with imperfect information are devised without any
difficulty. As logical examples he used \(\mathbf{FPO}\) sentences.
(For examples related to natural languages, see *Subsect*.
5.4.)



From the vantage point of GTS, independence friendly first-order logic
differs from first-order logic in that semantic games correlated with
formulas of the former are, in general, games of imperfect
information, while any game associated with a first-order formula is a
game of perfect information. Consider the game for \(\forall x\exists
y\forall z(\exists w/\forall x) R(x, y, z, w)\), played on a model
\(M\). A play of this game proceeds exactly as plays of the game
corresponding to \(\forall x\exists y\forall z\exists w R(x, y, z,
w)\). First, player 1 chooses an individual \(a\), whereafter player 2
chooses an individual \(b\). Then player 1 proceeds to pick out a
further individual \(c\), to which player 2 responds by choosing an
individual \(d\). So a play of the game has come to an end. The play
is won by player 2, if indeed \(R(a, b,c, d)\) holds in \(M\);
otherwise it is won by player 1. But \(\exists w\) was marked as
independent of \(\forall x\) - why does not this fact show in
any way in the course of a play?



One might be tempted to add to the description of a play:
'player 2 chooses a value for \(\exists w\) in ignorance of the
value for \(\forall x\).' However, such a paraphrase would not
clarify the conceptual situation. It makes no sense to speak of the
independence of a move from other given moves with reference to a
single play; this can only be done with reference to a multitude of
plays. Quantifier independence can be conceptualized in
game-theoretical terms making use of the notion of *strategy*.
In the example, a strategy of player 2 is a set \(\{f, g\}\) of
strategy functions, function \(f\) providing a value for \(\exists y\)
depending on the value of \(\forall x\), and function \(g\) providing
a value for \(\exists w\) depending on the value chosen for \(\forall
z\) but not on the value chosen for \(\forall x\). The strategy \(\{f,
g\}\) is, then, a winning strategy for player 2, iff \(R(a, f(a), c,
g(c))\) holds in \(M\), for all values \(a\) chosen for \(\forall x\)
and \(c\) chosen for \(\forall z\). One precise way of implementing
the idea that player 2 is 'ignorant' of the move player 1
made for \(\forall x\) is to say that **(a)** strategy
functions always only take as arguments the opponent's moves,
and **(b)** the strategy function corresponding to
\(\exists w\) may not take as its argument the move player 1 made for
\(\forall x\).



A sentence of IF first-order logic is by definition true in a model
\(M\) iff there is a winning strategy for player 2 in the correlated
game, and false iff there is a winning strategy for player 1 in the
correlated game. There are sentences which under these criteria are
neither true nor false; they are called *non-determined* (see
*Subsect.* 3.3).



In Hintikka's judgement, the game-theoretical semantics of
quantifiers can be taken to have the same rationale that was mentioned
as the deepest reason for IF first-order logic at the end of
*Section* 1: GTS is a method of representing, on the
first-order level, the (in)dependence relations between variables by
means of informational (in)dependence in the sense of game theory
(Hintikka 1991: 12-13, 2006a: 535).


## 3. The Syntax and Semantics of IF First-order Logic



In the literature one can find essentially different formulations of
'IF first-order logic.' The differences are not restricted
to syntax - examples of applying different semantic ideas can be
found as well. 



As already noted, there is a systematic connection between the Skolem
functions and strategy functions of player 2. In connection with
formulas in prenex form, a Skolem function for an existential
quantifier is a function of the values assigned to the preceding
*universal* quantifiers, but *not* a function of the
values assigned to the preceding existential
 quantifiers.[15]
 Skolem functions are strategy functions taking as arguments
exclusively moves made by player 1. Generally a strategy for a player
in a two-player game *can* perfectly well make use of the
previous choices of either player. Hodges (2007) stresses that it
makes a difference on which notion - Skolem function or strategy
function - the semantics of imperfect information is based.
Hodges (1997a) adopted the notational convention of writing, say,
\((\exists y/x)\) where Hintikka writes \((\exists y/\forall x)\),
hence marking the difference between semantic games formulated in
terms of arbitrary strategy functions and those whose strategy
functions are in effect Skolem functions; the variable \(x\) in
\((\exists y/x)\) can be 'bound' by any syntactically
preceding quantifier carrying the variable \(x\). Hodges proposed to
employ the former formulation, while in Hintikka (1991, 1995, 1996,
2002) and Sandu (1993, 1994) the latter formulation is employed.
Hodges (2007: 119) writes:



> 
> [W]e refer to the logic with my notation and the general game
> semantics as *slash logic*. During recent years many writers in
> this area (but never Hintikka himself) have transferred the name
> 'IF logic' to slash logic, often without realising the
> difference. Until the terminology settles down, we have to beware of
> examples and proofs that don't make clear which semantics they
> intend.
> 



The distinction that Hodges makes between slash logic and IF logic
serves to bring order to the mishmash of different formulations of IF
first-order logic to be found in the
 literature.[16]


### 3.1. Syntax



IF first-order logic is an extension of first-order logic. Now, any
first-order formula is equivalent to a first-order formula in which no
variable occurs both free and bound, and in which no two nested
quantifiers carry the same variable. Formulas meeting these two
syntactic conditions will be termed *regular*. Henceforth we
systematically restrict attention to regular first-order
 formulas.[17]
 A *vocabulary* (signature, non-logical terminology) is any
countable set \(\tau\) of relation symbols (each of which carries a
fixed arity), function symbols (again each with a fixed arity), and
constant symbols. The first-order logic of vocabulary \(\tau\) will be
referred to as \(\mathbf{FO}[\tau]\). It is assumed here that among
the logical symbols of first-order logic there is the *identity
symbol* (=). The identity symbol is syntactically a binary
relation symbol, but its semantic interpretation is fixed in a way
that the interpretations of the items in the non-logical terminology
are not.



A formula of \(\mathbf{FO}[\tau]\) is in *negation normal
form*, if all occurrences of the negation symbol \({\sim}\)
immediately precede an atomic formula. The set of *formulas* of
IF first-order logic of vocabulary \(\tau\) (or
\(\mathbf{IFL}[\tau])\) can be defined as the smallest set such
that:


1. If \(\phi\) is a formula of \(\mathbf{FO}[\tau]\) in negation
normal form, \(\phi\) is a formula.
2. If \(\phi\) is a formula and in \(\phi\) a token of \((\exists
x)\) occurs in the syntactic scope of a number of universal
quantifiers which include \((\forall y\_1),\ldots ,(\forall y\_n)\), the
result of replacing in \(\phi\) that token of \((\exists x)\) by
\((\exists x/\forall y\_1 ,\ldots ,\forall y\_n)\) is a formula.
3. If \(\phi\) is a formula and in \(\phi\) a token of \(\vee\)
occurs in the syntactic scope of a number of universal quantifiers
which include \((\forall y\_1),\ldots ,(\forall y\_n)\), the result of
replacing in \(\phi\) that token of \(\vee\) by \((\vee /\forall y\_1
,\ldots ,\forall y\_n)\) is a formula.
4. If \(\phi\) is a formula and in \(\phi\) a token of \((\forall
x)\) occurs in the syntactic scope of a number of existential
quantifiers which include \((\exists y\_1),\ldots ,(\exists y\_n)\), the
result of replacing in \(\phi\) that token of \((\forall x)\) by
\((\forall x/\exists y\_1 ,\ldots ,\exists y\_n)\) is a formula.
5. If \(\phi\) is a formula and in \(\phi\) a token of \(\wedge\)
occurs in the syntactic scope of a number of existential quantifiers
which include \((\exists y\_1),\ldots ,(\exists y\_n)\), the result of
replacing in \(\phi\) that token of \(\wedge\) by \((\wedge /\exists
y\_1 ,\ldots ,\exists y\_n)\) is a formula.



Clauses (2) and (3) allow the degenerate case that the list of
universal quantifiers is empty \((n = 0)\). The resulting expressions
\((\exists x\)/) and \((\vee\)/) are identified with the usual
existential quantifier \((\exists x)\) and the usual disjunction
\(\vee\), respectively. Similar stipulations are made about clauses
(4) and (5).



In a suitable vocabulary, each of the following is a formula:


* \((\forall x)(\forall y)(\exists z/\forall x) R(x, y, z, v)\),
* \((\forall x)(\forall y)(x = y \; (\vee /\forall x) \; Q(x,
y))\),
* \((\exists x)(S(x) \; (\wedge /\exists x) \; T(x))\),
* \((\forall x)(\exists y)(\forall z/\exists y)(\exists v/\forall
x) R(x, y, z, v)\).



By contrast, none of the following sequences of symbols is a
formula:


* \((\exists y/\forall x) P(x, y)\),
* \((\exists x)(\exists y/\exists x) P(x, y)\),
* \((\forall x)(\forall y/\forall x) P(x, y)\),
* \((\forall x)(S(x) \; (\vee /\exists y) \; T(x))\).



If \(\phi\) is an \(\mathbf{IFL}\) formula, generated by the above
clauses from some \(\mathbf{FO}\) formula \(\phi^\*\), the *free
variables* of \(\phi\) are simply the free variables of
\(\phi^\*\). \(\mathbf{IFL}\) formulas without free variables are
\(\mathbf{IFL}\)
 *sentences*.[18]


### 3.2. Semantics



Defining the semantics of a logic using GTS is a two-step process. The
first step is to define the relevant *semantic games*. The
second step is to define the notions of 'true' and
'false' in terms of the semantic games; this happens by
reference to the notion of *winning strategy*. Semantic games
may be defined by specifying recursively the alternative ways in which
a game associated with a given formula \(\phi\) can be
 begun.[19]



For every vocabulary \(\tau\), \(\mathbf{IFL}[\tau]\) formula
\(\phi\), model \((\tau\) structure) \(M\), and variable assignment
\(g\), a two-player zero-sum game \(G(\phi , M, g)\) between player 1
and player 2 is
 associated.[20]
 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\).


1. If \(\phi = R(t\_1 ,\ldots ,t\_n)\) and \(M, g \vDash R(t\_1 ,\ldots
,t\_n)\), player 2 wins (and player 1 loses); otherwise player 1 wins
(and player 2 loses).
2. If \(\phi = t\_1 = t\_2\) and \(M, g \vDash t\_1 = t\_2\), player 2
wins (and player 1 loses); otherwise player 1 wins (and player 2
loses).
3. If \(\phi = {\sim}R(t\_1 ,\ldots ,t\_n)\) and \(M, g \not\vDash
R(t\_1 ,\ldots ,t\_n)\), player 2 wins (and player 1 loses); otherwise
player 1 wins (and player 2 loses).
4. If \(\phi = {\sim}t\_1 = t\_2\) and \(M, g \not\vDash t\_1 = t\_2\),
player 2 wins (and player 1 loses); otherwise player 1 wins (and
player 2 loses).
5. If \(\phi = (\psi \; (\wedge /\exists y\_1 ,\ldots ,\exists y\_n) \;
\chi)\), player 1 chooses \(\theta \in \{\psi ,\chi \}\) and the rest
of the game is as in \(G(\theta , M, g)\).
6. If \(\phi = (\psi \; (\vee /\forall y\_1 ,\ldots ,\forall y\_n) \;
\chi)\), player 2 chooses \(\theta \in \{\psi ,\chi \}\) and the rest
of the game is as in \(G(\theta , M, g)\).
7. If \(\phi = (\forall x/\exists y\_1 ,\ldots ,\exists y\_n)\psi\),
player 1 chooses an element \(a\) from \(\rM\), and the rest of the
game is as in \(G(\psi , M, g[x/a]\)).
8. If \(\phi = (\exists x/\forall y\_1 ,\ldots ,\forall y\_n)\psi\),
player 2 chooses an element \(a\) from \(\rM\), and the rest of the
game is as in \(G(\psi , M, g[x/a]\)).



Observe that the independence indications play no role in the game
rules. Indeed, quantifier independence will be implemented on the
level of strategies. 



If a token of \((\vee /\forall y\_1 ,\ldots ,\forall y\_n)\) or
\((\exists x/\forall y\_1 ,\ldots ,\forall y\_n)\) appears in the
formula \(\phi\) in the scope of the universal quantifiers \(\forall
y\_1 ,\ldots ,\forall y\_n,\forall z\_1 ,\ldots ,\forall z\_m\) (and only
these universal quantifiers), a *strategy function* of player 2
for this token in game \(G(\phi , M, g)\) is any function \(f\)
satisfying the following:



The arguments of \(f\) are the elements \(a\_1 ,\ldots ,a\_m\) that
player 1 has chosen so as to interpret the quantifiers \(\forall z\_1
,\ldots ,\forall z\_m\). The value \(f(a\_1 ,\ldots ,a\_m)\) is the left
or the right disjunct when the token is a disjunction; and an element
of the domain when the token is an existential quantifier. 



The notion of the strategy function of player 1 for tokens of
\((\wedge /\exists y\_1 ,\ldots ,\exists y\_n)\) and \((\forall
x/\exists y\_1 ,\ldots ,\exists y\_n)\) can be defined dually. Strategy
functions are construed as Skolem functions - the more general
notion of strategy function operative in slash logic is not considered
here (cf. the beginning of *Sect.* 3 and *Subsect.*
6.1). Quantifier independence will be implemented directly in terms of
the *arguments* of the strategy functions.



A *strategy* of player 2 in game \(G(\phi , M, g)\) is a set
\(F\) of her strategy functions, one function for each token of
\((\vee /\forall y\_1 ,\ldots ,\forall y\_n)\) and \((\exists x/\forall
y\_1 ,\ldots ,\forall y\_n)\) appearing in \(\phi\). Player 2 is said to
*follow* the strategy \(F\), if for each token of \((\vee
/\forall y\_1 ,\ldots ,\forall y\_n)\) and \((\exists x/\forall y\_1
,\ldots ,\forall y\_n)\) for which she must make a move when game
\(G(\phi , M, g)\) is played, she makes the move determined by the
corresponding strategy function. A *winning strategy* for
player 2 in \(G(\phi , M, g)\) is a strategy \(F\) such that against
any sequence of moves by player 1, following strategy \(F\) yields a
win for player 2. The notions of strategy and winning strategy can be
similarly defined for player
 1.[21]



The *satisfaction* and *dissatisfaction* of the
\(\mathbf{IFL}\) formula \(\phi\) in the model \(M\) under the
assignment \(g\) are then *defined* as
 follows:[22]


* **(Satisfaction)** \(\phi\) is satisfied in \(M\)
under \(g\) iff there is a winning strategy for player 2 in game
\(G(\phi , M, g)\).
* **(Dissatisfaction)** \(\phi\) is dissatisfied in
\(M\) under \(g\) iff there is a winning strategy for player 1 in game
\(G(\phi , M, g)\).



As with \(\mathbf{FO}\), variable assignments do not affect the
(dis)satisfaction of sentences, *i.e.*, formulas containing no
free variables. Indeed, we may
 define:[23]


* **(Truth)** \(\phi\) is true in \(M\) iff there is a
winning strategy for player 2 in game \(G(\phi , M)\).
* **(Falsity)** \(\phi\) is false in \(M\) iff there is
a winning strategy for player 1 in game \(G(\phi , M)\).



The fact that \(\phi\) is true in \(M\) will be denoted by '\(M
\vDash \phi\).' Writing \(M \not\vDash \phi\) indicates, then,
that \(\phi\) is not true in \(M\). This does *not* mean that
\(\phi\) would in the above-defined sense be false in \(M\). As
mentioned in the end of *Section* 2, there are semantic games
in which neither player has a winning strategy.



The syntax of \(\mathbf{IFL}\) can be generalized by removing the
restriction according to which the negation sign may only appear as
prefixed to an atomic
 formula.[24].
 In order to interpret negation in GTS, two *roles* are added
as a new ingredient in the specification of the games: those of
'verifier' and 'falsifier.' Initially, player
1 has the role of 'falsifier' and player 2 that of
'verifier.' The roles may get switched, but only for one
reason: when an occurrence of the negation symbol is encountered. All
clauses defining semantic games must be rephrased in terms of roles
instead of players. It is the player whose role is
'verifier' who makes a move for disjunctions and
existential quantifiers, and similarly the player whose role is
'falsifier' who moves for conjunctions and universal
quantifiers. When a formula \({\sim}\psi\) is encountered, the players
change roles and the game continues with \(\psi\). Finally, if the
encountered atomic formula is true, 'verifier' wins and
'falsifier' loses, otherwise the payoffs are reversed. The
negation \({\sim}\) is variably referred to as *strong
negation*, *dual negation*, or *game-theoretical
 negation*.[25]
 It works as one would expect: \(\phi\) is false in \(M\) iff its
negation \({\sim}\phi\) is true therein (cf. Sandu 1993). 


### 3.3. Basic properties and notions



**Failure of bivalence.** There are sentences \(\phi\) of
\(\mathbf{IFL}\) and models \(M\) such that \(\phi\) is neither true
nor false in \(M\). Consider evaluating the sentence \((\forall
x)(\exists y/\forall x) x = y\) on a model whose domain has exactly
two elements, \(a\) and \(b\). Player 1 has no winning strategy. If he
chooses \(a\) to interpret \(\forall x\), he loses the play in which
player 2 chooses \(a\) to interpret \((\exists y/\forall x)\).
Similarly, if player 1 chooses \(b\), he loses the play in which
player 2 likewise chooses \(b\). Neither does player 2 have a winning
strategy. Her strategy functions for \((\exists y/\forall x)\) are
constants (zero-place functions). There are two such constants
available: \(a\) and \(b\). Whichever one of these strategy functions
player 2 assumes, there is a move by player 1 defeating it. If player
2 opts for \(a\), player 1 wins the play in which he chooses \(b\);
and if player 2 applies \(b\), player 1 wins the play in which he
chooses \(a\). Game \(G(\phi , M)\) is *non-determined*:
neither player has a winning
 strategy.[26]
 The notion of non-determinacy may be extended to formulas as
well:


* **(Non-determinacy)** \(\phi\) is non-determined in
\(M\) under \(g\) iff there is no winning strategy for player 1, nor
for player 2, in game \(G(\phi , M, g)\).



In \(\mathbf{IFL}\), falsity does not ensue from non-truth. That is,
bivalence fails in \(\mathbf{IFL}\). However, it should be noted that
it does not fail due to the postulation of a third truth-value or a
truth-value gap (cf. Hintikka 1991: 20,
 55).[27]
 Rather, the failure is a consequence of the basic assumptions of the
entire semantic theory (GTS). Non-determinacy corresponds to a
structural property: the fact that certain kinds of functions do not
exist on the model considered.



Due to the failure of bivalence, the logical law of excluded middle
fails for the dual negation \({\sim}\). Actually, \(\phi\) is
non-determined in \(M\) iff \(M \not\vDash(\phi \vee{\sim}\phi)\).




**Logical equivalence.** Sentences \(\psi\) and \(\chi\)
of \(\mathbf{IFL}\) are *truth equivalent* if they are true in
precisely the same models, and *falsity equivalent* if they are
false in precisely the same models. Sentences \(\psi\) and \(\chi\)
are *logically equivalent* if they are both truth equivalent
and falsity
 equivalent.[28]
 Due to the failure of bivalence, in \(\mathbf{IFL}\) truth
equivalence does not guarantee logical equivalence. 



**Truth, falsity, and independence indications.** The
syntax of \(\mathbf{IFL}\) allows formulas in which both universal and
existential quantifiers appear slashed, *e.g.*,

 
\[
\phi : (\forall x)(\exists y/\forall x)(\forall z/\exists y) R(x, y, z).
\]


On the other hand, quantifier independence is implemented at the level
of strategies. Consequently independence indications following a
universal quantifier are vacuous, when the satisfaction of a formula
(truth of a sentence) is considered. Similarly, independence
indications following an existential quantifier are vacuous when the
dissatisfaction of a formula (falsity of a sentence) is at stake. The
sentence \(\phi\) is true in the model \(M\) iff player 2 has a
winning strategy \(F=\{c\}\) in game \(G(\phi , M)\). This, again,
means that whichever elements \(a\) and \(b\) player 1 chooses to
interpret \((\forall x)\) and \((\forall z/\exists y)\), respectively,
the constant interpretation \(c\) of \((\exists y/\forall x)\) given
by the (zero-place) strategy function \(c\) satisfies \(R(a, c, b)\)
in \(M\). But this amounts to the same as requiring that whichever
elements \(a\) and \(b\) player 1 chooses to interpret \((\forall x)\)
and \((\forall z)\), respectively, the constant interpretation \(c\)
of \((\exists y/\forall x)\) satisfies \(R(a, c, b)\) in \(M\).
Indeed, \(\phi\) is truth equivalent to a sentence containing no
slashed universal quantifiers: 



\(\phi\) is true in a model \(M\) iff the sentence \((\forall
x)(\exists y/\forall x)(\forall z) R(x, y, z)\) is true in \(M\). 



Similarly, \(\phi\) is falsity equivalent to a sentence containing no
slashed existential quantifiers: \(\phi\) is false in a model \(M\)
iff the sentence \((\forall x)(\exists y)(\forall z/\exists y) R(x, y,
z)\) is false therein.


### 3.4. Extended IF first-order logic



If \(\phi\) is a sentence of \(\mathbf{FO}\), \(\phi\) is false in a
model \(M\) iff \({\sim}\phi\) is true in \(M\) iff \(\phi\) is not
true in \(M\). By contrast, in \(\mathbf{IFL}\) falsity and non-truth
do not coincide. An extension of \(\mathbf{IFL}\) can be introduced,
where it is possible to speak of the non-truth of sentences. To this
end, let us introduce a new negation symbol, \(\neg\), referred to as
*weak negation*, *contradictory negation* or
*classical
 negation*.[29]
 The set of formulas of *extended IF first-order logic* (to be
denoted \(\mathbf{EIFL})\) is obtained from the set of formulas of
\(\mathbf{IFL}\) by closing it under the operations \(\neg\),
\(\wedge\), and
 \(\vee\):[30]


* All formulas of \(\mathbf{IFL}\) are formulas of
\(\mathbf{EIFL}\).
* If \(\phi\) and \(\psi\) are formulas of \(\mathbf{EIFL}\), then
so are \(\neg \phi , (\phi \wedge \psi)\) and \((\phi \vee
\psi)\).



So if \(\phi\) and \(\psi\) are \(\mathbf{IFL}\) formulas,
*e.g.* \(\neg \phi\) and \((\neg \phi \vee \psi)\) are
\(\mathbf{EIFL}\) formulas; by contrast \((\forall x)\neg \phi\) is
not. For the crucial restriction that \(\neg\) 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) and especially Hintikka (2006b) in which the so-called
*fully extended IF first-order logic* (**FEIFL**)
is considered. In **FEIFL**, any occurrences of \(\neg\)
are allowed which are subject to the following syntactic condition: if
(Q\(x/W)\) is a quantifier in the syntactic scope of an occurrence of
\(\neg\), then all quantifiers listed in \(W\) are likewise in the
syntactic scope of that occurrence of \(\neg\).



The semantics of an \(\mathbf{EIFL}\) formula formed by contradictory
negation is simply this:

 
\[
M, g \vDash \neg \phi \text{ iff } M, g \not\vDash \phi.
\]


From the viewpoint of GTS, the connective \(\neg\) behaves in an
unusual way. For all connectives of \(\mathbf{IFL}\), there is a game
rule (which can be seen as specifying the meaning of the connective).
For contradictory negation there is no game rule, and its semantics is
not explained in terms of plays of semantic games. A formula \(\neg
\phi\) serves to say, globally, something about an entire game
\(G(\phi , M, g)\). If \(\phi\) is a sentence, to say that \(\neg
\phi\) is true in \(M\) is to say that player 2 does *not* have
a winning strategy in game \(G(\phi , M)\). If, again, there is indeed
a winning strategy for player 2 in \(G(\phi , M)\), by stipulation
\(\neg \phi\) is false in
 \(M\).[31]



Not only is \(\neg \phi\) not itself a formula of \(\mathbf{IFL}\),
but it cannot in general even be expressed in \(\mathbf{IFL}\) (see
*Subsect.* 4.2). The law of excluded middle holds for the
contradictory negation: for all sentences \(\phi\) and all models
\(M\), indeed \(M \vDash(\phi \vee \neg \phi)\). In *Section* 5
it will be seen how Hintikka has proposed to make use of
\(\mathbf{EIFL}\) when discussing issues in the philosophy of
mathematics. 


## 4. Metalogical Properties of IF First-order Logic



The metalogical properties of \(\mathbf{IFL}\) have been discussed in
several publications, by Hintikka as well as
 Sandu.[32]
 When presenting them, reference will be made to *existential
second-order logic*
 \((\mathbf{ESO})\);[33]
 further important notions are those of the *skolemization* and
*Skolem normal form* of an \(\mathbf{IFL}\) formula. For
precise definitions of these notions,
 the supplementary document
 can be consulted. In brief, \(\mathbf{ESO}\) is obtained from
\(\mathbf{FO}\) by allowing existential quantification over relation
and function symbols in a first-order formula. The skolemization
\(\mathrm{sk}[\phi]\) of an \(\mathbf{IFL}\) formula \(\phi\) is a
*first-order* formula of a larger vocabulary. It explicates in
terms of function symbols how existential quantifiers and disjunction
symbols of \(\phi\) depend on preceding universal quantifiers. For
example, a skolemization of the \(\mathbf{IFL}\) sentence \(\phi =
(\forall x)(\exists y)(\forall z)(\exists v/\forall x)R(x, y, z, v)\)
of vocabulary \(\{R\}\) is the \(\mathbf{FO}\) sentence
\(\mathrm{sk}[\phi] = (\forall x)(\forall z)R(x, f(x), z, h(z))\) of
vocabulary \(\{R, f, h\}\). Its Skolem normal form, again, is the
\(\mathbf{ESO}\) sentence \(\mathrm{SK}[\phi] = (\exists f)(\exists
h)(\forall x)(\forall z)R(x, f(x), z, h(z))\). The first-order
sentence \(\mathrm{sk}[\phi]\) must not be confused with the
second-order sentence \(\mathrm{SK}[\phi]\). 


### 4.1. First-order logic and existential second-order logic



**Game-theoretical vs. Tarskian semantics of FO.** The
set of formulas of \(\mathbf{FO}\) is a proper subset of the set of
\(\mathbf{IFL}\) formulas. The standard semantics of \(\mathbf{FO}\)
is not the one provided by GTS, but the Tarskian semantics specifying
recursively the satisfaction relation \(M, g \vDash \phi\). If the
*Axiom of Choice* is
 assumed,[34]
 the two semantics of \(\mathbf{FO}\) coincide:



**Theorem (assuming AC).** (Hodges 1983: 94, Hintikka
& Kulas 1985: 6-7) 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 winning strategy for player 2 in game
\(G(\phi , M,
 g)\).[35]




**Relation to ESO.** \(\mathbf{IFL}\) and
\(\mathbf{ESO}\) are
 intertranslatable:[36]




**Theorem** **(assuming AC)**
\(\mathbf{ESO}\) and \(\mathbf{IFL}\) have the same expressive power.




That is, (1) for every \(\mathbf{IFL}[\tau]\) formula \(\phi\) there
is an \(\mathbf{ESO}[\tau]\) formula \(\phi'\) such that for all
\(\tau\) structures \(M\) and variable assignments \(g\), we have:
\(M, g \vDash \phi\) iff \(M, g \vDash \phi'\). Actually,
\(\mathrm{SK}[\phi]\) is a suitable \(\mathbf{ESO}\) formula. And (2)
for every \(\mathbf{ESO}[\tau]\) formula \(\psi\) there is an
\(\mathbf{IFL}[\tau]\) formula \(\psi'\) such that \(M, g \vDash
\psi\) iff \(M, g \vDash \psi'\), for all \(\tau\) structures \(M\)
and variable assignments \(g\). This follows from the fact that
\(\mathbf{ESO}\) can be translated into \(\mathbf{FPO}\) (Enderton
1970, Walkoe 1970), which again can be translated into
\(\mathbf{IFL}\).



Hintikka suggests that \(\mathbf{IFL}\) is, substantially speaking, a
*first-order* logic: the entities its quantified variables
range over are *individuals*, and so are all entities with
which the players of the semantic games operate. (See
*Subsect.* 5.1 for a discussion of this idea.) A part of the
interest of the intertranslatability theorem lies in the fact that if
Hintikka's controversial claim is accepted, this would mean that
the expressive power of \(\mathbf{ESO}\) can actually be achieved on
the first-order level.



**IFL is more expressive than FO.** The following are
examples of properties expressible in \(\mathbf{ESO}\) - and
therefore in \(\mathbf{IFL}\) - but not in \(\mathbf{FO}\):
Dedekind-infinity of the domain, non-completeness of a linear order,
ill-foundedness of a binary relation, disconnectedness of a graph,
equicardinality of the extensions of two first-order formulas
\(\phi(x)\) and \(\psi(x)\), infinity of the extension of a
first-order formula \(\phi(x)\), and the topological notion of open
set (see, *e.g.*, Hintikka 1996, Vaananen 2007).




As an example, the Dedekind-infinity of the domain may be considered.
A set \(S\) is Dedekind-infinite precisely when there exists an
injective function from \(S\) to its proper subset. Let \(\phi\_{inf}\)
be the following sentence of
 \(\mathbf{IFL}\):[37]


 
\[
(\exists t)(\forall x)(\exists z)(\forall y)(\exists v/\forall x)((x = y \leftrightarrow z = v) \wedge z \ne t).
\]


The Skolem normal form of \(\phi\_{inf}\) is 

 
\[
(\exists f)(\exists g)(\exists t)(\forall x)(\forall y)((x = y
\leftrightarrow f(x) = g(y)) \wedge f(x) \ne t).
\]


Relative to a model \(M\), this \(\mathbf{ESO}\) sentence asserts the
existence of functions \(f\) and \(g\) and an element \(t\) such that
\(f = g\) (implication from left to right), this function is injective
(implication from right to left), and its domain is the whole domain
of \(M\) but the element \(t\) does not appear in its range.
Consequently the range is a proper subset of the domain of \(M\). In
other words, the sentence \(\phi\_{inf}\) is true in a model \(M\) iff
the domain of \(M\) is infinite.



Be it still noted that when attention is restricted to *finite*
models, Ronald Fagin's famous theorem (1974) connects
\(\mathbf{ESO}\) and the complexity class \(\mathbf{NP}\): a
computational problem is solvable by an algorithm running in
non-deterministic polynomial time iff it is definable in
\(\mathbf{ESO}\) relative to the class of all finite structures. The
following are \(\mathbf{NP}\)-complete properties and hence
expressible in \(\mathbf{IFL}\), over the class of all finite models:
evenness of the domain, oddness of the domain, 3-colorability of a
graph, and the existence of a Hamiltonian path on a
 graph.[38]




**Properties in common with FO.** IF first-order logic
shares many metalogical properties with first-order
 logic.[39]



**Compactness.** A set of \(\mathbf{IFL}\) sentences has
a model iff all its finite subsets have a model. 



**Lowenheim-Skolem property.** Suppose \(\phi\) is
an \(\mathbf{IFL}\) sentence that has an infinite model, or
arbitrarily large finite models. Then \(\phi\) has models of all
infinite cardinalities. 



The separation theorem holds in \(\mathbf{IFL}\) in a strengthened
form; the 'separation sentence' \(\theta\) is in
particular a sentence of \(\mathbf{FO}\). 



**Separation theorem.** Suppose \(\phi\) is an
\(\mathbf{IFL}\) sentence of vocabulary \(\tau\), and \(\psi\) an
\(\mathbf{IFL}\) sentence of vocabulary \(\tau'\). Suppose further
that \(\phi\) and \(\psi\) have no models in common. Then there is a
*first-order* sentence \(\theta\) of vocabulary \(\tau \cap
\tau'\) such that every model of \(\phi\) is a model of \(\theta\),
but \(\theta\) and \(\psi\) have no models in common. 



It is well known that for \(\mathbf{FO}\) there is a sound and
complete proof procedure. Because a first-order sentence \(\phi\) is
inconsistent (non-satisfiable) iff its negation \({\sim}\phi\) is
valid (true in all models), trivially \(\mathbf{FO}\) also has a sound
and complete disproof
 procedure.[40]
 The latter property extends to \(\mathbf{IFL}\) (while the former
does not, see *Subsect.* 4.3):



**Existence of a complete disproof procedure.** (Hintikka
1996: 68-70, 82) The set of inconsistent \(\mathbf{IFL}\)
sentences is recursively enumerable. 


### 4.2. Intricacies of negation



In *Subsection* 3.4, the contradictory negation \(\neg\) was
distinguished from the strong negation \({\sim}\). In \(\mathbf{FO}\)
the two coincide: for any first-order sentence \(\phi\), we have \(M
\vDash{\sim}\phi\) iff \(M \vDash \neg \phi\). 



**Strong negation fails as a semantic operation.** Let us
write \([\phi]\) for the set of models of sentence \(\phi\). In the
special case of \(\mathbf{FO}\), the strong negation \({\sim}\)
clearly defines a semantic operation: whenever \(\chi\) and \(\theta\)
are sentences such that \([\chi] = [\theta]\), we have \([{\sim}\chi]
= [{\sim}\theta]\). Burgess (2003) observed that in the context of IF
logic this property is lost in a very strong sense. In fact there are
IF sentences \(\chi\) and \(\theta\) such that while \([\chi] =
[\theta]\), the sets \([{\sim}\chi]\) and \([{\sim}\theta]\) are not
only distinct but even disjoint. 



**Inexpressibility of contradictory negation.** In
\(\mathbf{IFL}\) the strong negation \({\sim}\) and the contradictory
negation \(\neg\) do *not* coincide: we may have \(M \vDash
\neg \phi\) without having \(M \vDash{\sim}\phi\). This fact by itself
still leaves open the possibility that the contradictory negation of
every sentence \(\phi\) of \(\mathbf{IFL}\) could be defined in
\(\mathbf{IFL}\), *i.e.*, that there was a sentence
\(neg(\phi)\) of \(\mathbf{IFL}\) such that \(M \vDash\) \(neg(\phi)\)
iff \(M \not\vDash \phi\), for all models \(M\). All we know by the
failure of the law of excluded middle is that not in all cases can
\(neg(\phi)\) be chosen to be \({\sim}\phi\). However, as a matter of
fact contradictory negation is inexpressible in \(\mathbf{IFL}\).
There are sentences \(\phi\) of \(\mathbf{IFL}\) such that \(\neg
\phi\) (which is a sentence of \(\mathbf{EIFL})\) is not truth
equivalent to any sentence of \(\mathbf{IFL}\). This follows from the
well-known fact that \(\mathbf{ESO}\) is not closed under negation and
\(\mathbf{IFL}\) has the same expressive power as
 \(\mathbf{ESO}\).[41]



**Strong inexpressibility of contradictory negation.** As
a corollary to the separation theorem, the result holds in a much
stronger form. If \(\phi\) and \(\psi\) are sentences of
\(\mathbf{IFL}\) such that \(M \vDash \phi\) iff \(M \not\vDash
\psi\), then each of \(\phi\) and \(\psi\) is truth equivalent to a
sentence of \(\mathbf{FO}\). Hence the contradictory negation \(\neg
\phi\) is only expressible in \(\mathbf{IFL}\) for those
\(\mathbf{IFL}\) sentences \(\phi\) that are truth equivalent to an
\(\mathbf{FO}\)
 sentence.[42]



**Determined fragment.** Let us say that an
\(\mathbf{IFL}\) sentence \(\phi\) is *determined* if it
satisfies: \(M \vDash(\phi \vee{\sim}\phi)\), for all models \(M\).
The *determined fragment* of \(\mathbf{IFL}\) is the set of
determined \(\mathbf{IFL}\) sentences. In the determined fragment
contradictory negation *is* syntactically expressible by the
strong negation. By the strong inexpressibility of contradictory
negation, the determined fragment of \(\mathbf{IFL}\) has the same
expressive power as \(\mathbf{FO}\). Membership in the determined
fragment is a sufficient but not necessary condition for an
\(\mathbf{IFL}\) sentence to have its contradictory negation
expressible in \(\mathbf{IFL}\). The sentence \((\forall y)(\exists
x/\forall y) x = y\) is not
 determined;[43]
 yet its contradictory negation \((\forall x)(\exists y) x \ne y\) is
expressible in \(\mathbf{IFL}\).



**Contradictory negation and GTS.** The truth-conditions
that GTS yields are of the form 'there are strategy functions
\(f\_1 ,\ldots ,f\_n\) such that --,' *i.e.*, it gives
rise to truth-conditions expressible in \(\mathbf{ESO}\). By the
strong inexpressibility of contradictory negation, there is no single
\(\mathbf{IFL}\) sentence, not translatable into \(\mathbf{FO}\),
whose contradictory negation has a truth-condition of that form. This
fact makes it understandable why contradictory negation should not be
expected to admit of a game-theoretical interpretation along the same
lines in which the other logical operators are interpreted. Different
ways of assigning a game-theoretical interpretation to contradictory
negation can, however, be developed. To this end, in the context of
*fully extended IF first-order logic* (**FEIFL**,
cf. Subsect. 3.4), Hintikka has proposed to use semantic games with
*subgames*. (See Hintikka 2002c, 2006b; for subgames, see
Carlson & Hintikka 1979, Hintikka & Kulas 1983.) This approach
leads to mixing the play level with the strategy level: choices of
individuals made in a subgame may depend on strategy functions chosen
in earlier subgames. In Tulenheimo (2014), a game-theoretical
semantics is formulated for the fragment of **FEIFL**
that consists of formulas in prenex form. Plays of the correlated
games do not involve choosing any second-order objects, such as
strategy functions. Contradictory negation \((\neg)\) is interpreted
by introducing an additional component in game positions: a
*mode*. At the play level, the negation \(\neg\) triggers not
only a role switch (like the dual negation \({\sim})\), but it also
involves changing the mode from positive to negative or vice versa.
The semantic effect of modes becomes visible at the strategy level:
modes regulate the way in which the truth condition of a sentence
involves existentially or universally quantifying over strategy
functions. Like independence indications, also occurrences of \(\neg\)
are, then, interpreted in terms of conditions that act on the strategy
level. For related research, see Figueira *et al.* (2011,
2014).



**Contradictory negation and finite models.** Certain
major open questions in logic and theoretical computer science can be
formulated in terms of \(\mathbf{IFL}\). It is an open question in
complexity theory whether \(\mathbf{NP} = \mathbf{coNP}\), that is,
whether the class of \(\mathbf{NP}\)-solvable problems is the same as
the class of problems whose complement is solvable in \(\mathbf{NP}\).
By Fagin's theorem (1974), this open problem can be equivalently
formulated as follows: Is \(\mathbf{IFL}\) closed under negation
*over finite models*? That is, is there for every IF sentence
\(\phi\) another IF sentence \(neg(\phi)\) such that for any finite
model \(M\), \(neg(\phi)\) is true in \(M\) iff \(\phi\) is not true
in \(M\)? Proving that the answer is negative would settle the
notorious \(\mathbf{P} = \mathbf{NP}\) problem, i.e., establish that
there are computational problems for which one can efficiently
*verify* whether a proposed solution is correct although one
cannot efficiently *find* a
 solution.[44]


### 4.3 Failure of axiomatizability



As is well known, \(\mathbf{FO}\) admits of a sound and complete proof
procedure: there is a mechanical way of generating precisely those
first-order sentences that are valid (true in all models). This fact
can also be expressed by saying that \(\mathbf{FO}\) is axiomatizable,
or that the set of valid sentences of \(\mathbf{FO}\) is recursively
 enumerable.[45]
 Due to its greater expressive power, axiomatizability *fails*
for \(\mathbf{IFL}\). In other words, \(\mathbf{IFL}\) is semantically
 incomplete.[46]



One way to show this is as follows. Suppose for the sake of
contradiction that the set of valid \(\mathbf{IFL}\) sentences is
recursively enumerable. Recall that the sentence \(\phi\_{inf}\)
discussed in *Subsection* 4.1 is true in all and only infinite
models. Note, then, that an \(\mathbf{FO}\) sentence \(\chi\) is true
in all *finite* models iff the \(\mathbf{IFL}\) sentence
\((\phi\_{inf} \vee \chi)\) is valid. Given a valid \(\mathbf{IFL}\)
sentence, it can be effectively checked whether the sentence is
syntactically of the form \((\phi\_{inf} \vee \chi)\), where \(\chi\)
is a first-order sentence. Hence the recursive enumeration of all
valid \(\mathbf{IFL}\) sentences yields a recursive enumeration of
first-order sentences \(\chi\) true in all finite models. But this
contradicts Trakhtenbrot's theorem, according to which the set
of \(\mathbf{FO}\) sentences true in all finite models is *not*
recursively
 enumerable.[47]



What is the relevance of the failure of axiomatizability of
\(\mathbf{IFL}\)? Discussing finite partially ordered quantifiers,
Quine (1970: 89-91) suggests that we should refuse to give the
status of logic to any generalization of \(\mathbf{FO}\) which does
not have a sound and complete proof procedure *both* for
validity *and* for inconsistency. For Quine, any such
generalization belongs to mathematics rather than logic. Since
\(\mathbf{FPO}\) is not axiomatizable, it falls outside the realm of
logic, thus
 delineated.[48]



Hintikka finds this type of allegation unfounded. First,
\(\mathbf{IFL}\) shares many of the important metalogical results with
\(\mathbf{FO}\) (cf. *Subsect.* 4.1). Second, just like
\(\mathbf{IFL}\), also \(\mathbf{FO}\) can be translated into
second-order logic. The only difference is that in the former case a
larger variety of quantifier (in)dependencies must be encoded by
Skolem functions than in the latter. Why would the former translation
render \(\mathbf{IFL}\) a part of mathematics while the latter would
allow \(\mathbf{FO}\) to remain a logic (Hintikka 1991: 26-27)?
Third, one must make a distinction between what is needed to
understand an \(\mathbf{IFL}\) sentence, and what is needed to
mechanically deal with the validities (logical truths) of
\(\mathbf{IFL}\). Due to its non-axiomatizability, there are no
mechanical rules for generating the set of all validities of
\(\mathbf{IFL}\). However, to understand a sentence is to know what
things are like when it is *true*, not to know what things are
like when it is *logically true* (Hintikka 1995: 13-14).
Fourth, because of non-axiomatizability, the valid inference patterns
in \(\mathbf{IFL}\) cannot be exhausted by any recursive enumeration.
Insofar as important mathematical problems can be reduced to questions
about the validity of \(\mathbf{IFL}\) formulas (*Subsect.*
5.3), progress in mathematics can be seen to consist (not of the
discovery of stronger set-theoretical axioms but) of ever more
powerful rules for establishing validity in \(\mathbf{IFL}\) (Hintikka
1996: 100; 2000: 135-136).


### 4.4 Compositionality and the failure of Tarski-type semantics



The principle of compositionality (a.k.a. Frege principle) states that
semantic attributes of a complex expression \(E\) are determined by
the semantic attributes of its constituent expressions and the
structure of \(E\). In particular, the semantic attribute of interest
(*e.g.*, truth) may be determined in terms of one or more
auxiliary semantic attributes (*e.g.*,
 satisfaction).[49]
 Hintikka has argued that compositionality amounts to *semantic
context-independence*: semantic attributes of a complex expression
depend *only* on the semantic attributes of its constituent
expressions, plus its structure - they do *not* depend on
the sentential context in which the expression is embedded. Semantic
context-independence makes it possible to carry out semantic analysis
from *inside out* - from simpler expressions to more
complex
 ones.[50]
 This is what is needed for recursive definitions of semantic
attributes - such as Tarski-type definitions of truth and
satisfiability - to be
 possible.[51]
 By contrast, the GTS analysis of sentences is an *outside in*
process: a semantic game starts with an entire sentence, and stepwise
analyzes the sentence into simpler and simpler components, eventually
reaching an atomic formula (together with an appropriate variable
assignment). Therefore GTS allows accounting for semantic
context-dependencies that violate the principle of
 compositionality.[52]



In \(\mathbf{IFL}\) an existential quantifier may depend only on
*some* of the universal quantifiers in whose scope it lies.
Accordingly, its interpretation depends on its relation to quantifiers
outside its own scope. Such an existential quantifier is
 context-dependent.[53]
 On the face of it, then, \(\mathbf{IFL}\) cannot but violate the
principle of compositionality and does not admit of a Tarski-type
truth-definition. 



Hodges (1997a,b) showed, however, that \(\mathbf{IFL}\) can be given a
compositional
 semantics.[54]
 The semantics is given by recursively defining the satisfaction
relation '\(M \vDash\_X \phi\)' (read: \(\phi\) is
satisfied in \(M\) by \(X)\), where \(X\) is a *set* of
variable assignments. While the Tarskian semantics for \(\mathbf{FO}\)
is in terms of single variable assignments, Hodges's semantics
employs sets of variable assignments. The game-theoretical semantics
of \(\mathbf{IFL}\) is captured by this compositional semantics: for
every formula \(\phi\) of \(\mathbf{IFL}\), player 2 has a winning
strategy in \(G(\phi , M, g)\) iff the condition \(M \vDash\_{\{g\}}
\phi\) holds. Due to Hodges's semantic clauses for existential
quantifiers and disjunctions involving independence indications, the
evaluation of \(\phi\) relative to the singleton set \(\{g\}\)
generally leads to evaluating syntactic components of \(\phi\)
relative to sets of (possibly infinitely) many variable assignments.
Hintikka remarks (2006a: 65) that if one is sufficiently ruthless, one
can always save compositionality by building the laws of semantic
interaction of different expressions into the respective meanings of
those
 expressions.[55]



It is methodologically worth pointing out that compositionality is not
*needed* for defining \(\mathbf{IFL}\). The very existence of
\(\mathbf{IFL}\) proves that rejecting compositionality is no obstacle
for the formulation of a powerful logic (Hintikka 1995). It should
also be noted that what makes Hodges's result work is its
type-theoretical ascent. Let us say that a *Tarski-type*
compositional semantics is a compositional semantics which interprets
each formula \(\phi(x\_1 ,\ldots ,x\_n)\) of \(n\) free variables in
terms of an \(n\)-tuple of elements of the domain. Hence the standard
semantics of \(\mathbf{FO}\) is Tarski-type, but Hodges's
semantics employing the satisfaction relation '\(M \vDash\_X
\phi\)' is not, because the latter evaluates a formula
\(\phi(x\_1 ,\ldots ,x\_n)\) of \(n\) free variables relative to an
entire *set* of \(n\)-tuples of elements. Cameron & Hodges
(2001) proved that actually there is \(no\) Tarski-type compositional
semantics for \(\mathbf{IFL}\). 



The notion of compositionality can be refined by imposing constraints
on the auxiliary semantic attributes. Sandu and Hintikka (2001: 60)
suggested, by analogy with \(\mathbf{FO}\), that 'satisfaction
by a single variable assignment' would be a natural auxiliary
attribute in connection with \(\mathbf{IFL}\). By the result of
Cameron and Hodges, no semantics for \(\mathbf{IFL}\) exists that
would be compositional in this restricted sense.


### 4.5 Defining truth



The definability of truth can only be discussed in connection with
languages capable of speaking of themselves. Let us consider an
arithmetical vocabulary \(\tau\) and restrict attention to the
standard model \(N\) of Peano's axioms. Each sentence \(\phi\)
of vocabulary \(\tau\) can then be represented by a natural number
\(\ulcorner \phi \urcorner\), its Godel number. It is assumed
that \(\tau\) contains a numeral \(\boldsymbol{{}^\ulcorner \phi
{}^\urcorner}\) for each number \(\ulcorner \phi \urcorner\). If \(L\)
and \(L'\) are abstract logics of vocabulary \(\tau\), such as
\(\mathbf{FO}\) or \(\mathbf{IFL}\), and \(\TRUE(x)\) is a formula of
\(L'\) such that every sentence \(\phi\) of \(L\) satisfies: 



\[
N \vDash \phi \text{ iff } N \vDash \TRUE(\boldsymbol{{}^\ulcorner \phi {}^\urcorner}),
\]


then \(\TRUE(x)\) is said to be a *truth-predicate*
(**explicit* truth-**definition*) of logic \(L\)
in logic \(L'\) for the model \(N\). By Alfred Tarski's famous
theorem of the *undefinability of truth* (Tarski 1933), there
is no truth-predicate for \(\mathbf{FO}\) in \(\mathbf{FO}\) itself
for the model \(N\). More generally, Tarski showed that under certain
assumptions, a truth-definition for a logic \(L\) can only be given in
a metalanguage which is essentially stronger than \(L\). One of the
assumptions is that the negation used behaves like contradictory
negation. On the other hand, Tarski also pointed out that an implicit
truth-definition for \(\mathbf{FO}\) in \(\mathbf{FO}\) itself
*is* possible. Let \(\tau\) be an arithmetical vocabulary, and
let us stay with the standard model \(N\) of Peano's axioms. Let
'\(\TRUE\)' be a unary predicate not appearing in
\(\tau\). An \(\mathbf{FO}\) formula \(\psi(x)\) of vocabulary \(\tau
\cup \{\TRUE\}\) is an *implicit truth-definition* for
\(\mathbf{FO}[\tau]\) in \(\mathbf{FO}[\tau \cup \{\TRUE\}]\) for
\(N\), if for every \(\mathbf{FO}[\tau]\) sentence \(\phi\), the
following holds: 



\(N \vDash \phi\) iff there is an interpretation \(\TRUE^N\) of the
unary predicate \(\TRUE\) such that \((N, \TRUE^N ) \vDash
\psi(\boldsymbol{{}^\ulcorner \phi
 {}^\urcorner})\).[56]




Intuitively, \(\TRUE^N\) is the set of those natural numbers that are
Godel numbers of true arithmetic sentences of vocabulary
\(\tau\); and \(\psi(x)\) says that \(x\) is a Godel number in
the extension of the predicate \(\TRUE\). The formula \(\psi(x)\) is a
conjunction including clauses that mimic, on the object-language
level, the metalogical recursive clauses of the Tarski-type
truth-definition for \(\mathbf{FO}\). *E.g.*, one of the
conjuncts is

 
\[\begin{align\*} 
(\forall y)(\forall z)(y = \boldsymbol{{}^\ulcorner \chi {}^\urcorner}
 &\wedge z = \boldsymbol{{}^\ulcorner \theta {}^\urcorner} \wedge 
 x = \boldsymbol{{}^\ulcorner (\chi \wedge \theta) {}^\urcorner} \rightarrow \\
 &[\TRUE(x) \leftrightarrow (\TRUE(y) \wedge \TRUE(z))]).
\end{align\*}\]


The implicit nature of the truth-definition is seen from the fact that
the predicate \(\TRUE\) appears on both sides of the equivalence sign
in these
 clauses.[57]
 The above implicit truth-definition of \(\mathbf{FO}\) for \(N\) is
of the form 'there is a set \(S\) interpreting the predicate
\(\TRUE\) such that \(\psi(x)\).' Thus the implicit
truth-definition of \(\mathbf{FO}\) in \(\mathbf{FO}\) gives rise to
the explicit truth-definition \(\exists \TRUE\, \psi(x)\) of
\(\mathbf{FO}[\tau]\) in \(\mathbf{ESO}[\tau]\) for \(N\). Since
\(\mathbf{ESO}\) and \(\mathbf{IFL}\) have the same expressive power,
a truth-predicate of \(\mathbf{FO}\) for \(N\) can be formulated in
\(\mathbf{IFL}\). 



The same reasoning can be applied to \(\mathbf{ESO}\) itself, and
thereby to \(\mathbf{IFL}\) (Hintikka 1991, 1996; Hyttinen & Sandu
2000; Sandu 1996, 1998). Namely, an \(\mathbf{ESO}\) formula
\(\chi(x)\) of vocabulary \(\tau \cup \{\TRUE\}\) can be formulated
which is an *implicit* truth-definition of
\(\mathbf{ESO}[\tau]\) for \(N\). Therefore the \(\mathbf{ESO}[\tau]\)
formula \(\exists \TRUE\, \chi(x)\) is an *explicit*
truth-definition of \(\mathbf{ESO}[\tau]\) for \(N\). Here the
truth-predicate is formulated in the very same language whose notion
of truth is being defined: \(\mathbf{ESO}\). Hence \(\mathbf{ESO}\),
and thereby \(\mathbf{IFL}\), is capable of explicitly defining its
own truth-predicate relative to
 \(N\).[58]
 This result does not contradict Tarski's undefinability result,
because here non-determined sentences are possible; the negation used
is not contradictory
 negation.[59]



Tarski (1983) adopted a view according to which truth cannot be defined
for natural languages. It has been argued in Hintikka & Sandu
(1999) that this was due to Tarski's belief that
compositionality fails in natural
 languages.[60]
 \(\mathbf{IFL}\) does not have a Tarski-type compositional semantics,
but it admits of formulating a self-applied truth-predicate. The
proposed reason why Tarski believed it not to be possible to discuss
the notion of truth in natural languages themselves cannot, then, be
entertained from the viewpoint of \(\mathbf{IFL}\). For, the case of
\(\mathbf{IFL}\) shows that the failure of Tarski-type
compositionality for a language does not entail the impossibility for
the language to define its own
 truth-predicate.[61]



### 4.6 Properties of extended IF first-order logic



**Expressive power.** Since \(\mathbf{IFL}\) is not
closed under contradictory negation, \(\mathbf{EIFL}\) is strictly
more expressive than \(\mathbf{IFL}\) (cf. *Subsect.*
 4.2).[62]
 The following properties are expressible in \(\mathbf{EIFL}\) but not
in \(\mathbf{IFL}\) (Hintikka 1996: 188-190): finiteness of the
domain, well-foundedness of a binary relation, connectedness of a
graph, principle of mathematical induction, Bolzano-Weierstrass
theorem, and the topological notion of continuity.



**Metalogical properties.** The nice metatheorems that
\(\mathbf{IFL}\) shares with \(\mathbf{FO}\) are lost: Compactness,
Lowenheim-Skolem property, separation theorem, and the existence
of a complete disproof procedure all fail for \(\mathbf{EIFL}\)
(Hintikka 1991: 49, 1996: 189). No self-applied truth-predictate is
possible for \(\mathbf{EIFL}\). The definition of such a
truth-predicate would have to contain the clause

 
\[\begin{align\*}
(\forall y)(y = \boldsymbol{{}^\ulcorner \theta {}^\urcorner} &\wedge 
 x = \boldsymbol{{}^\ulcorner \neg \theta {}^\urcorner} \rightarrow \\
 &[\TRUE(x) \leftrightarrow \neg \TRUE(y)]).
\end{align\*}\]


But this clause is not a well-formed formula of \(\mathbf{EIFL}\),
since \(\neg\) appears in the scope of the universal quantifier
\((\forall y)\) (cf. Hintikka 1996: 151).



The validity and satisfiability problems of the full second-order can
be effectively reduced to the corresponding problems concerning
\(\mathbf{EIFL}\). Namely, why cannot a second-order sentence simply
be thought of as a two-sorted first-order sentence? Because in order
to capture the standard interpretation of second-order
 logic,[63]
 it must be said that for every extensionally possible set of
\(n\)-tuples of elements of sort 1 there exists a member of sort 2
having those and only those elements as members, for all arities \(n\)
such that the second-order sentence contains a quantifier \((\exists
R)\) where \(R\) is
 \(n\)-ary.[64]
 Now, such additional conditions can be expressed by a finite
conjunction \(X\) of \(\mathbf{USO}\) sentences, where
\(\mathbf{USO}\) (*universal second-order logic*) is obtained
from \(\mathbf{FO}\) by allowing universal quantification over
relation and function symbols in a first-order formula. Each of these
\(\mathbf{USO}\) sentences can be expressed as the contradictory
negation of an \(\mathbf{ESO}\) sentence and therefore as the
contradictory negation of an \(\mathbf{IFL}\) sentence. Consequently,
there is an \(\mathbf{IFL}\) sentence \(Y\) such that \(X\) itself is
logically equivalent to \(\neg Y\). And here \(\neg Y\) is a sentence
of \(\mathbf{EIFL}\). Therefore, if \(\phi\) is a second-order
sentence and \(\phi^\*\) its reconstruction in two-sorted first-order
logic, we have: \(\phi\) is satisfiable iff \((X \wedge \phi^\*)\) is
satisfiable iff \((\neg Y \wedge \phi^\*)\) is satisfiable. And:
\(\phi\) is valid iff \(\phi^\*\) is a logical consequence of \(X\) iff
\((\neg X \vee \phi^\*)\) is valid iff \((Y \vee \phi^\*)\) is valid.
Here, both \((\neg Y \wedge \phi^\*)\) and \((Y \vee \phi^\*)\) are
sentences of \(\mathbf{EIFL}\), the latter even a sentence of
\(\mathbf{IFL}\). It follows that the satisfiability (validity) of any
second-order sentence can be expressed as the satisfiability
(respectively, validity) of a sentence of
 \(\mathbf{EIFL}\).[65]



**Algebraic structure.** The two negations available in
\(\mathbf{EIFL}, \neg\) and \({\sim}\), agree on true sentences, as
well as on false ones: if \(\phi\) is true (false) in \(M\), then both
\({\sim}\phi\) and \(\neg \phi\) are false (true) in \(M\). By
contrast, if \(\phi\) is non-determined in \(M\), then \({\sim}\phi\)
is non-determined as well, but \(\neg \phi\) is true. The combination
\(\neg{\sim}\) of the two negations applied to a sentence \(\phi\)
asserts that \(\phi\) is not
 false.[66]



The propositional part of \(\mathbf{EIFL}\) involves the four
operators \(\neg , {\sim}, \wedge\), and \(\vee\). Hintikka (2004b)
raises the question of the algebraic structure induced by these
operators, when any two truth equivalent sentences are identified. The
operators \(\neg , \wedge\), and \(\vee\) give rise to a Boolean
algebra - but what does the strong negation \({\sim}\) add to
this structure? 



Restricting attention to truth equivalence, \({\sim}\) is definable
from the operators \(\neg\) and \(\neg{\sim}\). For, \({\sim}\phi\) is
true in \(M\) iff \(\neg(\neg{\sim}\phi)\) is true in \(M\). Instead
of \({\sim}\), the operator \(\neg{\sim}\) may then be considered.
Hintikka points out that the propositional part of \(\mathbf{EIFL}\)
(formulated in terms of the operators \(\vee , \wedge , \neg\) and
\(\neg{\sim})\) is a Boolean algebra with an operator in the sense of
Jonsson & Tarski (1951). The additional operator
\(\neg{\sim}\) is a closure operator. 



Jonsson and Tarski (1951, Thm. 3.14) showed that any closure
algebra is isomorphic to an algebraic system formed by a set equipped
with a reflexive and transitive
 relation.[67]
 As a matter of fact, the relevant algebraic structure is precisely
that of the propositional modal logic \(\mathbf{S4}\). Hence the
propositional part of \(\mathbf{EIFL}\) has the same algebraic
structure as \(\mathbf{S4}\). By a well-known result due to Godel
(1933) and McKinsey & Tarski (1948), intuitionistic propositional
logic can be interpreted in \(\mathbf{S4}\), via a translation \(t\)
such that \(\phi\) is intuitionistically provable iff \(t(\phi)\) is a
valid \(\mathbf{S4}\) formula. Thus, intuitionistic propositional
logic is interpretable in
 \(\mathbf{EIFL}\).[68]


## 5. Philosophical Consequences



Hintikka (2006a: 73-77) takes the following to be among
consequences of the novel insights made possible by (extended) IF
first-order logic: reconstruction of normal mathematical reasoning on
the first-order level, a novel perspective on the notion of truth in
axiomatic set theory, insights into the nature of negation, and the
formulation of a self-applied truth-predicate. A related topic of
general interest is the phenomenon of informational independence in
natural languages. The ideas related to negation and definability of
truth have been discussed in *Subsections* 4.2 and 4.5,
respectively. Let us consider here the remaining issues.


### 5.1 Place in type hierarchy



Hintikka maintains that the only reasonable way of making a
distinction between first-order logic and higher-order logic is by
reference to the entities that one's quantified variables range
over. A first-order logic is, then, a logic in which all quantifiers
range over individuals, in contrast to higher-order entities
(*e.g.*, subsets of the domain). On this basis Hintikka holds
that substantially speaking, \(\mathbf{IFL}\) and even
\(\mathbf{EIFL}\) are *first-order*
 logics.[69]
 Solomon Feferman (2006: 457-461) criticizes the criterion that
Hintikka employs for judging the first-order status of a logic.
Feferman makes use of generalized quantifiers in his
 argument.[70]
 The formulas 

 
\[
Q[z\_1] \ldots [z\_k] (\phi\_1 ,\ldots ,\phi\_k)
\]


involving generalized quantifiers are *syntactically
first-order*, insofar as the quantified variables \(z\_{i1},\ldots
,z\_{in\_i} = [z\_i]\) are first-order \((1 \le i \le k)\). The semantics
of a generalized quantifier \(Q\) is formulated by associating with
each domain M a \(k\)-ary relation \(Q\_M\) on M, with \(Q\_M
\subseteq\) M\(^{n\_1} \times \ldots \times\) M\(^{n\_k}\).
*E.g.*, for any infinite cardinal \(\kappa\), there is a
generalized quantifier \(Q\_{\ge \kappa}\) such that \(Q\_{\ge \kappa}z
P(z)\) is true in a model \(M\) iff there are at least \(\kappa\)
elements that satisfy the predicate \(P\). Hence generalized
quantifiers can be *semantically higher-order*. (The notion of
cardinality is a higher-order notion.) The fact that the variables in
a formula range over individuals only, does not offer a reliable
criterion for the logic's first-order status. 



Hintikka's criterion could be reformulated by saying that a
logic is of first order, if any *play* of a semantic game
associated with a formula of this logic only involves (in addition to
choices interpreting conjunctions and disjunctions) choices of
individuals, as opposed to choices of higher-order entities. By this
criterion \(\mathbf{IFL}\) (and even \(\mathbf{EIFL})\) are
first-order logics, but the logic of generalized quantifiers such as
\(Q\_{\ge \kappa}\) is
 not.[71]
 Feferman (2006: 461) anticipates the possibility of such a reply, but
finds it unconvincing.



By a result of Hintikka (1955), the problem of deciding whether a
sentence of second-order logic is valid can be effectively reduced to
the validity problem of
 \(\mathbf{IFL}\).[72]
 Vaananen (2001) has shown that the set of valid
sentences of \(\mathbf{IFL}\) has the same very high complexity as the
set of validities of the full second-order
 logic.[73]
 Vaananen (2001) and Feferman (2006) conclude that
speaking of validity in \(\mathbf{IFL}\) leads to a strong commitment
to full second-order logic. Hintikka (2006a: 476-477) looks at
these results from the opposite direction: for him they mean that
indeed one can speak of validity in full second-order logic in terms
of validity in \(\mathbf{IFL}\). What is more, Hintikka (1997) affirms
that even \(\mathbf{EIFL}\) is a first-order logic. If so, any
mathematical theory that can be expressed by the truth of an
\(\mathbf{EIFL}\) sentence is likewise free from problems of set
existence. 



Hintikka's position leads to a puzzle. If \(\phi\) is a sentence
of \(\mathbf{IFL}\) not truth equivalent to any \(\mathbf{FO}\)
sentence, the truth-condition of the sentence \(\neg \phi\) of
\(\mathbf{EIFL}\) cannot be formulated without recourse to the set of
all strategies of player 2: \(\neg \phi\) is true in model \(M\) iff
for *all* strategies of player 2 in game \(G(\phi , M)\), there
is a sequence of moves by player 1 such that player 1 wins the
resulting play. The set of all strategies of player 2 is undeniably a
higher-order entity. How can commitment to entities other than
individuals be said to have been avoided here? Can the meaning of the
sentence \(\neg \phi\) be well understood without presupposing the
genuinely second-order idea of all strategies of a given
 player?[74]
 Rather than being nominalistic, Hintikka's position appears to
be a variant of *universalia in rebus*. While rules of semantic
games pertain to actions performed on first-order objects,
combinatorial properties of sets of plays can only be formulated in
second-order terms. As soon as game rules are defined for a language
fragment, also the corresponding combinatorial properties are fully
determined, among them the properties labeled as truth and
falsity.


### 5.2 Philosophy of set theory



According to Hintikka, our pretheoretical idea of the truth of a
quantified sentence \(\phi\) (in negation normal form) is that there
exist 'witness individuals' for the existential
quantifiers, usually depending on values corresponding to the
preceding universal
 quantifiers.[75]
 It is the existence of such witnesses that constitutes the truth of
\(\phi\). Providing witnesses is precisely what Skolem functions for
\(\phi\)
 do.[76]
 The truth of a quantified sentence \(\phi\) amounts to the existence
of a full set of Skolem functions for \(\phi\). In Hintikka's
view, then, our ordinary notion of first-order truth is conceptualized
in terms of (existential) second-order logic. What happens when this
idea is applied to axiomatic set theory, say Zermelo-Fraenkel set
theory with the Axiom of Choice \((\mathbf{ZFC})\)? It should be borne
in mind that the very idea of axiomatic set theory is to dispense with
higher-order logic; its underlying logic is taken to be
\(\mathbf{FO}\). Hintikka argues as
 follows.[77]



For each sentence \(\phi\) of \(\mathbf{ZFC}\), there is another
sentence \(\phi^\* = (\exists f\_1)\ldots(\exists f\_n)\psi^\*\) of
\(\mathbf{ZFC}\) which says, intuitively, that 'Skolem
functions' for \(\phi\) exist. These 'Skolem
functions' are certain individuals of the domain of a model of
\(\mathbf{ZFC}\). Here both \(\phi^\*\) and \(\phi\) are first-order
sentences. But if for every sentence \(\phi\) of \(\mathbf{ZFC}\) we
have \(\phi\) and \(\phi^\*\) being logically equivalent, why could the
sentences \(\phi^\*\) not be used for formulating a truth-predicate for
\(\mathbf{ZFC}\) in \(\mathbf{ZFC}\) itself? However, by
Tarski's undefinability result, no such truth-predicate
 exists.[78]
 So there must be a model of \(\mathbf{ZFC}\) and a sentence \(\phi\)
true in that model such that \(\phi^\*\) is false: not all
'Skolem functions' asserted to exist by \(\phi^\*\)
actually exist in the model. 



This reasoning shows that \(\mathbf{ZFC}\) does not fully capture the
idea of truth according to which the truth of a sentence \(\phi\)
means that the Skolem functions for \(\phi\) exist. Furthermore, it
also shows that the standard interpretation of higher-order logic is
not fully captured by \(\mathbf{ZFC}\). To see this, observe that for
every sentence \(\phi\) there is a logically equivalent
*second-order* sentence \(\phi^{\*\*} = (\exists
F\_1)\ldots(\exists F\_n)\psi^{\*\*}\) actually asserting the existence of
Skolem functions for \(\phi\). The *first-order* sentence
\(\phi^\* = (\exists f\_1)\ldots(\exists f\_n)\psi^\*\) must not be
confused with the second-order sentence \(\phi^{\*\*} = (\exists
F\_1)\ldots(\exists F\_n)\psi^{\*\*}\). The Skolem functions \(F\_i\) of
which the sentence \(\phi^{\*\*}\) speaks are *sets* built out of
individuals of the set-theoretical universe, while the 'Skolem
functions' \(f\_i\) spoken of by \(\phi^\*\) are
 *individuals*.[79]



The conclusion of Hintikka's argument is that our ordinary
notion of truth is misrepresented by \(\mathbf{ZFC}\). Furthermore, by
Tarski's undefinability result the situation cannot be improved
by adding further axioms to \(\mathbf{ZFC}\). In Hintikka's
judgment, axiomatic set theory is a systematic but futile attempt to
capture on the first-order level truths of standardly interpreted
second-order logic. Like Godel (1947), also Hintikka holds that
the concepts needed to state, say, the continuum hypothesis are
sufficiently well-defined to determine the truth-value of this
conjecture. The continuum hypothesis does not receive its meaning from
phrasing it in \(\mathbf{ZFC}\). Godel and Hintikka agree that
the independence results due to Godel himself and Paul Cohen do
not by themselves show anything about the truth or falsity of the
continuum hypothesis. But unlike Godel, Hintikka finds the
derivability of any conjecture whatever in \(\mathbf{ZFC}\) (or in any
of its extensions) simply irrelevant for the truth of the conjecture.
For Hintikka, it is a 'combinatorial' question whether
every infinite subset of the reals is either countable or else has the
cardinality of the set of all reals - a question properly
conceptualized within second-order logic. This is what Hintikka takes
to be the pretheoretical sense of the truth of the continuum
hypothesis, and that is not captured by
 \(\mathbf{ZFC}\).[80]



### 5.3 Extended IF first-order logic and mathematical theorizing



Hintikka sees \(\mathbf{EIFL}\) as allowing to reconstruct all normal
mathematical reasoning on the first-order level. This result is
essentially dependent on the acceptability of Hintikka's claim
that \(\mathbf{EIFL}\) is ontologically committed to individuals only
(*Subsect.* 5.1). But how would \(\mathbf{EIFL}\) serve to
reconstruct an important part of all mathematical reasoning?



Hintikka (1996: 194-210) discusses mathematical
*theories* (or mathematical axiomatizations) and mathematical
*problems* (or questions of logical consequence)
separately.



Any higher-order *mathematical theory* \(T\) gives rise to a
many-sorted first-order theory \(T^\*\). If the theory is finite, there
is a finite conjunction \(J\) formulated in \(\mathbf{EIFL}\) -
equivalent to a sentence of \(\mathbf{USO}\) and therefore equivalent
to the contradictory negation of an \(\mathbf{ESO}\) sentence and so
indeed equivalent to the contradictory negation of an \(\mathbf{IFL}\)
sentence - expressing the requirement that the standard
interpretation of higher-order logic is respected. The question of the
truth of the higher-order theory \(T\) is thus reduced to the truth of
the sentence \((J \wedge T^\*)\) of \(\mathbf{EIFL}\) (cf.
*Subsect.* 4.6). 



The *mathematical problem* of whether a given sentence \(C\) is
a logical consequence of a finite higher-order theory \(T\) coincides
with the problem of whether the second-order sentence \((\neg(J \wedge
T^\*) \vee C^\*)\) is valid. Recalling that there is a sentence \(\chi\)
of \(\mathbf{IFL}\) such that \(J\) is equivalent to \(\neg \chi\), it
follows that \(\neg(J \wedge T^\*)\) is equivalent to a sentence of
\(\mathbf{IFL}\). Consequently there is a sentence of \(\mathbf{IFL}\)
which is valid iff the sentence \((\neg(J \wedge T^\*) \vee C^\*)\) is
valid (cf. *Subsect.* 4.6). Mathematical problems can be
understood as questions of the *validity* of an
\(\mathbf{IFL}\) sentence. Among mathematical problems thus
reconstructible using \(\mathbf{IFL}\) are the continuum hypothesis,
Goldbach's conjecture, Souslin's conjecture, the existence
of an inaccessible cardinal, and the existence of a measurable
 cardinal.[81]



As conceptualizations apparently transcending the proposed framework
- not expressible in a higher-order logic - Hintikka
considers the maximality assumption expressed by David Hilbert's
so-called axiom of completeness. The axiom says that no mathematical
objects can be added to the intended models without violating the
other
 axioms.[82]



If indeed problems related to the idea of *all subsets* are
avoided in \(\mathbf{EIFL}\) (Hintikka 1997), it offers a way of
defending a certain form logicism. Unlike in historical logicism, the
idea is not to consider logic as an axiom system on the same level as
mathematical axiom systems (Hintikka 1996:
 183),[83]
 and to attempt to reduce mathematics to logic. Rather, Hintikka
(1996: 184) proposes to ask: **(a)** Can the crucial
mathematical concepts be defined in logical terms?
**(b)** Can the modes of semantically valid logical
inferences used in mathematics be expressed in logical terms? The idea
is not to concentrate on deductive rules of logic: no complete set of
deductive rules exist anyway for \(\mathbf{IFL}\). Because the status
of higher-order logic is potentially dubious - due to the
problems associated with the notion of powerset - a positive
solution to questions (a) and (b) calls for a first-order logic more
powerful than \(\mathbf{FO}\). 



The suggested reduction of all mathematics expressible in higher-order
logic to the first-order level would be philosophically significant in
showing that mathematics is not a study of general concepts, but of
structures consisting of particulars (Hintikka 1996: 207). This is not
to say that actual mathematics would be best carried out in terms of
\(\mathbf{IFL}\), only that it could in principle be so carried out
(Hintikka 1996: 205, 2006a: 477). For a critique of Hintikka's
conclusions, see Vaananen (2001), Feferman (2006), and
Bazzoni (2015).


### 5.4 Informational independence in natural languages



When Hintikka began to apply GTS to the study of natural language
(Hintikka 1973a), he took up the question of whether branching
quantifiers occur in natural languages. He was led to ask whether
there are semantic games with imperfect information. He detected
various types of grammatical constructions in English that involve
informational
 independence.[84]
 An often cited example is the sentence 



*Some relative of each villager and some relative of each townsman
hate each other*, 



true under its relevant reading when the choice of a relative of each
townsman can be made independently of the individual chosen for
'each
 villager.'[85]
 Hintikka (1973a) sketched an argument to the effect that actually
every \(\mathbf{FPO}\) sentence can be reproduced as a representation
of an English sentence. From this it would follow that the logic of
idiomatic English quantifiers is much stronger than \(\mathbf{FO}\),
and that no effective procedure exists for classifying sentences as
analytical or nonanalytical, synonymous or
 nonsynonymous.[86]
 This would be methodologically a very important result, showing that
syntactic methods are even in principle insufficient in linguistic
theorizing. Jon Barwise (1979) suggested that particularly convincing
examples supporting Hintikka's thesis can be given in terms of
generalized quantifiers. 



Lauri Carlson and Alice ter Meulen (1979) were the first to observe
cases of informational independence between quantifiers and
intensional operators. Consider the
 question[87]



*Who does everybody admire?* 



Under one of its readings, the presupposition of this question is
\((\forall x)(\exists y)\) admires\((x, y)\). The desideratum of this
question is 



*I know who everybody admires.* 



Writing '\(K\_I\)' for 'I
 know,'[88]
 the desideratum has a reading whose logical form is 



\(K\_I (\forall x)(\exists y/K\_I)\) admires\((x, y)\). 



This desideratum is satisfied by an answer pointing out a function
\(f\) which yields for each person a suitable admired person. Such a
function can be *his or her father*. Importantly, the value
\(f(b)\) of this function only depends on the person \(b\)
interpreting 'everybody,' but does not depend on the
scenario \(w\), compatible with the questioner's knowledge, that
interprets the construction 'I know.' Interestingly, the
desideratum \(K\_I (\forall x)(\exists y/K\_I)\) admires\((x, y)\) is
not expressible without an explicit independence indicator. It is also
worth noting that this case cannot be represented in the notation of
\(\mathbf{FPO}\). This is because several types of semantic
interactions are possible among quantifiers and intensional operators,
and blocking interactions of one type does not automatically block
interactions of other types. In the example, the witness of \(\exists
y\) must not vary with the scenario \(w\) interpreting the operator
\(K\_I\), but still the values of both variables \(x\) and \(y\) must
belong to the domain of the particular scenario \(w\) chosen to
interpret
 \(K\_I\).[89]



Hintikka's ideas on desiderata of wh-questions were influenced
by his exchange with the linguist Elisabet
 Engdahl.[90]
 These wh-questions, again, functioned as important test cases for the
appearance of informational independence in natural languages. 



Hintikka and Sandu (1989) took up the task of formulating an explicit
unified formal treatment for the different varieties of informational
independence in natural language semantics. They posed the question of
which are the mechanisms that allow English to exceed the expressive
power of \(\mathbf{FO}\). For, natural languages typically do not
resort to higher-order quantifiers. Hintikka and Sandu suggested that
informational independence plays a key role in increasing the
expressive power of natural
 languages.[91]



In GTS as developed for English in Hintikka & Kulas (1983, 1985),
game rules are associated with a great variety of linguistic
expressions (cf. *Subsect.* 2.1). As Hintikka (1990) has
stressed, informational independence is a cross-categorical
phenomenon: it can occur in connection with expressions of widely
different grammatical categories. Hintikka and Sandu (1989) propose
several examples from English calculated to show that there is an
abundance of instances of informational independence in natural
languages. Among examples are wh-questions of the kind discussed
above, and the distinction between the *de dicto* and *de
re* readings of certain English sentences. Hintikka and Sandu
suggest that representing such readings in terms of IF logic is more
truthful to the syntax of English than the alternative, non-IF
representations are. 



In connection with knowledge, a *de dicto* attribution such
as



\(K\_{\textit{Ralph}} (\exists x) (x\) is a spy) 



can be turned into a *de re* attribution by marking the
existential quantifier as independent of the knowledge-operator (cf.
Hintikka and Sandu 1989):



\(K\_{\textit{Ralph}} (\exists x/K\_{\textit{Ralph}}) (x\) is a spy).




Because knowledge is a factive attitude (the actual world is among
Ralph's epistemic alternatives), this amounts indeed to the same
as the condition



\((\exists x) K\_{\textit{Ralph}} (x\) is a spy). 



Rebuschi & Tulenheimo (2011) observed that independent quantifiers
are of special interest in connection with non-factive attitudes such
as belief. The logical form of a statement ascribing to Ralph a belief
pertaining to a specific but non-existent object is 



\(B\_{\textit{Ralph}} (\exists x/B\_{\textit{Ralph}}) (x\) is a spy),




where '\(B\_{\textit{Ralph}}\)' stands for 'Ralph
believes
 that.'[92]



Attitudes of this form were dubbed *de objecto* attitudes.
Since the (intentional) object of such an attitude need not exist
actually, the *de objecto* attitude is weaker than the *de
re* attitude



\((\exists x) B\_{\textit{Ralph}} (x\) is a spy). 



On the other hand, the pattern of operators \(B\_{\textit{Ralph}}
(\exists x/B\_{\textit{Ralph}})\) requires that the witness of the
existential quantifier \(\exists x\) be the same relative to all
doxastic alternatives of Ralph, so the *de objecto* attitude is
stronger than the *de dicto* attitude



\(B\_{\textit{Ralph}} (\exists x) (x\) is a spy). 



Janssen (2013) discusses the possibility of providing in terms of
\(\mathbf{IFL}\) a compositional analysis of the *de re* /
*de dicto* ambiguity in natural languages. Brasoveanu and
Farkas (2011) argue that scopal properties of natural language
indefinites are best elucidated in terms of a semantics inspired by
\(\mathbf{IFL}\), more precisely by formulating the semantics relative
to sets of variable assignments as done in Hodges's
compositional semantics for slash logic. 



As a rule, informational independence is not indicated syntactically
in
 English.[93]
 Methodological consequences of this fact are discussed in Hintikka
(1990), where he tentatively puts forward the *Syntactic Silence
Thesis*, according to which sufficiently radical cross-categorical
phenomena are not likely to be marked syntactically in natural
languages. Evidence for this thesis would, for its part, be evidence
against the sufficiency of syntax-oriented approaches to
semantics.


## 6. Related logics


### 6.1 Slash logic



Syntactically slash logic uses quantifiers like \((\exists x/y)\)
instead of quantifiers such as \((\exists x/\forall y)\). Semantically
slash logic is otherwise like \(\mathbf{IFL}\) except that its
game-theoretical semantics is based on the idea that a player's
strategy functions may utilize as their arguments *any*
preceding moves made in the current play, save for those whose use is,
by the slash notation, explicitly indicated as forbidden (cf.
*Sect.* 3). That is, also a player's own earlier moves
may appear as arguments of a strategy function. This can make a
difference in the presence of imperfect information. For example,
consider evaluating the slash-logic sentence \((\forall x)(\exists
y)(\exists z/x) x = z\) containing the vacuous quantifier \(\exists
y\). This sentence is true on a two-element domain, since player 2 can
copy as the value of \(y\) the value that player 1 has chosen for
\(x\), and then select the value of \(z\) using a strategy function
whose only argument is the value of \(y\). (For this phenomenon of
'signaling,' see Hodges 1997a, Sandu 2001, Janssen &
Dechesne 2006, Barbero 2013.) By contrast, the IF sentence \((\forall
x)(\exists y)(\exists z/\forall x) x = z\) fails to be true on such a
domain, since there a strategy function for \((\exists z/\forall x)\)
must be a constant, and no such strategy function can guarantee a win
for player 2 against both possible values that player 1 can choose for
\(x\). As mentioned in *Subsection* 4.4, Hodges (1997a,b)
showed that slash logic admits of an alternative, compositional
semantics. This requires evaluating formulas relative to sets of
variable assignments, instead of single assignments as in connection
with \(\mathbf{FO}\).



All authors having studied slash logic, apart from Hodges himself,
have opted for not following Hodges's terminological recommendation
mentioned at the beginning of Section 3: they have referred to slash
logic as 'IF logic.'



Kuusisto (2013) studies the expressive power of fragments of slash
logic whose formulas are formed without employing the identity symbol.
Kontinen *et al.* (2014) investigate the complexity-theoretic
properties of the two-variable fragment of slash logic and compare
this fragment to the corresponding fragment of dependence logic.
Hodges (1997a,b) and Figueira *et al.* (2009, 2011, 2014)
discuss an extension of slash logic in which the contradictory
negation of slash-logic sentences can be expressed.



In Sevenster (2014), patterns of quantifier dependence and
independence in quantifier prefixes of slash-logical formulas are
systematically studied in order to determine which quantifier prefixes
allow slash logic to gain the expressive power of \(\mathbf{ESO}\).
Sevenster identifies two such patterns - the *signaling*
pattern and the *Henkin* pattern - and proves that they
are able to express \(\mathbf{NP}\)-hard decision problems. He further
shows that these two are the only patterns allowing slash logic to
exceed the expressive power of \(\mathbf{FO}\) insofar as attention is
confined to formulas in prenex form. An example of the signaling
pattern would be \( (\forall u)(\exists v)(\exists w/u) \) and of the
Henkin pattern \( (\forall x)(\exists u)(\forall y)(\exists v/x,u)
 \).[94]




Barbero (2021) and Barbero *et al.* (2021) take up the task of
investigating fragments of the general syntax of slash logic (not all
of whose formulas are in prenex form). Thereby these authors wish to
study systematically those expressive resources of slash logic that
allow it to exceed the expressive power of \(\mathbf{FO}\) and that do
not simply derive from its capacity to mimick Henkin quantifiers.
While many of the features studied in these two papers depend on the
*Eigenart* of slash logic, the phenomenon of *signaling by
disjunction* occurs in IF logic, as well. In Section 3.3, it was
seen that the IF-logical sentence \((\forall x)(\exists y/\forall x) x
= y\) is non-determined in any model whose domain has exactly two
elements. The slash-logical sentence \((\forall x)(\exists y/ x) x =
y\) is likewise non-determined in such a model. Now, consider the
result of replacing in the latter sentence the expression \((\exists
y/ x) x = y\) by the disjunction \(((\exists y/x) x = y \vee (\exists
y/ x) x = y))\), with a token of the initial expression in both
disjuncts: 
\[
(\forall x)((\exists y/ x) x = y \vee (\exists y/x) x = y).
\]
 The sentence that has been thus obtained is
actually *true* in a model whose domain consists of the objects
\(a\) and \(b\). Let \(f\), \(g\), and \(h\) be respectively the
strategy functions of player 2 for the unique token of the disjunction
symbol, the left token of the existential quantifier, and the right
token of the existential quantifier - defined as follows. First,
\(f\) selects the left disjunct if player 1 has chosen \(a\) as a
value of \(x\), selecting the right disjunct otherwise. Further, \(g\)
and \(h\) are constants (zero-place functions): \(g= a\) and \(h= b\).
The set \(\{f, g, h\}\) is clearly a winning strategy for player 2.
Either of the tokens of the existential quantifier occur in a specific
disjunct. Using the strategy function \(f\) to arrive at such a
disjunct makes sure that the disjunct arrived at reveals the choice
that player 1 has made to interpret \(\forall x\). The constants \(g\)
and \(h\) are selected so as to render this information explicit.
Thus, the resulting values of \(x\) and \(y\) indeed satisfy the
formula \(x= y\). By the same reasoning it is seen that the sentence
\((\forall x)((\exists y/ \forall x) x = y \vee (\exists y/\forall x)
x = y)\) of \(\mathbf{IFL}\) is true in the model considered.


### 6.2 Dependence logic



Jouko Vaananen (2007) formulated a new approach to IF
logic that he dubbed *dependence logic* \((\mathbf{DL})\); for
further work on \(\mathbf{DL}\), see *e.g.* Kontinen *et
al.* (2013). The syntax of \(\mathbf{DL}\) is obtained from that
of \(\mathbf{FO}\) by allowing atomic formulas of the following
special form: 

 
\[
=(x\_1 ,\ldots ,x\_n; x\_{n+1}).
\]


Intuitively such a formula means that the value of \(x\_{n+1}\) depends
only on the values of \(x\_1 ,\ldots ,x\_n\). The semantics of
\(\mathbf{DL}\) cannot be formulated relative to single variable
assignments like that of \(\mathbf{FO}\): we cannot explicate what it
means for the value of \(x\_{n+1}\) to depend on those of \(x\_1 ,\ldots
,x\_n\) with reference to a single assignment on the variables \(x\_1
,\ldots ,x\_{n+1}\). For example, consider the assignment described
below: 




|  |  |  |
| --- | --- | --- |
| \(x\_1\) | \(x\_2\) | \(x\_3\) |
| 7 | 5 | 8 |



Relative to this assignment, all of the following claims hold:
whenever the value of \(x\_1\) equals 7, the value of \(x\_3\) equals 8;
whenever the value of \(x\_2\) equals 5, the value of \(x\_3\) equals 8;
whenever the value of \(x\_1\) equals 7 and the value of \(x\_2\) equals
5, the value of \(x\_3\) equals 8; irrespective of the values of
\(x\_1\) and \(x\_2\), the value of \(x\_3\) equals 8. The question of
dependence only becomes interesting and non-vacuous relative to a set
of assignments:




|  |  |  |
| --- | --- | --- |
| \(x\_1\) | \(x\_2\) | \(x\_3\) |
| 7 | 5 | 8 |
| 9 | 5 | 6 |
| 7 | 11 | 8 |
| 7 | 3 | 8 |
| 9 | 19 | 6 |



The set \(X\) consisting of the above five assignments satisfies the
formula \(=(x\_1\); \(x\_3)\): the value of \(x\_3\) depends only on the
value of \(x\_1\). As is readily observed, any two assignments in \(X\)
which assign the same value to \(x\_1\) assign also the same value to
\(x\_3\). The interesting novelty of \(\mathbf{DL}\) is that claims
about variable dependencies are made at the atomic level. Quantifiers
of \(\mathbf{IFL}\) and those of slash logic with their independence
indications easily lead to somewhat messy formulas, whereas
\(\mathbf{DL}\) looks exactly like \(\mathbf{FO}\), apart from its
greater flexibility in forms of atomic formulas.


## 7. Conclusion



In this entry IF first-order logic and extended IF first-order logic
have been surveyed. Their metalogical properties have been explained
and the philosophical relevance of these properties has been
discussed. The suggested consequences of these logics for
philosophical issues such as the existence of a self-applied
truth-predicate, the logicist program, the philosophical relevance of
axiomatic set theory, and informational independence in natural
languages have been covered as well. Slash logic and dependence logic
- both closely related to \(\mathbf{IFL}\) and inspired by it
- were also briefly considered.