You are here
HomeIFlogic
Primary tabs
IFlogic
Independence Friendly logic (IFlogic) is an interesting conservative extension of classical firstorder logic based on very natural ideas from game theoretical semantics developed by Jaakko Hintikka and Gabriel Sandu among others. Although IFlogic is a conservative extension of first order logic, it has a number of interesting properties, such as allowing truthdefinitions and admitting a translation of all $\Sigma^{1}_{1}$ sentences (secondorder sentences with an initial secondorder existential quantifier followed by a firstorder sentence).
IFlogic can be characterised as the natural extension of firstorder logic when one allows informational independence to occur in the gametheoretical truth definition. To understand this idea we need first to introduce the game theoretical definition of truth for classical firstorder logic.
To each firstorder sentence $\phi$ we assign a game $G(\phi)$ with two players played on models of the appropriate language. 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(\phi)$ is defined as follows. We will use the convention that if $p$ is a symbol that names a function, a predicate or an object of the model $M$, then $p^{M}$ is that named entity.

if $P$ is an $n$ary predicate and $t_{i}$ are names of elements of the model, then $G(P(t_{1},...,t_{n}))$ is a game in which the verifier immediately wins if $(t^{M}_{1},...,t^{M}_{n})\in P^{M}$, otherwise the falsifier immediately wins.

the game $G(\phi_{1}\vee\phi_{2})$ begins with the choice $\phi_{i}$ from $\phi_{1}$ and $\phi_{2}$ ($i=1$ or $i=2$) by the verifier, and then proceeds as the game $G(\phi_{i})$

the game $G(\phi_{1}\wedge\phi_{2})$ is the same as $G(\phi_{1}\vee\phi_{2})$, except that the choice is made by the falsifier

the game $G(\exists x\phi(x))$ begins with the choice by verifier of a member of $M$ which is given a name $\mathbf{a}$, and then proceeds as $G(\phi(\mathbf{a}))$

the game $G(\forall x\phi(x))$ is the same as $G(\exists x\phi(x))$, except that the choice of $\mathbf{a}$ is made by the falsifier

