View source for Independence-friendly logic

{{short description|Extension of classical first-order logic}}
'''Independence-friendly logic''' ('''IF logic'''; proposed by [[Jaakko Hintikka]] and {{ill|Gabriel Sandu (philosopher)|fr|Gabriel Sandu|lt=Gabriel Sandu}} in 1989)<ref>[[#refHinSan1989|Hintikka&Sandu1989]]</ref> is an extension of classical [[first-order logic]] (FOL) by means of slashed quantifiers of the form <math>(\exists v/V)</math> and <math>(\forall v/V)</math>, where <math>V</math> is a finite set of variables. The intended reading of <math>(\exists v/V)</math> is "there is a <math>v</math> which is functionally independent from the variables in <math>V</math>". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of [[#IF Sentences|IF sentences]] can characterize the same classes of structures as [[existential second-order logic]] (<math>\Sigma^1_1</math>). 

For example, it can express [[branching quantifier]] sentences, such as the formula <math>\exists c\forall x\exists y\forall z(\exists w/\{x,y\})((x=z \leftrightarrow y=w) \land y \neq c)</math>  which expresses infinity in the empty signature; this cannot be done in FOL.  Therefore, first-order logic cannot, in general, express this pattern of dependency, in which <math>y</math> depends ''only'' on <math>x</math> and <math>c</math>, and <math>w</math> depends ''only'' on <math>z</math> and <math>c</math>. IF logic is more general than [[branching quantifier]]s, for example in that it can express dependencies that are not transitive, such as in the quantifier prefix <math>\forall x\exists y(\exists z/\{x\})</math>, which expresses that <math>y</math> depends on <math>x</math>, and <math>z</math> depends on <math>y</math>, but <math>z</math> does not depend on <math>x</math>.

The introduction of IF logic was partly motivated by the attempt of extending the [[game semantics]] of first-order logic to games of [[imperfect information]]. Indeed, a semantics for IF sentences can be given in terms of these kinds of games (or, alternatively, by means of a translation procedure to existential second-order logic). A semantics for open formulas cannot be given in the form of a [[Tarskian semantics]];<ref>[[#refCamHod2001|Cameron&Hodges 2001]]</ref> an adequate semantics must specify what it means for a formula to be satisfied by a set of assignments of common variable domain (a ''team'') rather than satisfaction by a single assignment. Such a ''team semantics'' was developed by [[Wilfrid Hodges|Hodges]].<ref>[[#refHod97|Hodges 1997]]</ref>

Independence-friendly logic is translation equivalent, at the level of sentences, with a number of other logical systems based on team semantics, such as [[dependence logic]], dependence-friendly logic, exclusion logic and independence logic; with the exception of the latter, IF logic is known to be equiexpressive to these logics also at the level of open formulas. However, IF logic differs from all the above-mentioned systems in that it lacks ''locality'': the meaning of an open formula cannot be described just in terms of the free variables of the formula; it is instead dependent on the context in which the formula occurs.

Independence-friendly logic shares a number of metalogical properties with first-order logic, but there are some differences, including lack of closure under (classical, contradictory) negation and higher complexity for deciding the validity of formulas. Extended IF logic addresses the closure problem, but its game-theoretical semantics is more complicated, and such logic corresponds to a larger fragment of second-order logic, a proper subset of [[Analytical hierarchy|<math>\Delta_2^1</math>]].<ref>[[#refFigGorGri2011|Figueira, Gorin & Grimson 2011]]</ref>

Hintikka argued<ref>e.g. in [[#refHin1996|Hintikka 1996]]</ref> that IF and extended IF logic should be used as a basis for the [[foundations of mathematics]]; this proposal was met in some cases with skepticism.<ref>e.g. [[#refFef2006|Feferman2006]]</ref>

== Syntax ==

A number of slightly different presentations of independence-friendly logic have appeared in the literature; here we follow Mann et al (2011).<ref>[[#refManSanSev2011|Mann, Sandu & Sevenster 2011]]</ref>

===Terms and atomic formulas===
For a fixed signature σ, terms and atomic formulas are defined exactly as in [[First-order logic|first-order logic with equality]].

===IF formulas===

Formulas of IF logic are defined as follows:

# Any atomic formula <math>\varphi</math> is an IF formula.
# If <math>\varphi</math> is an IF formula, then <math>\lnot \varphi</math> is an IF formula. 
# If <math>\varphi</math> and <math>\psi</math> are IF formulas, then <math>\phi \wedge \psi</math> and <math>\phi \vee \psi</math> are IF formulas.
# If <math>\varphi</math> is a formula, <math>v</math> is a variable, and <math>V</math> is a finite set of variables, then <math>(\exists v/V)\varphi</math> and <math>(\forall v/V)\varphi</math> are also IF formulas.

===Free variables===

The set <math>\mbox{Free}(\varphi)</math> of the free variables of an IF formula <math>\varphi</math> is defined inductively as follows:
 
# If <math>\varphi</math> is an atomic formula, then <math>\mbox{Free}(\varphi)</math> is the set of all variables occurring in it. 
# <math>\mbox{Free}(\lnot\varphi) = \mbox{Free}(\varphi)</math>;
# <math>\mbox{Free}(\varphi \vee \psi) = \mbox{Free}(\varphi) \cup \mbox{Free}(\psi)</math>;
# <math>\mbox{Free}((\exists v/V)\varphi) = \mbox{Free}((\forall v/V)\varphi) = (\mbox{Free}(\varphi) \backslash \{v\})\cup V</math>.

The last clause is the only one that differs from the clauses for first-order logic, the difference being that also the variables in the slash set <math>V</math> are counted as free variables.

===IF Sentences===

An IF formula <math>\varphi</math> such that <math>\mbox{Free}(\phi) = \emptyset</math> is an ''IF sentence''.

== Semantics ==

Three main approaches have been proposed for the definition of the semantics of IF logic. The first two, based respectively on games of imperfect information and on Skolemization, are mainly used in the definition of IF sentences only. The former generalizes a similar approach, for first-order logic, which was based instead on games of ''perfect'' information.
The third approach, ''team semantics'', is a compositional semantics in the spirit of Tarskian semantics. However, this semantics does not define what it means for a formula to be satisfied by an assignment (rather, by a ''set'' of assignments).
The first two approaches were developed in earlier publications on if logic;<ref>[[#refHinSan1989|Hintikka&Sandu 1989]]</ref><ref>[[#refSan1993|Sandu 1993]]</ref> the third one by Hodges in 1997.<ref>[[#refHod97|Hodges 1997]]</ref><ref>[[#refHod1997b|Hodges 1997b]]</ref>

In this section, we differentiate the three approaches by writing distinct pedices, as in <math>\models_{GTS},\models_{Sk},\models</math>. Since the three approaches are fundamentally equivalent, only the symbol <math>\models</math> will be used in the rest of the article.

=== Game-Theoretical Semantics ===

Game-Theoretical Semantics assigns truth values to IF sentences according to the properties of some 2-player games of imperfect information. 
For ease of presentation, it is convenient to associate games not only to sentences, but also to formulas. More precisely, one defines games <math>G(\varphi, \mathcal M, s)</math> for each triple formed by an IF formula <math>\varphi</math>, a structure <math>\mathcal M</math>, and an assignment <math>s:U\supseteq \mbox{Free}(\varphi)\rightarrow \mathcal M</math>.

==== Players ====

The semantic game <math>G(\varphi, \mathcal M, s)</math> has two players, called Eloise (or Verifier) and Abelard (or Falsifier).

==== Game rules ====

The allowed moves in the semantic game <math>G(\varphi,\mathcal M,s)</math> are determined by the synctactical structure of the formula under consideration.
For simplicity, we first assume that <math>\varphi</math> is in negation normal form, with negations symbols occurring only in front of atomic subformulas.

# If <math>\varphi</math> is a literal, the game ends, and, if <math>\varphi</math> is true in <math>\mathcal M</math> (in the first-order sense), then Eloise wins; otherwise, Abelard wins.
# If <math>\varphi=\psi_1\land\psi_2</math>, then Abelard chooses one of the subformulas <math>\psi_i</math>, and the corresponding game <math>G(\psi_i,\mathcal M,s)</math> is played. 
# If <math>\varphi=\psi_1\lor\psi_2</math>, then Eloises chooses one of the subformulas <math>\psi_i</math>, and the corresponding game <math>G(\psi_i,\mathcal M,s)</math> is played. 
# If <math>\varphi=(\forall v/V)\psi</math>, then Abelard chooses an element <math>a</math> of <math>\mathcal M</math>, and game <math>G(\psi,\mathcal M,s(a/v))</math> is played.
# If <math>\varphi=(\exists v/V)\psi</math>, then Eloise chooses an element <math>a</math> of <math>\mathcal M</math>, and game <math>G(\psi,\mathcal M,s(a/v))</math> is played.

More generally, if <math>\varphi</math> is not in negation normal form, we can state, as a rule for negation, that, when a game <math>G(\lnot\varphi,\mathcal M,s)</math> is reached, the players begin playing a dual game <math>G^*(\varphi,\mathcal M,s)</math> in which the roles of Verifiers and Falsifier are switched.

==== Histories ====
Informally, a sequence of moves in a game <math>G(\varphi,\mathcal M,s)</math> is a history. At the end of each history <math>h</math>, some subgame <math>G(\psi_h,\mathcal M,s_h)</math> is played; we call <math>s_h</math> the ''assignment associated to'' <math>h</math>, and <math>\psi_h</math> the ''subformula occurrence associated to'' <math>h</math>. The ''player associated to'' <math>h</math> is Eloise in case the most external logical operator in <math>\psi_h</math> is <math>\lor</math> or <math>\exists</math>, and Abelard in case it is <math>\land</math> or <math>\forall</math>.

The set <math>h</math> of ''allowed moves'' in a history <math>h</math> is <math>\mathcal M</math> if the most external operator of <math>\psi_h</math> is <math>\exists</math> or <math>\forall</math>; it is <math>\{L,R\}</math> (<math>L,R</math> being any two distinct objects, symbolizing 'left' and 'right') in case the most external operator of <math>\psi_h</math> is <math>\lor</math> or <math>\land</math>.

Given two assignments <math>s,t</math> of same domain, and <math>V\subseteq dom(s)</math> we write <math>s\sim_V t</math> if <math>s(w) = t(w)</math> on any variable <math>w\in dom(s)\setminus V</math>.

Imperfect information is introduced in the games by stipulating that certain histories are indistinguishable for the associated player; indistinguishable histories are said to form an 'information set'. Intuitively, if the history <math>h</math> is in the information set <math>I</math>, the player associated to <math>h</math> does not know whether he is in <math>h</math> or in some other history of <math>I</math>.
Consider two histories <math>h,h'</math> such that the associated <math>\psi_h,\psi_{h'}</math> are identical subformula occurrences of the form <math>(Qv/V)\chi</math> (<math>Q = \exists</math> or <math>\forall</math>); if furthermore <math>s_h\sim_V s_{h'}</math>, we write <math>h\sim_\exists h'</math> (in case <math>Q = \exists</math>) or <math>h\sim_\forall h'</math> (in case <math>Q = \forall</math>), in order to specify that the two histories are indistinguishable for Eloise, resp. for Abelard. We also stipulate, in general, reflexivity of this relation: if <math>\psi =\chi_1\lor\chi_2</math>, then <math>h\sim_\exists h'</math>; and if <math>\psi =\chi_1\land\chi_2</math>, then <math>h\sim_\forall h'</math>.

==== Strategies ====

For a fixed game <math>G(\varphi,\mathcal M,s)</math>, write <math>H_\exists</math> for the set of histories to which Eloise is associated, and similarly <math>H_\forall</math> for the set of histories of Abelard.

A ''strategy'' for Eloise in the game <math>G(\varphi,\mathcal M,s)</math> is any function that assigns, to any possible history in which it is Eloise's turn to play, a legal move; more precisely, any function <math>\sigma: H_\exists \rightarrow \prod_{h\in H_\exists}A(h)</math> such that <math>\sigma(h)\in A(h)</math> for every history <math>h\in H_\exists</math>. One can define dually the strategies of Abelard.

A strategy for Eloise is ''uniform'' if, whenever <math>h\sim_\exists h'</math>, <math>\sigma(h) = \sigma(h')</math>; for Abelard, if <math>h\sim_\forall h'</math> implies <math>\sigma(h) = \sigma(h')</math>.

A strategy <math>\sigma</math> for Eloise is ''winning'' if Eloise wins in each terminal history that can be reached by playing according to <math>\sigma</math>. Similarly for Abelard.

==== Truth, falsity, indeterminacy ====

An IF sentence <math>\varphi</math> is ''true'' in a structure <math>\mathcal M</math> (<math>\mathcal M\models_{GTS}^+\varphi</math>) if Eloise has a uniform winning strategy in the game <math>G(\varphi, \mathcal M, \emptyset)</math>. 
It is ''false'' (<math>\mathcal M\models_{GTS}^-\varphi</math>) if Abelard has a winning strategy.
It is ''undetermined'' if neither Eloise nor Abelard has a winning strategy.

==== Conservativity ====

The semantics of IF logic thus defined is a conservative extension of first-order semantics, in the following sense. If <math>\varphi</math> is an IF sentence with empty slash sets, associate to it the first-order formula <math>\varphi'</math> which is identical to it, except in that each IF quantifier <math>(Qv/\emptyset)</math> is replaced by the corresponding first-order quantifier <math>Qv</math>. Then <math>\mathcal M\models_{GTS}^+\varphi</math> iff <math>\mathcal M\models\varphi'</math> in the Tarskian sense; and <math>\mathcal M\models_{GTS}^-\varphi</math> iff <math>\mathcal M\not\models\varphi'</math> in the Tarskian sense.

==== Open formulas ====

More general games can be used to assign a meaning to (possibly open) IF formulas; more exactly, it is possible to define what it means for an IF formula <math>\varphi</math> to be satisfied, on a structure <math>\mathcal M</math>, by a ''team'' <math>X</math> (a set of assignments of common variable domain <math>dom(X)</math> and codomain <math>\mathcal M</math>).
The associated games <math>G(\varphi,M,X)</math> begin with the random choice of an assignment <math>s\in X</math>; after this initial move, the game 
<math>G(\varphi,M,s)</math> is played. The existence of a winning strategy for Eloise defines ''positive satisfaction'' (<math>M,X\models_{GTS}^+\varphi</math>), and existence of a winning strategy for Abelard defines ''negative satisfaction'' (<math>M,X\models_{GTS}^-\varphi</math>).
At this level of generality, Game-theoretical Semantics can be replaced by an algebraic approach, ''team semantics'' (defined below).

=== Skolem Semantics ===

A definition of truth for IF sentences can be given, alternatively, by means of a translation into existential second-order logic. The translation generalizes the [[Skolemization]] procedure of first-order logic. Falsity is defined by a dual procedure called Kreiselization.

==== Skolemization ====

Given an IF formula <math>\varphi</math>, we first define its skolemization relativized to a finite set <math>U\supseteq \mbox{Free}(\varphi)</math> of variables. For every existential quantifier <math>(\exists v/V)</math> occurring in <math>\varphi</math>, let <math>f_v</math> be a new function symbol (a "Skolem function"). We write <math>Subst(\varphi,v,t)</math> for the formula which is obtained substituting, in <math>\varphi</math>, all free occurrences of the variable <math>v</math> with the term <math>t</math>. The Skolemization of <math>\varphi</math> relative to <math>U</math>, denoted <math>\mbox{Sk}_U(\varphi)</math>, is defined by the following inductive clauses:

#<math>\operatorname{Sk}_{U}(\varphi )= \varphi </math> if <math>\varphi</math> is a literal.  
#<math>\operatorname{Sk}_{U}(\psi \lor  \chi)=\operatorname{Sk}_{U}(\psi )\lor  \operatorname{Sk}_{U}(\chi)</math>.
#<math>\operatorname{Sk}_{U}(\psi \land \chi)=\operatorname{Sk}_{U}(\psi )\land \operatorname{Sk}_{U}(\chi)</math>.
#<math>\operatorname{Sk}_{U}((\forall v/V)\psi )=\forall v\operatorname{Sk}_{U\cup \{v\}}(\psi )</math>.
#<math>\operatorname{Sk}_{U}((\exists v/V)\psi )=Subst(\operatorname{Sk}_{U\cup \{v\}}(\psi ),v,f_v(y_{1},...,y_{n}))</math>, where <math>y_{1},...,y_{n}</math> is a list of the variables in <math>U\setminus V</math>.

If <math>\varphi</math> is an IF sentence, its (unrelativized) Skolemization is defined as <math>\mbox{Sk}(\varphi) = \mbox{Sk}_\varnothing(\varphi)</math>.

==== Kreiselization ====

Given an IF formula <math>\varphi</math>, associate, to each universal quantifier <math>(\forall v/V)</math> occurring in it, a new function symbol <math>g_v</math> (a "Kreisel function"). Then, the Kreiselization <math>\mbox{Kr}_U(\varphi)</math> of <math>\varphi</math> relative to a finite set of variables <math>U\supseteq\mbox{Free}(\varphi)</math>, is defined by the following inductive clauses:

#<math>\operatorname{Kr}_{U}(\varphi )= \lnot\varphi </math> if <math>\varphi</math> is a literal.  
#<math>\operatorname{Kr}_{U}(\psi \land \chi)=\operatorname{Kr}_{U}(\psi )\lor \operatorname{Kr}_{U}(\chi)</math>.
#<math>\operatorname{Kr}_{U}(\psi \lor \chi)=\operatorname{Kr}_{U}(\psi )\land \operatorname{Kr}_{U}(\chi)</math>.
#<math>\operatorname{Kr}_{U}((\forall v/V)\psi )=Subst(\operatorname{Kr}_{U\cup \{v\}}(\psi ),v,g_v(y_{1},...,y_{n}))</math>, where <math>y_{1},...,y_{n}</math> is a list of the variables in <math>U\setminus V</math>.
#<math>\operatorname{Kr}_{U}((\exists v/V)\psi )=\forall v\operatorname{Kr}_{U\cup \{v\}}(\psi )</math>

If <math>\varphi</math> is an IF sentence, its (unrelativized) Kreiselization is defined as <math>\mbox{Kr}(\varphi) = \mbox{Kr}_\varnothing(\varphi)</math>.

==== Truth, falsity, indeterminacy ====

Given an IF sentence <math>\varphi</math> with <math>n</math> existential quantifiers, a structure <math>\mathcal M</math>, and a list <math>\vec f</math> of <math>n</math> functions of appropriate arities, we denote as <math>(\mathcal M,\vec f)</math> the expansion of <math>\mathcal M</math> which assigns the functions <math>\vec f</math> as interpretations for the Skolem functions of <math>\varphi</math>.

An IF sentence is true on a structure <math>\mathcal M</math>, written <math>\mathcal M\models_{\mbox{Sk}}^+\varphi</math>, if there is a tuple <math>\vec f</math> of functions such that <math>(\mathcal M,\vec f)\models \mbox{Sk}(\varphi)</math>.
Similarly, <math>\mathcal M\models_{\mbox{Sk}}^-\varphi</math> if there is a tuple <math>\vec f</math> of functions such that <math>(\mathcal M,\vec f)\models \mbox{Kr}(\varphi)</math>; and <math>\mathcal M\models_{\mbox{Sk}}^0\varphi</math> iff neither of the previous conditions holds.

For any IF sentence, Skolem Semantics returns the same values as Game-theoretical Semantics.{{cn|reason=Where can the proof of this claim be found?|date=April 2021}}

=== Team Semantics ===

By means of team semantics, it is possible to give a [[compositional]] account of the semantics of IF logic. Truth and falsity are grounded on the notion of 'satisfiability of a formula by a team'.

==== Teams ====

Let  <math>\mathcal M </math> be a [[Structure (mathematical logic)|structure]] and let <math>V = \{v_1, \ldots, v_n\}</math> be a finite set of variables. Then a team over <math>\mathcal M</math> with domain <math>V</math> is a set of assignments over <math>\mathcal M</math> with domain <math>V</math>, that is, a set of functions <math>s</math> from <math>V</math> to <math>\mathcal M</math>.

==== Duplicating and supplementing teams ====

Duplicating and supplementing are two operations on teams which are related to the semantics of universal and existential quantification.

#Given a team <math>X</math> over a structure <math>\mathcal M</math> and a variable <math>v</math>, the duplicating team <math>X[\mathcal M/v]</math> is the team <math>\{s(a/v)|s\in X, a\in \mathcal M\}</math>.<ref>The notation <math>s(a/v)</math> is used to denote an assignment that maps <math>v</math> to <math>a</math>, and all other variables to the same element as <math>s</math> does.</ref>
#Given a team <math>X</math> over a structure <math>\mathcal M</math>, a function <math>F:X\rightarrow \mathcal M</math> and a variable <math>v</math>, the supplementing team <math>X[F/v]</math> is the team <math>\{s(F(s)/v)|s\in X\}</math>.

It is customary to replace repeated applications of these two operation with more succinct notations, such as <math>X[\mathcal MF/uv]</math> for <math>(X[\mathcal M/u])[F/v]</math>.

==== Uniform functions on teams ====

As above, given two assignments <math>s,t</math> with same variable domain, we write <math>s\sim_V t</math> if <math>s(w) = t(w)</math> for every variable <math>w\in dom(s)\setminus V</math>.

Given a team <math>X</math> on a structure <math>\mathcal M</math> and a finite set <math>V</math> of variables, we say that a function <math>F:X\rightarrow \mathcal M</math> is <math>V</math>-uniform if <math>F(s)=F(t)</math> whenever <math>s \sim_V t</math>.

==== Semantic clauses ====

Team semantics is three-valued, in the sense that a formula may happen to be positively satisfied by a team on a given structure, or negatively satisfied by it, or neither. The semantics clauses for positive and negative satisfaction are defined by simultaneous induction on the synctactical structure of IF formulas.

Positive satisfaction:

# <math>\!\mathcal M, X \models^+ R t_1 \ldots t_n</math> if and only if, for every assignment <math>s \in X</math>, <math>\!\mathcal M, s \models R t_1 \ldots t_n</math> in the sense of first-order logic (that is, the tuple <math>\!(s(t_1) \ldots s(t_n))</math> is in the interpretation <math>R^{\mathcal M}</math> of <math>R</math>).
# <math>\!\mathcal M,X \models^+ t_1 = t_2</math> if and only if, for every assignment <math>s \in X</math>, <math>\!\mathcal M, s \models t_1 = t_2</math> in the sense of first-order logic (that is, <math>s(t_1) = s(t_2)</math>).
# <math>\!\mathcal M,X \models^+ \lnot \phi</math> if and only if <math>\!\mathcal M,X \models^- \phi</math>.
# <math>\!\mathcal M,X \models^+ \varphi \wedge \psi</math> if and only if <math>\!\mathcal M,X \models^+ \varphi</math> and <math>\!\mathcal M,X \models^+ \psi</math>.
# <math>\!\mathcal M,X \models^+ \varphi \vee \psi</math> if and only if there exist teams <math>\!Y</math> and <math>\!Z</math> such that <math>X = Y \cup Z</math> and <math>\!\mathcal M,Y \models^+ \varphi</math> and  <math>\!\mathcal M,Z \models^+ \psi</math>. 
# <math>\!\mathcal M,X \models^+ (\forall v/V) \varphi</math> if and only if <math>\!\mathcal M,X[M/v] \models^+ \varphi</math>.
# <math>\!\mathcal M,X \models^+ (\exists v/V) \varphi</math> if and only if there exists a <math>V</math>-uniform function <math>F: X \rightarrow M</math> such that <math>\!\mathcal M,X[F/v] \models^+ \phi</math>.

Negative satisfaction:

# <math>\!\mathcal M, X \models^- R t_1 \ldots t_n</math> if and only if, for every assignment <math>s \in X</math>, the tuple <math>\!(s(t_1) \ldots s(t_n))</math> is not in the interpretation <math>R^{\mathcal M}</math> of <math>R</math>.
# <math>\!\mathcal M,X \models^- t_1 = t_2</math> if and only if, for every assignment <math>s \in X</math>,  <math>s(t_1) \neq s(t_2)</math>.
# <math>\!\mathcal M,X \models^- \lnot \phi</math> if and only if <math>\!\mathcal M,X \models^+ \phi</math>.
# <math>\!\mathcal M,X \models^- \varphi \wedge \psi</math> if and only if  there exist teams <math>\!Y</math> and <math>\!Z</math> such that <math>X = Y \cup Z</math> and <math>\!\mathcal M,Y \models^- \varphi</math> and  <math>\!\mathcal M,Z \models^- \psi</math>.
# <math>\!\mathcal M,X \models^- \varphi \vee \psi</math> if and only if <math>\!\mathcal M,X \models^- \varphi</math> and <math>\!\mathcal M,X \models^- \psi</math>. 
# <math>\!\mathcal M,X \models^- (\forall v/V) \varphi</math> if and only if there exists a <math>V</math>-uniform function <math>F: X \rightarrow M</math> such that <math>\!\mathcal M,X[F/v] \models^- \phi</math>.
# <math>\!\mathcal M,X \models^- (\exists v/V) \varphi</math> if and only if <math>\!\mathcal M,X[M/v] \models^- \varphi</math>.

==== Truth, falsity, indeterminacy ====

According to team semantics, an IF sentence <math>\varphi</math> is said to be true (<math>\mathcal M\models^+ \varphi</math>) on a structure <math>\mathcal M</math> if it is satisfied on <math>\mathcal M</math> by the singleton team <math>\{\emptyset\}</math>, in symbols: <math>\mathcal M,\{\emptyset\}\models^+ \varphi</math>. 
Similarly, <math>\varphi</math> is said to be false (<math>\mathcal M\models^- \varphi</math>) on <math>\mathcal M</math> if <math>\mathcal M,\{\emptyset\}\models^-\varphi</math>; it is said to be undetermined (<math>\mathcal M\models^0 \varphi</math>) if <math>\mathcal M,\{\emptyset\}\not\models^+\varphi</math> and <math>\mathcal M,\{\emptyset\}\not\models^-\varphi</math>.

==== Relationship with Game-Theoretical Semantics ====

For any team <math>X</math> on a structure <math>\mathcal M</math>, and any IF formula <math>\varphi</math>, we have:
<math>\mathcal M,X \models^+ \varphi</math> iff <math>\mathcal M,X \models_{GTS}^+ \varphi</math>
and
<math>\mathcal M,X \models^- \varphi</math> iff <math>\mathcal M,X \models_{GTS}^- \varphi</math>.

From this it immediately follows that, for sentences <math>\varphi</math>, <math>\mathcal M\models^+ \varphi \Leftrightarrow \mathcal M\models_{GTS}^+ \varphi</math>, <math>\mathcal M\models^- \varphi \Leftrightarrow \mathcal M\models_{GTS}^- \varphi</math> and <math>\mathcal M\models^0 \varphi \Leftrightarrow \mathcal M\models^0_{GTS} \varphi</math>.

== Notions of equivalence ==

Since IF logic is, in its usual acception, three-valued, multiple notions of formula equivalence are of interest.

=== Equivalence of formulas ===

Let <math>\varphi,\psi</math> be two IF formulas.

<math>\varphi\models^+\psi</math> (<math>\varphi</math> ''truth entails'' <math>\psi</math>) if <math>\mathcal M,X\models^+\varphi \Rightarrow \mathcal M,X\models^+\psi</math> for any structure <math>\mathcal M</math> and any team <math>X</math> such that <math>dom(X)\supseteq \mbox{Free}(\varphi)\cup \mbox{Free}(\psi)</math>.

<math>\varphi \equiv^+\psi</math> (<math>\varphi</math> is ''truth equivalent'' to <math>\psi</math>) if <math>\varphi\models^+\psi</math> and <math>\psi\models^+\varphi</math>.

<math>\varphi\models^-\psi</math> (<math>\varphi</math> ''falsity entails'' <math>\psi</math>) if <math>\mathcal M,X\models^-\psi \Rightarrow \mathcal M,X\models^-\varphi</math> for any structure <math>\mathcal M</math> and any team <math>X</math> such that <math>dom(X)\supseteq \mbox{Free}(\varphi)\cup \mbox{Free}(\psi)</math>.

<math>\varphi \equiv^-\psi</math> (<math>\varphi</math> is ''falsity equivalent'' to <math>\psi</math>) if <math>\varphi\models^-\psi</math> and <math>\psi\models^-\varphi</math>.

<math>\varphi\models\psi</math> (<math>\varphi</math> ''strongly entails'' to <math>\psi</math>) if <math>\varphi\models^+\psi</math> and <math>\varphi\models^-\psi</math>.

<math>\varphi \equiv\psi</math> (<math>\varphi</math> is ''strongly equivalent'' to <math>\psi</math>) if <math>\varphi \equiv^+\psi</math> and <math>\varphi \equiv^-\psi</math>.

=== Equivalence of sentences ===

The definitions above specialize for IF sentences as follows.
Two IF sentences <math>\varphi,\psi</math> are ''truth equivalent'' if they are true in the same structures; they are ''falsity equivalent'' if they are false in the same structures; they are ''strongly equivalent'' if they are both truth and falsity equivalent.

Intuitively, using strong equivalence amounts to considering IF logic as 3-valued (true/undetermined/false), while truth equivalence treats IF sentences as if they were 2-valued (true/untrue).

=== Equivalence relative to a context ===

Many logical rules of IF logic can be adequately expressed only in terms of more restricted notions of equivalence, which take into account the context in which a formula might appear.

For example, if <math>U</math> is a finite set of variables and <math>U\supseteq \mbox{Free}(\varphi)\cup\mbox{Free}(\psi)</math>, one can state that <math>\varphi</math> is ''truth equivalent to'' <math>\psi</math> ''relative to'' <math>U</math> (<math>\varphi \equiv_U\psi</math>) in case <math>\mathcal M,X\models^+\psi \Leftrightarrow \mathcal M,X\models^+\varphi</math> for any structure <math>\mathcal M</math> and any team <math>X</math> ''of domain'' <math>U</math>.

== Model-theoretic properties ==

=== Sentence level ===

IF sentences can be translated in a truth-preserving fashion into sentences of (functional) [[second-order logic|existential second-order logic]] (<math>\Sigma_1^1</math>) by means of the Skolemization procedure (see above). Vice versa, every <math>\Sigma_1^1</math> can be translated into an IF sentence by means of a variant of the Walkoe-Enderton translation procedure for [[branching quantifier|partially-ordered quantifiers]] (<ref>[[#refWal1970|Walkoe 1970]]</ref><ref>[[#refEnd1970|Enderton 1970]]</ref>). In other words, IF logic and <math>\Sigma_1^1</math> are expressively equivalent at the level of sentences. This equivalence can be used to prove many of the properties that follow; they are inherited from <math>\Sigma_1^1</math> and in many cases similar to properties of FOL.

We denote by <math>T</math> a (possibly infinite) set of IF sentences.

* Löwenheim-Skolem property: if <math>T</math> has an infinite model, or arbitrarily large finite models, than it has models of every infinite cardinality.
* Existential compactness: if every finite <math>T_0\subseteq T</math> has a model, then also <math>T</math> has a model.
* Failure of deductive compactness: there are <math>T,\varphi</math> such that <math>T\models\varphi</math>, but <math>T_0\not\models\varphi</math> for any finite <math>T_0\subset T</math>. This is a difference from FOL.
* Separation theorem: if <math>\varphi,\psi</math> are mutually inconsistent IF sentences, then there is a FOL sentence <math>\theta</math> such that <math>\varphi\models^+\theta</math> and <math>\psi\models^+\lnot\theta</math>. This is a consequence of [[Craig's interpolation theorem]] for FOL.
* Burgess' theorem:<ref>[[#refBur2003|Burgess 2003]]</ref> if <math>\varphi,\psi</math> are mutually inconsistent IF sentences, then there is an IF sentence <math>\theta</math> such that <math>\varphi\equiv^+\theta</math> and <math>\psi\equiv^+\lnot\theta</math> (except possibly for one-element structures). In particular, this theorem reveals that the negation of IF logic is not a semantical operation with respect to truth equivalence (truth-equivalent sentences may have non-equivalent negations).
* Definability of truth:<ref>[[#refSan1998|Sandu 1998]]</ref> there is an IF sentence <math>TRUE(c)</math>, in the language of Peano Arithmetic, such that, for any IF sentence <math>\varphi,</math>, <math>\mathbb{N}\models\varphi \Leftrightarrow \mathbb{N}\models TRUE(\ulcorner\varphi\urcorner)</math> (where <math>\ulcorner\urcorner</math> denotes a Gödel numbering). A weaker statement also holds for nonstandard models of [[Peano arithmetic|Peano Arithmetic]] (<ref>[[#refVaa2007|Väänänen 2007]]</ref>).

=== Formula level ===

The notion of satisfiability by a team has the following properties:

*Downward closure: if <math>\mathcal M,X\models^\pm \varphi</math> and <math>Y\subseteq X</math>, then <math>\mathcal M,Y\models^\pm \varphi</math>.
*Consistency: <math>\mathcal M,X\models^+ \varphi</math> and <math>\mathcal M,X\models^- \varphi</math> if and only if <math>X=\emptyset</math>.
*Non-locality: there are <math>\mathcal M,X,\varphi</math> such that <math>\mathcal M,X\models \varphi\not\Leftrightarrow M,X_{\upharpoonright \mbox{Free}(\varphi)}\models \varphi</math>.

Since IF formulas are satisfied by teams and formulas of classical logics are satisfied by assignments, there is no obvious intertranslation between IF formulas and formulas of some classical logic system. However, there is a translation procedure<ref>[[#refHod1997b|Hodges 1997b]]</ref> of IF formulas into ''sentences'' of ''relational'' <math>\Sigma_1^1</math> (actually, one distinct translation <math>\tau_{U,R}</math> for each finite <math>U\supseteq \mbox{Free}(\varphi)</math> and for each choice of a predicate symbol <math>R</math> of arity <math>card(U)</math>). In this kind of translation, an extra n-ary predicate symbol <math>R</math> is used to represent an n-variable team <math>X</math>. This is motivated by the fact that, once an ordering <math>v_1\dots v_n</math> of the variables of <math>dom(X)</math> has been fixed, it is possible to associate a relation <math>Rel_{v_1\dots v_n}(X) = \{(s(v_1),\dots,s(v_n)) | s\in X\}</math> to the team <math>X</math>. With this conventions, an IF formula is related to its translation thus:
:<math>\mathcal M,X\models \varphi \Leftrightarrow (\mathcal M,Rel_{v_1\dots v_n}(X))\models \tau_{dom(X),R}(\varphi)</math>   
where <math>(M,Rel_{v_1\dots v_n}(X))</math> is the expansion of <math>\mathcal M</math> that assigns <math>Rel_{v_1\dots v_n}(X)</math> as interpretation for the predicate <math>R</math>.

Through this correlation, it is possible to say that, on a structure <math>\mathcal M</math>, an IF formula <math>\varphi</math> of n free variables ''defines'' a family of n-ary relations over <math>\mathcal M</math> (the family of the relations <math>Rel_{v_1\dots v_n}(X)</math> such that <math>\mathcal M,X\models\varphi</math>).

In 2009, Kontinen and Väänänen,<ref>[[#refKonVaa2009|Kontinen&Väänänen 2009]]</ref> showed, by means of a partial inverse translation procedure, that the families of relations that are definable by IF logic are exactly those that are nonempty, downward closed and definable in relational <math>\Sigma_1^1</math> with an extra predicate <math>R</math> (or, equivalently, nonempty and definable by a <math>\Sigma_1^1</math> sentence in which <math>R</math> occurs only negatively).

== Extended IF logic ==
{{expand section|date=October 2012}}
IF logic is not closed under classical negation. The boolean closure of IF logic is known as '''extended IF logic''' and it is equivalent to a proper fragment of <math>\Delta_2^1</math> (Figueira et al. 2011). Hintikka (1996, p.&nbsp;196) claimed that "virtually all of classical mathematics can in principle be done in extended IF first-order logic".

== Properties and critique ==
A number of properties of IF logic follow from logical equivalence with <math>\Sigma^1_1</math> and bring it closer to [[first-order logic]] including a [[compactness theorem]], a [[Löwenheim–Skolem theorem]], and a [[Craig interpolation]] theorem. (Väänänen, 2007, p.&nbsp;86). However, Väänänen (2001) proved that the set of [[Gödel number]]s of valid sentences of IF logic with at least one binary
predicate symbol (set denoted by ''Val<sub>IF</sub>'') is [[recursively]] [[isomorphic]] with the corresponding set of Gödel numbers of valid (full) second-order sentences in a vocabulary that contains one binary predicate symbol (set denoted by ''Val<sup>2</sup>''). Furthermore, Väänänen showed that ''Val<sup>2</sup>'' is the complete [[Levy hierarchy|Π<sub>2</sub>-definable]] set of integers, and that it is ''Val<sup>2</sup>'' not in <math>\Sigma^m_n</math> for any finite ''m'' and ''n''. Väänänen (2007, pp.&nbsp;136–139) summarizes the complexity results as follows:

{| class="wikitable"
|-
! Problem !! first-order logic !! IF/dependence/ESO logic
|-
| [[Decidability (logic)|Decision]]|| <math>\Sigma_1^0</math> ([[recursively enumerable|r.e.]]) || <math>\Pi_2</math> 
|-
| Non-[[Validity (logic)|validity]]|| <math>\Pi_1^0</math> ([[co-r.e.]]) || <math>\Sigma_2</math> 
|-
| [[Consistency]]|| <math>\Pi_1^0</math> || <math>\Pi_1^0</math>
|-
| Inconsistency||  <math>\Sigma_1^0</math>|| <math>\Sigma_1^0</math>
|-
|}

Feferman (2006) cites Väänänen's 2001 result to argue (contra Hintikka) that while satisfiability might be a first-order matter, the question of whether there is a winning strategy for Verifier over all structures in general "lands us squarely in ''full second order logic''" (emphasis Feferman's). Feferman also attacked the claimed usefulness of the extended IF logic, because the sentences in <math>\Pi_1^1</math> do not admit a game-theoretic interpretation.

== See also ==
* [[Game semantics|Game Semantics]]
* [[Branching quantifier|Branching Quantifiers]]
* [[Dependence logic|Dependence Logic]]

== Notes ==
{{reflist|3}}

== References ==
{{refbegin}}
* {{wikicite |ref=refBur2003|reference= Burgess, John P., "[https://projecteuclid.org/download/pdfview_1/euclid.ndjfl/1091030856 A Remark on Henkin Sentences and Their Contraries]", Notre Dame Journal of Formal Logic 44 (3):185-188 (2003). }} 
* {{wikicite |ref=refCamHod2001 |reference= Cameron, Peter and Hodges, Wilfrid (2001), "[https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/some-combinatorics-of-imperfect-information/20CEDF9ED53B639FAACF1B9741C87DC0 Some combinatorics of imperfect information]". Journal of Symbolic Logic 66: 673-684.}}
* {{wikicite |ref=refEklKol2002 | reference = Eklund, Matti and Kolak, Daniel, "[https://www.academia.edu/33499634/Is_Hintikkas_logic_first_order Is Hintikka’s Logic First Order?]" [[Synthese]], 131(3): 371-388 June 2002, [https://link.springer.com/content/pdf/10.1023%2FA%3A1016184410627].}} 
* {{wikicite |ref=refEnd1970 | reference = Enderton, Herbert B., "[https://onlinelibrary.wiley.com/doi/abs/10.1002/malq.19700160802 Finite Partially-Ordered Quantifiers]", Mathematical Logic Quarterly Volume 16, Issue 8 1970 Pages 393–397.}}
* {{wikicite |ref= refFef2006 | reference = [[Solomon Feferman|Feferman, Solomon]], "What kind of logic is “Independence Friendly” logic?", in ''The Philosophy of Jaakko Hintikka'' (Randall E. Auxier and Lewis Edwin Hahn, eds.); Library of Living Philosophers vol. 30, Open Court (2006), 453-469, http://math.stanford.edu/~feferman/papers/hintikka_iia.pdf.}}
* {{wikicite |ref= refFigGorGri2011 | reference =  Figueira, Santiago, Gorín, Daniel and Grimson, Rafael "On the Expressive Power of IF-Logic with Classical Negation", WoLLIC 2011 proceedings, pp. 135-145, {{isbn|978-3-642-20919-2}},[http://www.glyc.dc.uba.ar/santiago/papers/iflso.pdf]. }}
* {{wikicite |ref=refHin1996 | reference =  Hintikka, Jaakko (1996), "The Principles of Mathematics Revisited", Cambridge University Press, {{isbn|978-0-521-62498-5}}. }}
* {{wikicite |ref=refHin2002 | reference = Hintikka, Jaakko, "Hyperclassical logic (a.k.a. IF logic) and its implications for logical theory", [[Bulletin of Symbolic Logic]] 8, 2002, 404-423http://www.math.ucla.edu/~asl/bsl/0803/0803-004.ps .}}
* {{wikicite |ref=refHinSan1989 |reference = [[Jaakko Hintikka|Hintikka, Jaakko]] and Sandu, Gabriel (1989), "Informational independence as a semantical phenomenon", in ''Logic, Methodology and Philosophy of Science VIII'' (J. E. Fenstad, et al., eds.), North-Holland, Amsterdam, {{doi|10.1016/S0049-237X(08)70066-1}}. }}
* {{wikicite |ref=refHinSan1996 | reference = Hintikka, Jaakko and Sandu, Gabriel, "[https://www.sciencedirect.com/science/article/pii/B9780444817143500096 Game-theoretical semantics]", in ''Handbook of logic and language'', ed. J. van Benthem and [[Alice ter Meulen|A. ter Meulen]], Elsevier 1996 (1st ed.) Updated in the 2nd second edition of the book (2011). }}
* {{wikicite |ref=refHod97 |reference=[[Wilfrid Hodges|Hodges, Wilfrid]] (1997), "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.5740&rep=rep1&type=ps Compositional semantics for a language of imperfect information]". Journal of the IGPL 5: 539–563.}}
* {{wikicite |ref=refHod97b | reference = Hodges, Wilfrid, "Some Strange Quantifiers", in Lecture Notes in Computer Science 1261:51-65, Jan. 1997. }}
* {{wikicite |ref=refJan2002 | reference =  Janssen, Theo M. V.,  "Independent choices and the interpretation of IF logic." ''[[Journal of Logic, Language and Information]]'', Volume 11 Issue 3, Summer 2002, pp. 367-387 {{doi|10.1023/A:1015542413718}}[http://dare.uva.nl/document/1273]. }}
* {{wikicite |ref=refKol2001 | reference = Kolak, Daniel, ''On Hintikka'', Belmont: Wadsworth 2001 {{isbn|0-534-58389-X}}.}}
* {{wikicite |ref=refKolSym2004 | reference = Kolak, Daniel and Symons, John, "The Results are In: The Scope and Import of Hintikka’s Philosophy" in Daniel Kolak and [http://www.johnsymons.net John Symons], eds., ''Quantifiers, Questions, and Quantum Physics. Essays on the Philosophy of Jaakko Hintikka'', Springer 2004, pp. 205-268 {{isbn|1-4020-3210-2}}, {{doi|10.1007/978-1-4020-32110-0_11}}. }}
* {{wikicite |ref= refKonVaa2009 | reference = Kontinen, Juha and Väänänen, Jouko, "On definability in dependence logic" (2009), Journal of Logic, Language and Information 18 (3), 317-332.}}
* {{wikicite |ref= refManSanSev2011 | reference = Mann, Allen L., Sandu, Gabriel and Sevenster, Merlijn (2011) ''Independence-Friendly Logic. A Game-Theoretic Approach'', Cambridge University Press, {{isbn|0521149347}}. }}
* {{wikicite |ref= refSan2008 | reference = Sandu, Gabriel, "[https://link.springer.com/article/10.1023/A:1017905122049 If-Logic and Truth-definition]", Journal of Philosophical Logic April 1998, Volume 27, Issue 2, pp 143–164. }}
* {{wikicite |ref= refSan1993 | reference = Sandu, Gabriel, "[https://link.springer.com/article/10.1007/BF01049180 On the Logic of Informational Independence and Its Applications]",  Journal of Philosophical Logic Vol. 22, No. 1 (Feb. 1993), pp. 29-60. }}
* {{wikicite |ref= refVää2007 | reference = [[Jouko Väänänen|Väänänen, Jouko]], 2007, 'Dependence Logic -- A New Approach to Independence Friendly Logic', Cambridge University Press, {{isbn|978-0-521-87659-9}}, [https://web.archive.org/web/20070921164444/http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521876599].}}
* {{wikicite |ref= refWal1970 | reference = Walkoe, Wilbur John Jr., "[https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/finite-partiallyordered-quantification/115E0CF95F881AF1B95A9D72DE54D6FF Finite Partially-Ordered Quantification]", The Journal of Symbolic Logic Vol. 35, No. 4 (Dec., 1970), pp. 535-555. }} 
{{refend}}

== External links ==
* {{cite SEP |url-id=logic-if |title=Independence friendly logic |last=Tulenheimo |first=Tero}}
* {{cite SEP |url-id=logic-games |title=Logic and Games |last=Hodges |first=Wilfrid}}
* [https://planetmath.org/iflogic IF logic] on [[Planet Math]]

[[Category:Systems of formal logic]]
[[Category:Philosophical logic]]
[[Category:Non-classical logic]]