This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic (
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).
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.
[4] Hintikka argued[5] 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.
[6] A number of slightly different presentations of independence-friendly logic have appeared in the literature; here we follow Mann et al (2011).
[7] For a fixed signature σ, terms and atomic formulas are defined exactly as in first-order logic with equality.
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.
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.
has two players, called Eloise (or Verifier) and Abelard (or Falsifier).
is reached, the players begin playing a dual game
being any two distinct objects, symbolizing 'left' and 'right') in case the most external operator of
is an IF sentence with empty slash sets, associate to it the first-order formula
The existence of a winning strategy for Eloise defines positive satisfaction (
), and existence of a winning strategy for Abelard defines negative satisfaction (
A definition of truth for IF sentences can be given, alternatively, by means of a translation into existential second-order logic.
Falsity is defined by a dual procedure called Kreiselization.
Truth and falsity are grounded on the notion of 'satisfiability of a formula by a team'.
Duplicating and supplementing are two operations on teams which are related to the semantics of universal and existential quantification.
It is customary to replace repeated applications of these two operation with more succinct notations, such as
The semantics clauses for positive and negative satisfaction are defined by simultaneous induction on the synctactical structure of IF formulas.
Since IF logic is, in its usual acception, three-valued, multiple notions of formula equivalence are of interest.
This equivalence can be used to prove many of the properties that follow; they are inherited from
In this kind of translation, an extra n-ary predicate symbol
of n free variables defines a family of n-ary relations over
In 2009, Kontinen and Väänänen,[19] 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
Hintikka (1996, p. 196) claimed that "virtually all of classical mathematics can in principle be done in extended IF first-order logic".
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