Independence-friendly logic

A number of slightly different presentations of independence-friendly logic have appeared in the literature; here we follow Mann et al (2011).Mann, Sandu & Sevenster 2011

For a fixed signature σ, terms and atomic formulas are defined exactly as in first-order logic with equality.

Formulas of IF logic are defined as follows:

1. Any atomic formula $\backslash varphi$ is an IF formula.
2. If $\backslash varphi$ is an IF formula, then $\backslash lnot\; \backslash varphi$ is an IF formula.
3. If $\backslash varphi$ and $\backslash psi$ are IF formulas, then $\backslash phi\; \backslash wedge\; \backslash psi$ and $\backslash phi\; \backslash vee\; \backslash psi$ are IF formulas.
4. If $\backslash varphi$ is a formula, $v$ is a variable, and $V$ is a finite set of variables, then $(\backslash exists\; v/V)\backslash varphi$ and $(\backslash forall\; v/V)\backslash varphi$ are also IF formulas.

The set $\backslash mbox\{Free\}(\backslash varphi)$ of the free variables of an IF formula $\backslash varphi$ is defined inductively as follows:

1. If $\backslash varphi$ is an atomic formula, then $\backslash mbox\{Free\}(\backslash varphi)$ is the set of all variables occurring in it.
2. $\backslash mbox\{Free\}(\backslash lnot\backslash varphi)\; =\; \backslash mbox\{Free\}(\backslash varphi)$;
3. $\backslash mbox\{Free\}(\backslash varphi\; \backslash vee\; \backslash psi)\; =\; \backslash mbox\{Free\}(\backslash varphi)\; \backslash cup\; \backslash mbox\{Free\}(\backslash psi)$;
4. $\backslash mbox\{Free\}((\backslash exists\; v/V)\backslash varphi)\; =\; \backslash mbox\{Free\}((\backslash forall\; v/V)\backslash varphi)\; =\; (\backslash mbox\{Free\}(\backslash varphi)\; \backslash backslash\; \backslash \{v\backslash \})\backslash cup\; V$.

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 $V$ are counted as free variables.

An IF formula $\backslash varphi$ such that $\backslash mbox\{Free\}(\backslash phi)\; =\; \backslash emptyset$ is an IF sentence.

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;Hintikka&Sandu 1989Sandu 1993 the third one by Hodges in 1997.Hodges 1997Hodges 1997b

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

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 $G(\backslash varphi,\; \backslash mathcal\; M,\; s)$ for each triple formed by an IF formula $\backslash varphi$, a structure $\backslash mathcal\; M$, and an assignment $s:U\backslash supseteq\; \backslash mbox\{Free\}(\backslash varphi)\backslash rightarrow\; \backslash mathcal\; M$.

The semantic game $G(\backslash varphi,\; \backslash mathcal\; M,\; s)$ has two players, called Eloise (or Verifier) and Abelard (or Falsifier).

The allowed moves in the semantic game $G(\backslash varphi,\backslash mathcal\; M,s)$ are determined by the synctactical structure of the formula under consideration.

For simplicity, we first assume that $\backslash varphi$ is in negation normal form, with negations symbols occurring only in front of atomic subformulas.

1. If $\backslash varphi$ is a literal, the game ends, and, if $\backslash varphi$ is true in $\backslash mathcal\; M$ (in the first-order sense), then Eloise wins; otherwise, Abelard wins.
2. If $\backslash varphi=\backslash psi\_1\backslash land\backslash psi\_2$, then Abelard chooses one of the subformulas $\backslash psi\_i$, and the corresponding game $G(\backslash psi\_i,\backslash mathcal\; M,s)$ is played.
3. If $\backslash varphi=\backslash psi\_1\backslash lor\backslash psi\_2$, then Eloises chooses one of the subformulas $\backslash psi\_i$, and the corresponding game $G(\backslash psi\_i,\backslash mathcal\; M,s)$ is played.
4. If $\backslash varphi=(\backslash forall\; v/V)\backslash psi$, then Abelard chooses an element $a$ of $\backslash mathcal\; M$, and game $G(\backslash psi,\backslash mathcal\; M,s(a/v))$ is played.
5. If $\backslash varphi=(\backslash exists\; v/V)\backslash psi$, then Eloise chooses an element $a$ of $\backslash mathcal\; M$, and game $G(\backslash psi,\backslash mathcal\; M,s(a/v))$ is played.

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

