Independence Friendly logic (IF-logic) is an interesting conservative extension of classical first-order logic based on very natural ideas from game theoretical semantics developed by Jaakko Hintikka and Gabriel Sandu among others. Although IF-logic is a conservative extension of first order logic, it has a number of interesting properties, such as allowing truth-definitions and admitting a translation of all Σ11 sentencesMathworldPlanetmath (second-order sentences with an initial second-order existential quantifierMathworldPlanetmath followed by a first-order sentence).

IF-logic can be characterised as the natural extensionPlanetmathPlanetmath of first-order logic when one allows informational independence to occur in the game-theoretical truth definition. To understand this idea we need first to introduce the game theoretical definition of truth for classical first-order logic.

To each first-order sentence ϕ we assign a game G(ϕ) with two players played on models of the appropriate languagePlanetmathPlanetmath. The two players are called verifier and falsifier (or nature). The idea is that the verifier attempts to show that the sentence is true in the model, while the falsifier attempts to show that it is false in the model. The game G(ϕ) is defined as follows. We will use the convention that if p is a symbol that names a function, a predicateMathworldPlanetmath or an object of the model M, then pM is that named entity.

  • if P is an n-ary predicate and ti are names of elements of the model, then G(P(t1,,tn)) is a game in which the verifier immediately wins if (t1M,,tnM)PM, otherwise the falsifier immediately wins.

  • the game G(ϕ1ϕ2) begins with the choice ϕi from ϕ1 and ϕ2 (i=1 or i=2) by the verifier, and then proceeds as the game G(ϕi)

  • the game G(ϕ1ϕ2) is the same as G(ϕ1ϕ2), except that the choice is made by the falsifier

  • the game G(xϕ(x)) begins with the choice by verifier of a member of M which is given a name 𝐚, and then proceeds as G(ϕ(𝐚))

  • the game G(xϕ(x)) is the same as G(xϕ(x)), except that the choice of 𝐚 is made by the falsifier

  • the game G(¬ϕ) is the same as G(ϕ) with the roles of the falsifier and verifier exchanged

Truth of a sentence ϕ is defined as the existence of a winning strategy for verifier for the game G(ϕ). Similarly, falsity of ϕ is defined as the existence of a winning strategy for the falsifier for the game G(ϕ). (A strategy is a specification that determines for each move of the opponent what the player should do. A winning strategy is a strategy which guarantees victory no matter what strategy the opponent follows.)

For classical first-order logic, this definition is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to the usual Tarskian definition of truth (i.e. the one based on satisfactionMathworldPlanetmath found in most treatments of semantics of first-order logic). This means also that since the law of excluded middleMathworldPlanetmathPlanetmath holds for first-order logic that the games G(ϕ) have a very strong property: either the falsifier or the verifier has a winning strategy.

Notice that all rules except those for negationMathworldPlanetmath and atomic sentences concern choosing a sentence or finding an element. These can be codified into functions, which tell us which sentence to pick or which element of the model to choose, based on our previous choices and those of our opponent. For example, consider the sentence x(P(x)Q(x)). The corresponding game begins with the falsifier picking an element 𝐚 from the model, so a strategy for the verifier must specify for each element 𝐚 which of Q(𝐚) and P(𝐚) to pick. The truth of the sentence is equivalent to the existence of a winning strategy for the verifier, i.e. just such a function. But this means that x(P(x)Q(x)) is equivalent to fxP(x)f(x)=0Q(x)f(x)=1. Let’s consider a more complicated example: xyzs¬P(x,y,z,s). The truth of this is equivalent to the existence of a functions f and g, s.t. xzP(x,f(x),z,g(z)).

These sort of functions are known as Skolem functionsMathworldPlanetmath, and they are in essence just winning strategies for the verifier. We won’t prove it here, but all first-order sentences can be expressed in form f1fnx1xkϕ, where ϕ is a truth-functional combinationMathworldPlanetmathPlanetmath of atomic sentences in which all terms are either constants or variables xi or formed by application of the functions fi to such terms. Such sentences are said to be in Σ11 form.

Let’s consider a Σ11 sentence fgxzϕ(x,f(x),y,g(z)). Up front, it seems to assert the existence of a winning strategy in a simple semantical game like those described above. However, the game can’t correspond to any (classical) first-order formulaMathworldPlanetmath! Let’s see what such a strategy would look like. First, the falsifier chooses elements 𝐚 and 𝐛 to serve as x and y. Then the verifier chooses an element 𝐜 knowing only 𝐚 and an element 𝐝 knowing only 𝐛. The verifier’s goal is that ϕ(𝐚,𝐜,𝐛,𝐝) comes out as a true atomic sentence. The game could actually be arranged so that the verifier is a team of two players (who aren’t allowed to communicate with each other), one of which picks 𝐜, the other one picking 𝐝.

From a game-theoretical point of view, games in which some moves must be made without depending on some of the earlier moves are called “informationally incomplete” games, and they occur very commonly. Bridge is such a game, for example, and usually real examples of such games have “players” being actually teams made up of several people.

