Abstract
We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Armstrong, W. W. (1974). Dependency structures of data base relationships. In Information processing 74. Proc. IFIP Congress (pp. 580–583). Netherlands: North Holland.
Biering, B., Birkedal, L., Trop-Smith, N. (2007). BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems, 29(5), (to appear).
Cameron P., Hodges W. (2001) Some combinatorics of imperfect information. Journal of Symbolic Logic 66(2): 673–684
Curry H.B., Feys R. (1958) Combinatory logic. Volume 1, studies in logic and the foundations of mathematics. Netherlands, North Holland
Davey B.A., Priestley H.A. (2002) Introduction to lattices and order (2nd ed). Cambridge University Press, Cambridge
Fagin R. (1977) Functional dependencies in a relational data base and propositional logic. IBM Journal of Research and Development 21(6): 543–544
Girard J.-Y. (1987) Linear logic. Theoretical Computer Science 50: 1–102
Henkin L. (1950) Completeness in the theory of types. Journal of Symbolic Logic 15: 81–91
Henkin, L. (1961). Some remarks on infinitely long formulas. In Infinitistic methods. Proc. symposium on foundations of mathematics (pp. 167–183). Pergamon.
Hintikka J. (1998) The principles of mathematics revisited. Cambridge University Press, Cambridge
Hintikka J. (2002) Hyperclassical logic (a.k.a. IF logic) and its implications for logical theory. Bulletin of Symbolic Logic 8(3): 404–423
Hintikka J., Sandu G. et al (1989) Informational independence as a semantical phenomenon. In: Fenstad J.E. (eds) Logic, methodology and philosophy of science VIII. Elsevier, London, pp 571–589
Hintikka J., Sandu G. (1996) Game-theoretical semantics. In: van Benthem J., ter Meulen A. (eds) Handbook of logic and language. Elsevier, London
Hodges W. (1997a) Compositional semantics for a language of imperfect information. Logic Journal of the IGPL 5(4): 539–563
Hodges W. (1997b) Some strange quantifiers. In: Mycielski G.R.J., Salomaa A. (eds) Structures in logic and computer science. Lecture notes in computer science (Vol. 1261). Springer, New York, pp 51–65
Lang, S. (1964). Algebraic numbers. Addison-Wesley.
Lawvere F.W. (1969) Adjointness in foundations. Dialectica 23: 281–296
Lindström P. (1969) On extensions of elementary logic. Theoria 35: 1–11
Milner R. (1977) Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4: 1–22
Mitchell J.C. (1996) Foundations for programming languages. MIT Press, USA
Mitchell W.P.R., Simmons H. (2001) Monoid based semantics for linear formulas. Journal of Symbolic Logic 66(4): 1597–1619
O’Hearn P.W., Pym D.J. (1999) The logic of bunched implications. Bulletin of Symbolic Logic 5(2): 215–244
Pitts A. (2000) Categorical logic. In: Abramsky S., Gabbay D., Maibaum T. (eds) Handbook of logic in computer science (Vol. 5). Oxford University Press, Oxford, pp 39–128
Plotkin G.D. (1977) LCF considered as a programming language. Theoretical Computer Science 5: 223–255
Pym D.J. (2002) The semantics and proof theory of the logic of bunched implications. Applied logic series (Vol. 26). Kluwer, Netherlands
Pym D.J., O’Hearn P.W., Yang H. (2004) Possible worlds and resources: The semantics of BI. Theoretical Computer Science 315: 257–305
Reynolds, J. (2002). Separation logic: A logic for shared mutable data structures. In Proc. LiCS 2002. IEEE.
Rosenthal, K. I. (1990). Quantales and their applications. Pitman research notes in mathematics (No. 234). Longman Scientific and Technical.
Scott, D. S. (1969). Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory.
Tarski A. (1936) Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1: 261–405
Tarski, A., Vaught, R. (1956) Arithmetical extensions of relational systems. Compositio Mathematica, 81–102
Urquhart A. (1972) Semantics for relevant logics. Journal of Symbolic Logic 37(1): 159–169
Väänänen J. (2001) Second-order logic and foundations of mathematics. Bulletin of Symbolic Logic 7(4): 504–520
Väänänen J. (2007) Dependence logic. London Mathematical Society student texts (Vol. 70). Cambridge University Press, Cambridge
Winskel G. (1993) The formal semantics of programming languages. MIT Press, USA
Yetter D.N. (1990) Quantales and (noncommutative) linear logic. Journal of Symbolic Logic 55(1): 41–64
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Abramsky, S., Väänänen, J. From IF to BI. Synthese 167, 207–230 (2009). https://doi.org/10.1007/s11229-008-9415-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-008-9415-6