Informally, a sequence of moves in a game $G(\backslash varphi,\backslash mathcal\; M,s)$ is a history. At the end of each history $h$, some subgame $G(\backslash psi\_h,\backslash mathcal\; M,s\_h)$ is played; we call $s\_h$ the assignment associated to $h$, and $\backslash psi\_h$ the subformula occurrence associated to $h$. The player associated to $h$ is Eloise in case the most external logical operator in $\backslash psi\_h$ is $\backslash lor$ or $\backslash exists$, and Abelard in case it is $\backslash land$ or $\backslash forall$.

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

Given two assignments $s,t$ of same domain, and $V\backslash subseteq\; dom(s)$ we write $s\backslash sim\_V\; t$ if $s(w)\; =\; t(w)$ on any variable $w\backslash in\; dom(s)\backslash setminus\; V$.

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 $h$ is in the information set $I$, the player associated to $h$ does not know whether he is in $h$ or in some other history of $I$.

Consider two histories $h,h\text{'}$ such that the associated $\backslash psi\_h,\backslash psi\_\{h\text{'}\}$ are identical subformula occurrences of the form $(Qv/V)\backslash chi$ ($Q\; =\; \backslash exists$ or $\backslash forall$); if furthermore $s\_h\backslash sim\_V\; s\_\{h\text{'}\}$, we write $h\backslash sim\_\backslash exists\; h\text{'}$ (in case $Q\; =\; \backslash exists$) or $h\backslash sim\_\backslash forall\; h\text{'}$ (in case $Q\; =\; \backslash forall$), 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 $\backslash psi\; =\backslash chi\_1\backslash lor\backslash chi\_2$, then $h\backslash sim\_\backslash exists\; h\text{'}$; and if $\backslash psi\; =\backslash chi\_1\backslash land\backslash chi\_2$, then $h\backslash sim\_\backslash forall\; h\text{'}$.

For a fixed game $G(\backslash varphi,\backslash mathcal\; M,s)$, write $H\_\backslash exists$ for the set of histories to which Eloise is associated, and similarly $H\_\backslash forall$ for the set of histories of Abelard.

A strategy for Eloise in the game $G(\backslash varphi,\backslash mathcal\; M,s)$ 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 $\backslash sigma:\; H\_\backslash exists\; \backslash rightarrow\; \backslash prod\_\{h\backslash in\; H\_\backslash exists\}A(h)$ such that $\backslash sigma(h)\backslash in\; A(h)$ for every history $h\backslash in\; H\_\backslash exists$. One can define dually the strategies of Abelard.

A strategy for Eloise is uniform if, whenever $h\backslash sim\_\backslash exists\; h\text{'}$, $\backslash sigma(h)\; =\; \backslash sigma(h\text{'})$; for Abelard, if $h\backslash sim\_\backslash forall\; h\text{'}$ implies $\backslash sigma(h)\; =\; \backslash sigma(h\text{'})$.

A strategy $\backslash sigma$ for Eloise is winning if Eloise wins in each terminal history that can be reached by playing according to $\backslash sigma$. Similarly for Abelard.

An IF sentence $\backslash varphi$ is true in a structure $\backslash mathcal\; M$ ($\backslash mathcal\; M\backslash models\_\{GTS\}^+\backslash varphi$) if Eloise has a uniform winning strategy in the game $G(\backslash varphi,\; \backslash mathcal\; M,\; \backslash emptyset)$.

It is false ($\backslash mathcal\; M\backslash models\_\{GTS\}^-\backslash varphi$) if Abelard has a winning strategy.

It is undetermined if neither Eloise nor Abelard has a winning strategy.

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

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 $\backslash varphi$ to be satisfied, on a structure $\backslash mathcal\; M$, by a team $X$ (a set of assignments of common variable domain $dom(X)$ and codomain $\backslash mathcal\; M$).

The associated games $G(\backslash varphi,M,X)$ begin with the random choice of an assignment $s\backslash in\; X$; after this initial move, the game

