TR-2003003: Finite Information Logic
Rohit Parikh, Jouko Väänánen · CUNY Academic Works (City University of New York) · 2003
we introduce a generalization of Independence Friendly (IF) logic in which Eloise is restricted to a nite amount of information about Abelard's moves. This Logic is shown to be equivalent to a sublogic ∃∀ of rst order logic, has the nite model property, and is decidable. Moreover, it gives an exponential compression relative to ∃∀ logic. Partial information logic is a generalization of both rst order logic and Hintikka-Sandu [3] IF-logic. We motivate this logic by means of an example. Suppose we have a model M on some domain D and some formula A = (∀x)(∀y)(∃z)R(x, y, z) where R is atomic. Then to this formula corresponds a game between two players Abelard and Eloise. Abelard chooses two elements a, b from D. Then Eloise chooses a third element c from D. If the formula R(a, b, c) holds in M then Eloise has won, else Abelard has. Now it can be shown that the formula A is true inM i Eloise has a winning strategy. The game as we have just desribed tells us how classical rst order logic works. To look at IF-logic we consider a slight variant. Let B be the variant of A obtained by writing B = (∀x)(∀y)(∃z/x)R(x, y, z). Now the game proceeds as before with Abelard choosing a, b and Eloise choosing c, but now, the choice of c has to be independent of a because the quanti er ∃z has now been marked by a /x, indicating independence of x, or as we might say, ignorance of x. But we could just as easily say that Eloise's knowledge is restricted to the value of y, i.e. to b. Instead of concentrating on what Eloise does not know we concentrate on what she does. Similar restrictions might of course apply to Abelard in case he too has a move which follows the move of Eloise. ∗City University of New York †University of Helsinki