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 sentences (second-order sentences with an initial second-order existential quantifier followed by a first-order sentence).
IF-logic can be characterised as the natural extension 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 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 is defined as follows. We will use the convention that if is a symbol that names a function, a predicate or an object of the model , then is that named entity.
if is an -ary predicate and are names of elements of the model, then is a game in which the verifier immediately wins if , otherwise the falsifier immediately wins.
the game begins with the choice from and ( or ) by the verifier, and then proceeds as the game
the game is the same as , except that the choice is made by the falsifier
the game begins with the choice by verifier of a member of which is given a name , and then proceeds as
the game is the same as , except that the choice of is made by the falsifier
the game is the same as 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 . Similarly, falsity of is defined as the existence of a winning strategy for the falsifier for the game . (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 equivalent to the usual Tarskian definition of truth (i.e. the one based on satisfaction found in most treatments of semantics of first-order logic). This means also that since the law of excluded middle holds for first-order logic that the games 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 . 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 and 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 is equivalent to . Let’s consider a more complicated example: . The truth of this is equivalent to the existence of a functions and , s.t. .
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 first-order sentences can be expressed in form , where is a truth-functional combination of atomic sentences in which all terms are either constants or variables or formed by application of the functions to such terms. Such sentences are said to be in form.
Let’s consider a sentence . 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 formula! Let’s see what such a strategy would look like. First, the falsifier chooses elements and to serve as and . 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 connective 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 asserts that for any choice of value for by the falsifier, the verifier can find a value for that does not depend on the value of , s.t. comes out true. This is not a very characteristic example, as it can be written as an ordinary first-order formula . The curious game we described above corresponding to the second-order Skolem-function formulation sentence corresponds to an IF-sentence . IF-logic allows informational independence also for the usual logical connectives, for example is true if and only if for all , either or is true, but which of these is picked by the verifier must be decided independently of the choice for by the falsifier.
One of the striking characteristics of IF-logic is that every formula has an IF-translation 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 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 assumption 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 forcing 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 structures which are IF-definable but not first-order definable. Some of these are even finite. Many interesting concepts are expressible in IF-logic, such as equicardinality, infinity (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 complete (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 functional combinations thereof. This extended IF-logic is extremely strong. For example, the second-order induction axiom for PA is . The negation of this is a sentence asserting the existence of a set that invalidates the induction axiom. Since 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 number system.
There exists also an interesting “translation” of th-order logic into extended IF-logic. Consider an -sorted first-order language and an th-order theory translated into this language. Now, extend the language to second order and add the axiom stating that the sort actually comprises the whole of the powerset of the sort . This is a sentence (i.e. of the form “for all predicates P there is a first order element of sort that comprises exactly the extension of ”). It is easy to see that a formula is valid in this new system if and only if it was valid in the original th-order logic. The negation of this axiom is again 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 (where is the multisorted translation of ), which express logical implication of by (correctly). This is equivalent to (where is contradictory), but since is a conjunction of a -sentence-asserting comprehension translated into extended IF-logic and first-order translation of the axioms of , this is a formula translatable to non-extended IF-logic and so is . Thus sentences of form of th-order logic are translatable into IF-sentences which are true just in case the originals were.
|Date of creation||2013-03-22 13:50:46|
|Last modified on||2013-03-22 13:50:46|
|Last modified by||mathcam (2727)|
|Synonym||Independence Friendly logic|
|Defines||Independence Friendly logic|