$G(\backslash varphi,M,s)$ is played. The existence of a winning strategy for Eloise defines positive satisfaction ($M,X\backslash models\_\{GTS\}^+\backslash varphi$), and existence of a winning strategy for Abelard defines negative satisfaction ($M,X\backslash models\_\{GTS\}^-\backslash varphi$).

At this level of generality, Game-theoretical Semantics can be replaced by an algebraic approach, team semantics (defined below).

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.

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

1. $\backslash operatorname\{Sk\}\_\{U\}(\backslash varphi\; )=\; \backslash varphi$ if $\backslash varphi$ is a literal.
2. $\backslash operatorname\{Sk\}\_\{U\}(\backslash psi\; \backslash lor\; \backslash chi)=\backslash operatorname\{Sk\}\_\{U\}(\backslash psi\; )\backslash lor\; \backslash operatorname\{Sk\}\_\{U\}(\backslash chi)$.
3. $\backslash operatorname\{Sk\}\_\{U\}(\backslash psi\; \backslash land\; \backslash chi)=\backslash operatorname\{Sk\}\_\{U\}(\backslash psi\; )\backslash land\; \backslash operatorname\{Sk\}\_\{U\}(\backslash chi)$.
4. $\backslash operatorname\{Sk\}\_\{U\}((\backslash forall\; v/V)\backslash psi\; )=\backslash forall\; v\backslash operatorname\{Sk\}\_\{U\backslash cup\; \backslash \{v\backslash \}\}(\backslash psi\; )$.
5. $\backslash operatorname\{Sk\}\_\{U\}((\backslash exists\; v/V)\backslash psi\; )=Subst(\backslash operatorname\{Sk\}\_\{U\backslash cup\; \backslash \{v\backslash \}\}(\backslash psi\; ),v,f\_v(y\_\{1\},...,y\_\{n\}))$, where $y\_\{1\},...,y\_\{n\}$ is a list of the variables in $U\backslash setminus\; V$.

If $\backslash varphi$ is an IF sentence, its (unrelativized) Skolemization is defined as $\backslash mbox\{Sk\}(\backslash varphi)\; =\; \backslash mbox\{Sk\}\_\backslash varnothing(\backslash varphi)$.

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

1. $\backslash operatorname\{Kr\}\_\{U\}(\backslash varphi\; )=\; \backslash lnot\backslash varphi$ if $\backslash varphi$ is a literal.
2. $\backslash operatorname\{Kr\}\_\{U\}(\backslash psi\; \backslash land\; \backslash chi)=\backslash operatorname\{Kr\}\_\{U\}(\backslash psi\; )\backslash lor\; \backslash operatorname\{Kr\}\_\{U\}(\backslash chi)$.
3. $\backslash operatorname\{Kr\}\_\{U\}(\backslash psi\; \backslash lor\; \backslash chi)=\backslash operatorname\{Kr\}\_\{U\}(\backslash psi\; )\backslash land\; \backslash operatorname\{Kr\}\_\{U\}(\backslash chi)$.
4. $\backslash operatorname\{Kr\}\_\{U\}((\backslash forall\; v/V)\backslash psi\; )=Subst(\backslash operatorname\{Kr\}\_\{U\backslash cup\; \backslash \{v\backslash \}\}(\backslash psi\; ),v,g\_v(y\_\{1\},...,y\_\{n\}))$, where $y\_\{1\},...,y\_\{n\}$ is a list of the variables in $U\backslash setminus\; V$.
5. $\backslash operatorname\{Kr\}\_\{U\}((\backslash exists\; v/V)\backslash psi\; )=\backslash forall\; v\backslash operatorname\{Kr\}\_\{U\backslash cup\; \backslash \{v\backslash \}\}(\backslash psi\; )$

If $\backslash varphi$ is an IF sentence, its (unrelativized) Kreiselization is defined as $\backslash mbox\{Kr\}(\backslash varphi)\; =\; \backslash mbox\{Kr\}\_\backslash varnothing(\backslash varphi)$.

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

An IF sentence is true on a structure $\backslash mathcal\; M$, written $\backslash mathcal\; M\backslash models\_\{\backslash mbox\{Sk\}\}^+\backslash varphi$, if there is a tuple $\backslash vec\; f$ of functions such that $(\backslash mathcal\; M,\backslash vec\; f)\backslash models\; \backslash mbox\{Sk\}(\backslash varphi)$.

