Independence-friendly logic (IF logic), proposed by Jaakko Hintikka and Gabriel Sandu in 1989 (), is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form
Contents
- Syntax
- Terms and atomic formulas
- IF formulas
- Free variables
- IF Sentences
- Semantics
- Game Theoretical Semantics
- Players
- Game rules
- Histories
- Strategies
- Truth falsity indeterminacy
- Conservativity
- Open formulas
- Skolem Semantics
- Skolemization
- Kreiselization
- Team Semantics
- Teams
- Duplicating and supplementing teams
- Uniform functions on teams
- Semantic clauses
- Relationship with Game Theoretical Semantics
- Notions of equivalence
- Equivalence of formulas
- Equivalence of sentences
- Equivalence relative to a context
- Sentence level
- Formula level
- Extended IF logic
- Properties and critique
- References
The introduction of IF logic was partly motivated by the attempt of extending the game-theoretical 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 (); 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 Hodges ().
IF 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).
IF 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
Hintikka has argued (e.g. in the book ) that IF and extended IF logic should be used as a basis for the foundations of mathematics; this proposal has been met in some cases with skepticism (see e.g.).
Syntax
A number of slightly different presentations of IF logic have appeared in the literature; here we follow.
Terms and atomic formulas
Terms and atomic formulas are defined exactly as in first-order logic with equality.
IF formulas
For a fixed signature σ, formulas of IF logic are defined as follows:
- Any atomic formula
φ is an IF formula. - If
φ is an IF formula, then¬ φ is an IF formula. - If
φ andψ are IF formulas, thenϕ ∧ ψ andϕ ∨ ψ are IF formulas. - If
φ is a formula,v is a variable, andV is a finite set of variables, then( ∃ v / V ) φ and( ∀ v / V ) φ are also IF formulas.
Free variables
The set
- If
φ is an atomic formula, thenFree ( φ ) is the set of all variables occurring in it. -
Free ( ¬ φ ) = Free ( φ ) ; -
Free ( φ ∨ ψ ) = Free ( φ ) ∪ Free ( ψ ) ; -
Free ( ( ∃ v / V ) φ ) = Free ( ( ∀ v / V ) φ ) = ( Free ( φ ) ∖ { v } ) ∪ 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
IF Sentences
An IF formula
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 (); the third one by Hodges in 1997 ().
In this section, we differentiate the three approaches by writing distinct pedices, as in
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
Players
The semantic game
Game rules
The allowed moves in the semantic game
- If
φ is a literal, the game ends, and, ifφ is true inM (in the first-order sense), then Eloise wins; otherwise, Abelard wins. - If
φ = ψ 1 ∧ ψ 2 ψ i G ( ψ i , M , s ) is played. - If
φ = ψ 1 ∨ ψ 2 ψ i G ( ψ i , M , s ) is played. - If
φ = ( ∀ v / V ) ψ , then Abelard chooses an elementa ofM , and gameG ( ψ , M , s ( a / v ) ) is played. - If
φ = ( ∃ v / V ) ψ , then Eloise chooses an elementa ofM , and gameG ( ψ , M , s ( a / v ) ) is played.
More generally, if
Histories
Informally, a sequence of moves in a game
The set
Given two assignments
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
Strategies
For a fixed game
A strategy for Eloise in the game
A strategy for Eloise is uniform if, whenever
A strategy
Truth, falsity, indeterminacy
An IF sentence
Conservativity
The semantics of IF logic thus defined is a conservative extension of first-order semantics, in the following sense. If
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
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
-
Sk U ( φ ) = φ ifφ is a literal. -
Sk U ( ψ ∘ χ ) = Sk U ( ψ ) ∘ Sk U ( χ ) if∘ = ∧ , ∨ . -
Sk U ( ( ∀ v / V ) ψ ) = ∀ v Sk U ∪ { v } ( ψ ) . -
Sk U ( ( ∃ v / V ) ψ ) = S u b ( Sk U ∪ { v } ( ψ ) , v , f v ( y 1 , . . . , y n ) ) , wherey 1 , . . . , y n U ∖ V .
If
Kreiselization
Given an IF formula
-
Kr U ( φ ) = ¬ φ ifφ is a literal. -
Kr U ( ψ ∧ χ ) = Kr U ( ψ ) ∨ Kr U ( χ ) . -
Kr U ( ψ ∨ χ ) = Kr U ( ψ ) ∧ Kr U ( χ ) . -
Kr U ( ( ∀ v / V ) ψ ) = S u b ( Kr U ∪ { v } ( ψ ) , v , g v ( y 1 , . . . , y n ) ) , wherey 1 , . . . , y n U ∖ V . -
Kr U ( ( ∃ v / V ) ψ ) = ∀ v Kr U ∪ { v } ( ψ )
If
Truth, falsity, indeterminacy
Given an IF sentence
An IF sentence is true on a structure
For any IF sentence, Skolem Semantics returns the same values as Game-theoretical Semantics.
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
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
X over a structureM and a variablev , the duplicating teamX [ M / v ] is the team{ s ( a / v ) | s ∈ X , a ∈ M } .
- Given a team
X over a structureM , a functionF : X → M and a variablev , the supplementing teamX [ F / v ] is the team{ s ( F ( s ) / v ) | s ∈ X } .
It is customary to replace repeated applications of these two operation with more succinct notations, such as
Uniform functions on teams
As above, given two assignments
Given a team
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:
-
M , X ⊨ + R t 1 … t n s ∈ X ,M , s ⊨ R t 1 … t n ( s ( t 1 ) … s ( t n ) ) is in the interpretationR M R ). -
M , X ⊨ + t 1 = t 2 s ∈ X ,M , s ⊨ t 1 = t 2 s ( t 1 ) = s ( t 2 ) ). -
M , X ⊨ + ¬ ϕ if and only ifM , X ⊨ − ϕ . -
M , X ⊨ + φ ∧ ψ if and only ifM , X ⊨ + φ andM , X ⊨ + ψ . -
M , X ⊨ + φ ∨ ψ if and only if there exist teamsY andZ such thatX = Y ∪ Z andM , Y ⊨ + φ andM , Z ⊨ + ψ . -
M , X ⊨ + ( ∀ v / V ) φ if and only ifM , X [ M / v ] ⊨ + φ . -
M , X ⊨ + ( ∃ v / V ) φ if and only if there exists aV -uniform functionF : X → M such thatM , X [ F / v ] ⊨ + ϕ .
Negative satisfaction:
-
M , X ⊨ − R t 1 … t n s ∈ X , the tuple( s ( t 1 ) … s ( t n ) ) is not in the interpretationR M R . -
M , X ⊨ − t 1 = t 2 s ∈ X ,s ( t 1 ) ≠ s ( t 2 ) . -
M , X ⊨ − ¬ ϕ if and only ifM , X ⊨ + ϕ . -
M , X ⊨ − φ ∧ ψ if and only if there exist teamsY andZ such thatX = Y ∪ Z andM , Y ⊨ − φ andM , Z ⊨ − ψ . -
M , X ⊨ − φ ∨ ψ if and only ifM , X ⊨ − φ andM , X ⊨ − ψ . -
M , X ⊨ + ( ∀ v / V ) φ if and only if there exists aV -uniform functionF : X → M such thatM , X [ F / v ] ⊨ + ϕ . -
M , X ⊨ + ( ∃ v / V ) φ if and only ifM , X [ M / v ] ⊨ + φ .
Truth, falsity, indeterminacy
According to team semantics, an IF sentence
Relationship with Game-Theoretical Semantics
For any team
From this it immediately follows that, for sentences
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
Equivalence of sentences
The definitions above specialize for IF sentences as follows. Two IF sentences
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
Sentence level
IF sentences can be translated in a truth-preserving fashion into sentences of (functional) existential second-order logic (
We denote by
Formula level
The notion of satisfiability by a team has the following properties:
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 of IF formulas into sentences of relational
where
Through this correlation, it is possible to say that, on a structure
In 2009, Kontinen and Väänänen, 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
Extended IF logic
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
Properties and critique
A number of properties of IF logic follow from logical equivalence with
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