IF-logic comes out of the game-theoretical definition in a natural way if we allow informational independence in our semantical games. In IF-logic, every connectiveMathworldPlanetmath can be augmented with an independence marker //, so that *//* means that the game for the occurrence of * within the scope of * must be played without knowledge of the choices made for *. For example (x//y)yϕ(x,y) asserts that for any choice of value for x by the falsifier, the verifier can find a value for y that does not depend on the value of x, s.t. ϕ(x,y) comes out true. This is not a very characteristic example, as it can be written as an ordinary first-order formula yxϕ(x,y). The curious game we described above corresponding to the second-order Skolem-function formulation Σ11 sentence fgxzϕ(x,f(x),y,g(z)) corresponds to an IF-sentence (x//y)(z//u)(y)(u)ϕ(x,y,z,u). IF-logic allows informational independence also for the usual logical connectives, for example (x//)(ϕ(x)ψ(x)) is true if and only if for all x, either ϕ(x) or ψ(x) is true, but which of these is picked by the verifier must be decided independently of the choice for x by the falsifier.

One of the striking characteristics of IF-logic is that every Σ11 formula ϕ has an IF-translation ϕIF which is true if and only if ϕ is true (the equivalence does not in general hold if we replace ’true’ with ’false’). Since for example first-order truth (in a model) is Σ11 definable (it’s just quantification over all possible valuations, which are second-order objects), there are IF-theories which correctly represent the truth predicate for their first-order part. What is even more striking is that sufficiently strong IF-theories can do this for the whole of the language they are expressed in.

This seems to contradict Tarski’s famous result on the undefinability of truth, but this is illusory. Tarski’s result depends on the assumptionPlanetmathPlanetmath that the logic is closed under contradictory negation. This is not the case for IF-logic. In general for a given sentence ϕ there is no sentence ϕ* that is true just in case ϕ is not true. Thus the law of excluded middle does not hold in general in IF-logic (although it does for the classical first-order portion). This is quite unsurprising since games of imperfect information are very seldom determined in the sense that either the verifier or the falsifier has a winning strategy. For example, a game in which I choose a 10-letter word and you have one go at guessing it is not determined in this sense, since there is no 10-letter word you couldn’t guess, and on the other hand you have no way of forcingMathworldPlanetmath me to choose any particular 10-letter word (which would guarantee your victory).

IF-logic is stronger than first-order logic in the usual sense that there are classes of structuresMathworldPlanetmath which are IF-definable but not first-order definable. Some of these are even finite. Many interesting conceptsMathworldPlanetmath are expressible in IF-logic, such as equicardinality, infinityMathworldPlanetmath (which can be expressed by a logical formula in contradistinction to ordinary first-order logic in which non-logical symbols are needed), and well-ordering.

By Lindström’s theorem we thus know that either IF-logic is not completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath (i.e. its set of validities is not r.e.) or the Löwenheim-Skolem theorem does not hold. In fact, the (downward) Löwenheim-Skolem theorem does hold for IF-logic, so it’s not complete. There is a complete disproof procedure for IF-logic, but because IF-logic is not closed under contradictory negation this does not yield a complete proof procedure.

IF-logic can be extended by allowing contradictory negations of closed sentences and truth functionalPlanetmathPlanetmathPlanetmathPlanetmath combinations thereof. This extended IF-logic is extremely strong. For example, the second-order induction axiomMathworldPlanetmath for PA is X((X(0)y(X(y)X(y+1)))yX(y)). The negation of this is a Σ11 sentence asserting the existence of a set that invalidates the induction axiom. Since Σ11 sentences are expressible in IF-logic, we can translate the negation of the induction axiom into IF-sentence ϕ. But now ¬ϕ is a formula of extended IF-logic, and is clearly equivalent to the usual induction axiom! As all the rest of PA axioms are first order, this shows that extended IF-logic PA can correctly define the natural numberMathworldPlanetmath system.

There exists also an interesting “translation” of nth-order logic into extended IF-logic. Consider an n-sorted first-order language and an nth-order theory T translated into this language. Now, extend the language to second order and add the axiom stating that the sort k+1 actually comprises the whole of the powerset of the sort k. This is a Π11 sentence (i.e. of the form “for all predicates P there is a first order element of sort k+1 that comprises exactly the k extension of P”). It is easy to see that a formula is valid in this new system if and only if it was valid in the original nth-order logic. The negation of this axiom is again Σ11 and translatable into IF-logic, and thus the axiom itself is expressible in extended IF-logic. Moreover, since most interesting second-order theories are finitely axiomatisable, we can consider sentences of form T*ϕ (where T* is the multisorted translation of T), which express logical implication of ϕ by T (correctly). This is equivalent to ¬(T*)ϕ (where ¬ is contradictory), but since T* is a conjunctionMathworldPlanetmath of a Π11-sentence-asserting comprehension translated into extended IF-logic and first-order translation of the axioms of T, this is a Σ11 formula translatable to non-extended IF-logic and so is ϕ. Thus sentences of form Tϕ of nth-order logic are translatable into IF-sentences which are true just in case the originals were.

Title IF-logic
Canonical name IFlogic
Date of creation 2013-03-22 13:50:46
Last modified on 2013-03-22 13:50:46
Owner mathcam (2727)
Last modified by mathcam (2727)
Numerical id 9
Author mathcam (2727)
Entry type Definition
Classification msc 03B99
Synonym Independence Friendly logic
Related topic SecondOrderLogic
Related topic TarskisResultOnTheUndefinabilityOfTruth
Defines IF-logic
Defines Independence Friendly logic