Similarly, $\backslash mathcal\; M\backslash models\_\{\backslash mbox\{Sk\}\}^-\backslash varphi$ if there is a tuple $\backslash vec\; f$ of functions such that $(\backslash mathcal\; M,\backslash vec\; f)\backslash models\; \backslash mbox\{Kr\}(\backslash varphi)$; and $\backslash mathcal\; M\backslash models\_\{\backslash mbox\{Sk\}\}^0\backslash varphi$ 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}}

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

Let $\backslash mathcal\; M$ be a structure and let $V\; =\; \backslash \{v\_1,\; \backslash ldots,\; v\_n\backslash \}$ be a finite set of variables. Then a team over $\backslash mathcal\; M$ with domain $V$ is a set of assignments over $\backslash mathcal\; M$ with domain $V$, that is, a set of functions $s$ from $V$ to $\backslash mathcal\; M$.

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

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

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

As above, given two assignments $s,t$ with same variable domain, we write $s\backslash sim\_V\; t$ if $s(w)\; =\; t(w)$ for every variable $w\backslash in\; dom(s)\backslash setminus\; V$.

Given a team $X$ on a structure $\backslash mathcal\; M$ and a finite set $V$ of variables, we say that a function $F:X\backslash rightarrow\; \backslash mathcal\; M$ is $V$-uniform if $F(s)=F(t)$ whenever $s\; \backslash sim\_V\; t$.

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:

1. $\backslash !\backslash mathcal\; M,\; X\; \backslash models^+\; R\; t\_1\; \backslash ldots\; t\_n$ if and only if, for every assignment $s\; \backslash in\; X$, $\backslash !\backslash mathcal\; M,\; s\; \backslash models\; R\; t\_1\; \backslash ldots\; t\_n$ in the sense of first-order logic (that is, the tuple $\backslash !(s(t\_1)\; \backslash ldots\; s(t\_n))$ is in the interpretation $R^\{\backslash mathcal\; M\}$ of $R$).
2. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; t\_1\; =\; t\_2$ if and only if, for every assignment $s\; \backslash in\; X$, $\backslash !\backslash mathcal\; M,\; s\; \backslash models\; t\_1\; =\; t\_2$ in the sense of first-order logic (that is, $s(t\_1)\; =\; s(t\_2)$).
3. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash lnot\; \backslash phi$ if and only if $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash phi$.
4. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash varphi\; \backslash wedge\; \backslash psi$ if and only if $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash varphi$ and $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash psi$.
5. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash varphi\; \backslash vee\; \backslash psi$ if and only if there exist teams $\backslash !Y$ and $\backslash !Z$ such that $X\; =\; Y\; \backslash cup\; Z$ and $\backslash !\backslash mathcal\; M,Y\; \backslash models^+\; \backslash varphi$ and $\backslash !\backslash mathcal\; M,Z\; \backslash models^+\; \backslash psi$.
6. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; (\backslash forall\; v/V)\; \backslash varphi$ if and only if $\backslash !\backslash mathcal\; M,X[M/v]\; \backslash models^+\; \backslash varphi$.
7. $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; (\backslash exists\; v/V)\; \backslash varphi$ if and only if there exists a $V$-uniform function $F:\; X\; \backslash rightarrow\; M$ such that $\backslash !\backslash mathcal\; M,X[F/v]\; \backslash models^+\; \backslash phi$.

Negative satisfaction:

1. $\backslash !\backslash mathcal\; M,\; X\; \backslash models^-\; R\; t\_1\; \backslash ldots\; t\_n$ if and only if, for every assignment $s\; \backslash in\; X$, the tuple $\backslash !(s(t\_1)\; \backslash ldots\; s(t\_n))$ is not in the interpretation $R^\{\backslash mathcal\; M\}$ of $R$.
2. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; t\_1\; =\; t\_2$ if and only if, for every assignment $s\; \backslash in\; X$, $s(t\_1)\; \backslash neq\; s(t\_2)$.
3. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash lnot\; \backslash phi$ if and only if $\backslash !\backslash mathcal\; M,X\; \backslash models^+\; \backslash phi$.
4. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash varphi\; \backslash wedge\; \backslash psi$ if and only if there exist teams $\backslash !Y$ and $\backslash !Z$ such that $X\; =\; Y\; \backslash cup\; Z$ and $\backslash !\backslash mathcal\; M,Y\; \backslash models^-\; \backslash varphi$ and $\backslash !\backslash mathcal\; M,Z\; \backslash models^-\; \backslash psi$.
5. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash varphi\; \backslash vee\; \backslash psi$ if and only if $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash varphi$ and $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; \backslash psi$.
6. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; (\backslash forall\; v/V)\; \backslash varphi$ if and only if there exists a $V$-uniform function $F:\; X\; \backslash rightarrow\; M$ such that $\backslash !\backslash mathcal\; M,X[F/v]\; \backslash models^-\; \backslash phi$.
7. $\backslash !\backslash mathcal\; M,X\; \backslash models^-\; (\backslash exists\; v/V)\; \backslash varphi$ if and only if $\backslash !\backslash mathcal\; M,X[M/v]\; \backslash models^-\; \backslash varphi$.

According to team semantics, an IF sentence $\backslash varphi$ is said to be true ($\backslash mathcal\; M\backslash models^+\; \backslash varphi$) on a structure $\backslash mathcal\; M$ if it is satisfied on $\backslash mathcal\; M$ by the singleton team $\backslash \{\backslash emptyset\backslash \}$, in symbols: $\backslash mathcal\; M,\backslash \{\backslash emptyset\backslash \}\backslash models^+\; \backslash varphi$.

Similarly, $\backslash varphi$ is said to be false ($\backslash mathcal\; M\backslash models^-\; \backslash varphi$) on $\backslash mathcal\; M$ if $\backslash mathcal\; M,\backslash \{\backslash emptyset\backslash \}\backslash models^-\backslash varphi$; it is said to be undetermined ($\backslash mathcal\; M\backslash models^0\; \backslash varphi$) if $\backslash mathcal\; M,\backslash \{\backslash emptyset\backslash \}\backslash not\backslash models^+\backslash varphi$ and $\backslash mathcal\; M,\backslash \{\backslash emptyset\backslash \}\backslash not\backslash models^-\backslash varphi$.

For any team $X$ on a structure $\backslash mathcal\; M$, and any IF formula $\backslash varphi$, we have:

$\backslash mathcal\; M,X\; \backslash models^+\; \backslash varphi$ iff $\backslash mathcal\; M,X\; \backslash models\_\{GTS\}^+\; \backslash varphi$

and

$\backslash mathcal\; M,X\; \backslash models^-\; \backslash varphi$ iff $\backslash mathcal\; M,X\; \backslash models\_\{GTS\}^-\; \backslash varphi$.

From this it immediately follows that, for sentences $\backslash varphi$, $\backslash mathcal\; M\backslash models^+\; \backslash varphi\; \backslash Leftrightarrow\; \backslash mathcal\; M\backslash models\_\{GTS\}^+\; \backslash varphi$, $\backslash mathcal\; M\backslash models^-\; \backslash varphi\; \backslash Leftrightarrow\; \backslash mathcal\; M\backslash models\_\{GTS\}^-\; \backslash varphi$ and $\backslash mathcal\; M\backslash models^0\; \backslash varphi\; \backslash Leftrightarrow\; \backslash mathcal\; M\backslash models^0\_\{GTS\}\; \backslash varphi$.

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

Let $\backslash varphi,\backslash psi$ be two IF formulas.

$\backslash varphi\backslash models^+\backslash psi$ ($\backslash varphi$ truth entails $\backslash psi$) if $\backslash mathcal\; M,X\backslash models^+\backslash varphi\; \backslash Rightarrow\; \backslash mathcal\; M,X\backslash models^+\backslash psi$ for any structure $\backslash mathcal\; M$ and any team $X$ such that $dom(X)\backslash supseteq\; \backslash mbox\{Free\}(\backslash varphi)\backslash cup\; \backslash mbox\{Free\}(\backslash psi)$.

$\backslash varphi\; \backslash equiv^+\backslash psi$ ($\backslash varphi$ is truth equivalent to $\backslash psi$) if $\backslash varphi\backslash models^+\backslash psi$ and $\backslash psi\backslash models^+\backslash varphi$.