the game $G(\neg\phi)$ is the same as $G(\phi)$ with the roles of the falsifier and verifier exchanged
Truth of a sentence $\phi$ is defined as the existence of a winning strategy for verifier for the game $G(\phi)$. Similarly, falsity of $\phi$ is defined as the existence of a winning strategy for the falsifier for the game $G(\phi)$. (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 firstorder logic, this definition is equivalent to the usual Tarskian definition of truth (i.e. the one based on satisfaction found in most treatments of semantics of firstorder logic). This means also that since the law of excluded middle holds for firstorder logic that the games $G(\phi)$ have a very strong property: either the falsifier or the verifier has a winning strategy.
Notice that all rules except those for negation 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 $\forall x(P(x)\vee Q(x))$. The corresponding game begins with the falsifier picking an element $\mathbf{a}$ from the model, so a strategy for the verifier must specify for each element $\mathbf{a}$ which of $Q(\mathbf{a})$ and $P(\mathbf{a})$ 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 $\forall x(P(x)\vee Q(x))$ is equivalent to $\exists f\forall xP(x)\wedge f(x)=0\vee Q(x)\wedge f(x)=1$. Let’s consider a more complicated example: $\forall x\exists y\forall z\exists s\neg P(x,y,z,s)$. The truth of this is equivalent to the existence of a functions $f$ and $g$, s.t. $\forall x\forall zP(x,f(x),z,g(z))$.
These sort of functions are known as Skolem functions, and they are in essence just winning strategies for the verifier. We won’t prove it here, but all firstorder sentences can be expressed in form $\exists f_{1}...\exists f_{n}\forall x_{1}...\forall x_{k}\phi$, where $\phi$ is a truthfunctional combination of atomic sentences in which all terms are either constants or variables $x_{i}$ or formed by application of the functions $f_{i}$ to such terms. Such sentences are said to be in $\Sigma^{1}_{1}$ form.
Let’s consider a $\Sigma^{1}_{1}$ sentence $\exists f\exists g\forall x\forall z\phi(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) firstorder formula! Let’s see what such a strategy would look like. First, the falsifier chooses elements $\mathbf{a}$ and $\mathbf{b}$ to serve as $x$ and $y$. Then the verifier chooses an element $\mathbf{c}$ knowing only $\mathbf{a}$ and an element $\mathbf{d}$ knowing only $\mathbf{b}$. The verifier’s goal is that $\phi(\mathbf{a},\mathbf{c},\mathbf{b},\mathbf{d})$ 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 $\mathbf{c}$, the other one picking $\mathbf{d}$.
From a gametheoretical 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.
IFlogic comes out of the gametheoretical definition in a natural way if we allow informational independence in our semantical games. In IFlogic, every connective can be augmented with an independence marker $//$, so that $*//*^{{\prime}}$ means that the game for the occurrence of $*^{{\prime}}$ within the scope of $*$ must be played without knowledge of the choices made for $*$. For example $(\forall x//\exists y)\exists y\phi(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. $\phi(x,y)$ comes out true. This is not a very characteristic example, as it can be written as an ordinary firstorder formula $\exists y\forall x\phi(x,y)$. The curious game we described above corresponding to the secondorder Skolemfunction formulation $\Sigma^{1}_{1}$ sentence $\exists f\exists g\forall x\forall z\phi(x,f(x),y,g(z))$ corresponds to an IFsentence $(\forall x//\exists y)(\forall z//\exists u)(\exists y)(\exists u)\phi(x,y,z,u)$. IFlogic allows informational independence also for the usual logical connectives, for example $(\forall x//\vee)(\phi(x)\vee\psi(x))$ is true if and only if for all $x$, either $\phi(x)$ or $\psi(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 IFlogic is that every $\Sigma^{1}_{1}$ formula $\phi$ has an IFtranslation $\phi^{I}F$ which is true if and only if $\phi$ is true (the equivalence does not in general hold if we replace ’true’ with ’false’). Since for example firstorder truth (in a model) is $\Sigma^{1}_{1}$ definable (it’s just quantification over all possible valuations, which are secondorder objects), there are IFtheories which correctly represent the truth predicate for their firstorder part. What is even more striking is that sufficiently strong IFtheories 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 assumption that the logic is closed under contradictory negation. This is not the case for IFlogic. In general for a given sentence $\phi$ there is no sentence $\phi*$ that is true just in case $\phi$ is not true. Thus the law of excluded middle does not hold in general in IFlogic (although it does for the classical firstorder 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 10letter word and you have one go at guessing it is not determined in this sense, since there is no 10letter word you couldn’t guess, and on the other hand you have no way of forcing me to choose any particular 10letter word (which would guarantee your victory).
IFlogic is stronger than firstorder logic in the usual sense that there are classes of structures which are IFdefinable but not firstorder definable. Some of these are even finite. Many interesting concepts are expressible in IFlogic, such as equicardinality, infinity (which can be expressed by a logical formula in contradistinction to ordinary firstorder logic in which nonlogical symbols are needed), and wellordering.
By Lindström’s theorem we thus know that either IFlogic is not complete (i.e. its set of validities is not r.e.) or the LöwenheimSkolem theorem does not hold. In fact, the (downward) LöwenheimSkolem theorem does hold for IFlogic, so it’s not complete. There is a complete disproof procedure for IFlogic, but because IFlogic is not closed under contradictory negation this does not yield a complete proof procedure.
IFlogic can be extended by allowing contradictory negations of closed sentences and truth functional combinations thereof. This extended IFlogic is extremely strong. For example, the secondorder induction axiom for PA is $\forall X((X(0)\wedge\forall y(X(y)\rightarrow X(y+1)))\rightarrow\forall yX(y))$. The negation of this is a $\Sigma^{1}_{1}$ sentence asserting the existence of a set that invalidates the induction axiom. Since $\Sigma^{1}_{1}$ sentences are expressible in IFlogic, we can translate the negation of the induction axiom into IFsentence $\phi$. But now $\neg\phi$ is a formula of extended IFlogic, and is clearly equivalent to the usual induction axiom! As all the rest of PA axioms are first order, this shows that extended IFlogic PA can correctly define the natural number system.
There exists also an interesting “translation” of $n$thorder logic into extended IFlogic. Consider an $n$sorted firstorder language and an $n$thorder 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 $\Pi^{1}_{1}$ 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 $n$thorder logic. The negation of this axiom is again $\Sigma^{1}_{1}$ and translatable into IFlogic, and thus the axiom itself is expressible in extended IFlogic. Moreover, since most interesting secondorder theories are finitely axiomatisable, we can consider sentences of form $T*\rightarrow\phi$ (where $T*$ is the multisorted translation of $T$), which express logical implication of $\phi$ by $T$ (correctly). This is equivalent to $\neg(T*)\vee\phi$ (where $\neg$ is contradictory), but since $T*$ is a conjunction of a $\Pi^{1}_{1}$sentenceasserting comprehension translated into extended IFlogic and firstorder translation of the axioms of $T$, this is a $\Sigma_{1}^{1}$ formula translatable to nonextended IFlogic and so is $\phi$. Thus sentences of form $T\rightarrow\phi$ of $n$thorder logic are translatable into IFsentences which are true just in case the originals were.
Mathematics Subject Classification
03B99 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
Recent Activity
new question: Prove a formula is part of the Gentzen System by LadyAnne
Mar 30
new question: A problem about Euler's totient function by mbhatia
new problem: Problem: Show that phi(a^n1), (where phi is the Euler totient function), is divisible by n for any natural number n and any natural number a >1. by mbhatia
new problem: MSC browser just displays "No articles found. Up to ." by jaimeglz
Mar 26
new correction: Misspelled name by DavidSteinsaltz
Mar 21
new correction: underlinetypo by Filipe
Mar 19
new correction: cocycle pro cocyle by pahio
Mar 7
new image: plot W(t) = P(waiting time <= t) (2nd attempt) by robert_dodier
new image: expected waiting time by robert_dodier
new image: plot W(t) = P(waiting time <= t) by robert_dodier