Hostname: page-component-8448b6f56d-t5pn6 Total loading time: 0 Render date: 2024-04-20T02:50:55.817Z Has data issue: false hasContentIssue false
  • English
  • Français

POSITIVE LOGIC WITH ADJOINT MODALITIES: PROOF THEORY, SEMANTICS, AND REASONING ABOUT INFORMATION

Published online by Cambridge University Press:  12 August 2010

MEHRNOOSH SADRZADEH  and
ROY DYCKHOFF
MEHRNOOSH SADRZADEH*
Affiliation:
Computing Laboratory, University of Oxford
ROY DYCKHOFF*
Affiliation:
School of Computer Science, St Andrews University
*
*OXFORD UNIVERSITY COMPUTING LABORATORY, OXFORD, UK. E-mail:mehrs@comlab.ox.ac.uk
†SCHOOL OF COMPUTER SCIENCE, ST ANDREWS UNIVERSITY, ST ANDREWS, SCOTLAND, UK. E-mail:rd@st-andrews.ac.uk
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider a simple modal logic whose nonmodal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of (e.g.) T, S4, and S5, such logics are useful, as shown in previous work by Baltag, Coecke, and the first author, for encoding and reasoning about information and misinformation in multiagent systems. For the propositional-only fragment of such a dynamic epistemic logic, we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 3 , Issue 3 , September 2010 , pp. 351 - 373
Copyright
Copyright © Association for Symbolic Logic 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Baltag, A., Coecke, B., & Sadrzadeh, M. (2007). Epistemic actions as resources. Journal of Logic and Computation, 17, 555–585.CrossRefGoogle Scholar
Baltag, A., & Moss, L. (2004). Logics for epistemic programs. Synthese, 139, 165–224.CrossRefGoogle Scholar
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic. Cambridge, UK: Cambridge University Press.CrossRefGoogle Scholar
Bonnette, N., & Goré, R. (1998). A labelled sequent system for tense logic Kt. In Antoniou, G., and Slaney, J. K., editors. Australian Joint Conference on Artificial Intelligence, Volume 1502 of Lecture Notes in Computer Science. London: Springer, pp. 71–82.Google Scholar
Brünnler, K. (2006). Deep sequent systems for modal logic. In Governatori, G., Hodkinson, I., and Venema, Y., editors. Advances in Modal Logic. Vol. 6. London: College Publications, pp. 107–119.Google Scholar
Celani, S., & Jansana, R. (1999). Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic. Logic Journal of the IGPL, 7, 683–715.CrossRefGoogle Scholar
Dunn, M. (2005). Positive modal logic. Studia Logica, 55, 301–317.CrossRefGoogle Scholar
Gehrke, M., Nagahashi, H., & Venema, Y. (2005). A Sahlqvist theorem for distributive modal logic. Annals of Pure and Applied Logic, 131, 65–102.CrossRefGoogle Scholar
Goré, R. (1998). Substructural logics on display. Logic Journal of the IGPL, 6(3), 451–504.CrossRefGoogle Scholar
Huth, M., & Ryan, M. (2000). Logic in Computer Science. Cambridge, UK: Cambridge University Press.Google Scholar
Kashima, R. (1994). Cut-free sequent calculi for some tense logics. Studia Logica, 53, 119–135.CrossRefGoogle Scholar
Kriener, J., Sadrzadeh, M., & Dyckhoff, R. (2009). Implementation of a cut-free sequent calculus for logics with adjoint modalities. Technical report, School of Computer Science, University of St Andrews, St Andrews, Scotland.Google Scholar
Moortgat, M. (1995). Multimodal linguistic inference. Logic Journal of the IGPL, 3, 371–401.CrossRefGoogle Scholar
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34, 507–544.CrossRefGoogle Scholar
Prior, A. (1968). Papers on Time and Tense. Oxford, UK: Oxford University Press.Google Scholar
Restall, G. (2000). An Introduction to Substructural Logics. London: Routledge.CrossRefGoogle Scholar
Richards, S., & Sadrzadeh, M. (2009). Aximo: Automated axiomatic reasoning for information update. Electronic Notes in Theoretical Computer Science, 231, 211–225.CrossRefGoogle Scholar
Sadrzadeh, M. (2006). Actions and Resources in Epistemic Logic. PhD Thesis, Université du Québec à Montréal.Google Scholar
Sadrzadeh, M. (2009). Ockham’s razor and reasoning about information flow. Synthese, 167, 391–408.CrossRefGoogle Scholar
Sadrzadeh, M., & Dyckhoff, R. (2009). Positive logic with adjoint modalities: Proof theory, semantics and reasoning about information. Electronic Notes in Theoretical Computer Science, 249, 451–470.CrossRefGoogle Scholar
Simpson, A. (1993). The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD Thesis, University of Edinburgh.Google Scholar
von Karger, B. (1998). Temporal algebras. Mathematical Structures in Computer Science, 8, 277–320.CrossRefGoogle Scholar
Wansing, H. (1994). Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, 4(2), 125–142.CrossRefGoogle Scholar