$\backslash varphi\backslash models^-\backslash psi$ ($\backslash varphi$ falsity entails $\backslash psi$) if $\backslash mathcal\; M,X\backslash models^-\backslash psi\; \backslash Rightarrow\; \backslash mathcal\; M,X\backslash models^-\backslash varphi$ for any structure $\backslash mathcal\; M$ and any team $X$ such that $dom(X)\backslash supseteq\; \backslash mbox\{Free\}(\backslash varphi)\backslash cup\; \backslash mbox\{Free\}(\backslash psi)$.

$\backslash varphi\; \backslash equiv^-\backslash psi$ ($\backslash varphi$ is falsity equivalent to $\backslash psi$) if $\backslash varphi\backslash models^-\backslash psi$ and $\backslash psi\backslash models^-\backslash varphi$.

$\backslash varphi\backslash models\backslash psi$ ($\backslash varphi$ strongly entails to $\backslash psi$) if $\backslash varphi\backslash models^+\backslash psi$ and $\backslash varphi\backslash models^-\backslash psi$.

$\backslash varphi\; \backslash equiv\backslash psi$ ($\backslash varphi$ is strongly equivalent to $\backslash psi$) if $\backslash varphi\; \backslash equiv^+\backslash psi$ and $\backslash varphi\; \backslash equiv^-\backslash psi$.

The definitions above specialize for IF sentences as follows.

Two IF sentences $\backslash varphi,\backslash psi$ 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).

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 $U$ is a finite set of variables and $U\backslash supseteq\; \backslash mbox\{Free\}(\backslash varphi)\backslash cup\backslash mbox\{Free\}(\backslash psi)$, one can state that $\backslash varphi$ is truth equivalent to $\backslash psi$ relative to $U$ ($\backslash varphi\; \backslash equiv\_U\backslash psi$) in case $\backslash mathcal\; M,X\backslash models^+\backslash psi\; \backslash Leftrightarrow\; \backslash mathcal\; M,X\backslash models^+\backslash varphi$ for any structure $\backslash mathcal\; M$ and any team $X$ of domain $U$.

IF sentences can be translated in a truth-preserving fashion into sentences of (functional) existential second-order logic ($\backslash Sigma\_1^1$) by means of the Skolemization procedure (see above). Vice versa, every $\backslash Sigma\_1^1$ can be translated into an IF sentence by means of a variant of the Walkoe-Enderton translation procedure for partially-ordered quantifiers (Walkoe 1970Enderton 1970). In other words, IF logic and $\backslash Sigma\_1^1$ 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 $\backslash Sigma\_1^1$ and in many cases similar to properties of FOL.

We denote by $T$ a (possibly infinite) set of IF sentences.

• Löwenheim-Skolem property: if $T$ has an infinite model, or arbitrarily large finite models, than it has models of every infinite cardinality.
• Existential compactness: if every finite $T\_0\backslash subseteq\; T$ has a model, then also $T$ has a model.
• Failure of deductive compactness: there are $T,\backslash varphi$ such that $T\backslash models\backslash varphi$, but $T\_0\backslash not\backslash models\backslash varphi$ for any finite $T\_0\backslash subset\; T$. This is a difference from FOL.
• Separation theorem: if $\backslash varphi,\backslash psi$ are mutually inconsistent IF sentences, then there is a FOL sentence $\backslash theta$ such that $\backslash varphi\backslash models^+\backslash theta$ and $\backslash psi\backslash models^+\backslash lnot\backslash theta$. This is a consequence of Craig's interpolation theorem for FOL.
• Burgess' theorem:Burgess 2003 if $\backslash varphi,\backslash psi$ are mutually inconsistent IF sentences, then there is an IF sentence $\backslash theta$ such that $\backslash varphi\backslash equiv^+\backslash theta$ and $\backslash psi\backslash equiv^+\backslash lnot\backslash theta$ (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:Sandu 1998 there is an IF sentence $TRUE(c)$, in the language of Peano Arithmetic, such that, for any IF sentence $\backslash varphi,$, $\backslash mathbb\{N\}\backslash models\backslash varphi\; \backslash Leftrightarrow\; \backslash mathbb\{N\}\backslash models\; TRUE(\backslash ulcorner\backslash varphi\backslash urcorner)$ (where $\backslash ulcorner\backslash urcorner$ denotes a Gödel numbering). A weaker statement also holds for nonstandard models of Peano Arithmetic (Väänänen 2007).

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

• Downward closure: if $\backslash mathcal\; M,X\backslash models^\backslash pm\; \backslash varphi$ and $Y\backslash subseteq\; X$, then $\backslash mathcal\; M,Y\backslash models^\backslash pm\; \backslash varphi$.
• Consistency: $\backslash mathcal\; M,X\backslash models^+\; \backslash varphi$ and $\backslash mathcal\; M,X\backslash models^-\; \backslash varphi$ if and only if $X=\backslash emptyset$.
• Non-locality: there are $\backslash mathcal\; M,X,\backslash varphi$ such that $\backslash mathcal\; M,X\backslash models\; \backslash varphi\backslash not\backslash Leftrightarrow\; M,X\_\{\backslash upharpoonright\; \backslash mbox\{Free\}(\backslash varphi)\}\backslash models\; \backslash varphi$.

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 procedureHodges 1997b of IF formulas into sentences of relational $\backslash Sigma\_1^1$ (actually, one distinct translation $\backslash tau\_\{U,R\}$ for each finite $U\backslash supseteq\; \backslash mbox\{Free\}(\backslash varphi)$ and for each choice of a predicate symbol $R$ of arity $card(U)$). In this kind of translation, an extra n-ary predicate symbol $R$ is used to represent an n-variable team $X$. This is motivated by the fact that, once an ordering $v\_1\backslash dots\; v\_n$ of the variables of $dom(X)$ has been fixed, it is possible to associate a relation $Rel\_\{v\_1\backslash dots\; v\_n\}(X)\; =\; \backslash \{(s(v\_1),\backslash dots,s(v\_n))\; |\; s\backslash in\; X\backslash \}$ to the team $X$. With this conventions, an IF formula is related to its translation thus:

:$\backslash mathcal\; M,X\backslash models\; \backslash varphi\; \backslash Leftrightarrow\; (\backslash mathcal\; M,Rel\_\{v\_1\backslash dots\; v\_n\}(X))\backslash models\; \backslash tau\_\{dom(X),R\}(\backslash varphi)$

where $(M,Rel\_\{v\_1\backslash dots\; v\_n\}(X))$ is the expansion of $\backslash mathcal\; M$ that assigns $Rel\_\{v\_1\backslash dots\; v\_n\}(X)$ as interpretation for the predicate $R$.

Through this correlation, it is possible to say that, on a structure $\backslash mathcal\; M$, an IF formula $\backslash varphi$ of n free variables defines a family of n-ary relations over $\backslash mathcal\; M$ (the family of the relations $Rel\_\{v\_1\backslash dots\; v\_n\}(X)$ such that $\backslash mathcal\; M,X\backslash models\backslash varphi$).

In 2009, Kontinen and Väänänen,Kontinen&Väänänen 2009 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 $\backslash Sigma\_1^1$ with an extra predicate $R$ (or, equivalently, nonempty and definable by a $\backslash Sigma\_1^1$ sentence in which $R$ occurs only negatively).

{{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 $\backslash Delta\_2^1$ (Figueira et al. 2011). Hintikka (1996, p. 196) claimed that "virtually all of classical mathematics can in principle be done in extended IF first-order logic".

A number of properties of IF logic follow from logical equivalence with $\backslash Sigma^1\_1$ 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. 86). However, Väänänen (2001) proved that the set of Gödel numbers of valid sentences of IF logic with at least one binary

predicate symbol (set denoted by Val_IF) 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²). Furthermore, Väänänen showed that Val² is the complete Π₂-definable set of integers, and that it is Val² not in $\backslash Sigma^m\_n$ for any finite m and n. Väänänen (2007, pp. 136–139) summarizes the complexity results as follows:

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 $\backslash Pi\_1^1$ do not admit a game-theoretic interpretation.

• Game Semantics
• Branching Quantifiers
• Dependence Logic

{{reflist|3}}

{{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 = 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 = 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 A. ter Meulen, Elsevier 1996 (1st ed.) Updated in the 2nd second edition of the book (2011). }}
• {{wikicite |ref=refHod97 |reference=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 = 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}}

• {{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