Proof theory of epistemic logic of programs

• Authors: Maffezioli Paolo , Naibo Alberto
• Languages of publication: EN

Abstracts

EN

A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to give a step-by-step reconstruction of agents omniscience. In particular, its semantic assumptions are made explicit and a possible solution can be found in weakening the properties of the knowledge operator.

Keywords

EN

epistemic logic; dynamic propositional logic; structural proof theory; labelled sequent calculus; epistemic paradox

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2014
• Volume: 23
• Issue: 3
• Pages: 301–328

Dates

published

2014-09-01

online

2013-09-12

Contributors

author

Maffezioli Paolo

• Faculty of Philosophy, University of Groningen, Oude Boteringestraat 52, 9712 GL Groningen, the Netherlands

author

Naibo Alberto

• Department of Philosophy, University of Paris 1 Panthéon-Sorbonne 17, rue de la Sorbonne, 75005 Paris, France

References

• Aumann, R., “Agreeing to disagree”, Annals of Statistics, 4 (1976): 1236–1239. DOI: 10.1214/aos/1176343654
• Bull, R.A., “Cut elimination for propositional dynamic logic without *”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38 (1992): 85–100. DOI: 10.1002/malq.19920380107
• Dowek, G., “About folding-unfolding cuts and cuts modulo”, Journal of Logic and Computation, 11 (2001): 419–429. DOI: 10.1093/logcom/11.3.419
• Dummett, M., “What is a theory of meaning? (II)”, pages 67–137 in Truth and Meaning. Essays in semantics, G. Evans and J. McDowell (eds.), Oxford: Clarendon Press, 1976.
• Dummett, M., The Logical Basis of Metaphysics, London: Duckworth, 1991.
• Fagin, R., J.Y. Halpern, Y. Moses, and M.Y. Vardi, Reasoning about Knowledge, Cambridge (USA): MIT Press, 1995.
• Fitting, M., “Reasoning about games”, Studia Logica, 99 (2011): 143–169. DOI: 10.1007/s11225-011-9358-7
• Gentzen, G., “New version of the consistency proof for elementary number theory”, pages 252–286 in The Collected Papers of Gerhard Gentzen, M. Szabo (ed.), Amsterdam: North-Holland, 1969.
• Girard, J.-Y., Proof Theory and Logical Complexity (Vol. 1), Naples: Bibliopolis, 1987.
• Goldblatt, R., Logic of Time and Computation (2nd ed.), Stanford: CSLI Publications, 1992.
• Gödel, K., “An interpretation of the intuitionistic propositional calculus”, pages 296–302 in Collected Works (Vol. 3), S. Feferman et al. (eds.), Oxford: Oxford University Press, 2001.
• Hakli, R., and S. Negri, “Proof theory for distributed knowledge”, pages 100–116 in Computational Logic in Multi-Agent Systems 8th International Workshop, CLIMA VIII, Porto, Portugal, September 10-11, 2007, F. Sadri and K. Satoh (eds.), Lecture Notes in Artificial Intelligence (Vol. 5405), Berlin-Heidelberg: Springer, 2008. DOI: 10.1007/978-3-540-88833-8_6
• Harel, D., D. Kozen, and J. Tiuryn, Dynamic Logic, Cambridge, MA: MIT Press, 2000.
• Hill, B., and F. Poggiolesi, “A contraction-free and cut-free sequent calculus for propositional dynamic logic”, Studia Logica, 94 (2010): 47–72. DOI: 10.1007/s11225-010-9224-z
• Hintikka, J., Knowledge and Belief. An introduction to the logic of the two notions, Ithaca & London: Cornell University Press, 1962.
• Maffezioli, P., A. Naibo, and S. Negri, “The Church-Fitch knowability paradox in the light of structural proof theory”, Synthese (2012). DOI: 10.1007/s11229-012-0061-7
• Martin-Löf, P., “Verificationism then and now”, pages 187–196 in The Foundational Debate. Complexity and constructivity in mathematics and physics, W. DePauli-Schimanovich et al. (eds.), Dordrecht: Kluwer, 1995. DOI: 10.1007/978-94-017-3327-4_14
• Negri, S., “Contraction-free sequent calculi for geometric theories, with an application to Barr’s theorem”, Archive for Mathematical Logic, 42 (2003): 389–401. DOI: 10.1007/s001530100124
• Negri, S., “Proof analysis in modal logic”, Journal of Philosophical Logic, 34 (2005): 507–544. DOI: 10.1007/s10992-005-2267-3
• Negri, S., and J. von Plato, Structural Proof Theory, Cambridge: Cambridge University Press, 2001.
• Negri, S., and L. von Plato, Proof Analysis. A contribution to Hilbert’s last problem, Cambridge: Cambridge University Press, 2011.
• Pauly, M., and R. Parikh, “Game Logic: An overview”, Studia Logica, 75 (2003): 165–182.
• Sakalauskait˙ e, J., “A sequent calculus for propositional dynamic logic for agents with interactions”, Lithuanian Mathematical Journal, 45 (2005): 217–224. DOI: 10.1007/s10986-005-0025-4
• Salerno, J. (ed.), New Essays on the Knowability Paradox, Oxford: Oxford University Press, (2009).
• Schmidt, R., and D. Tishkovsky, “On combination of propositional dynamic logic and doxastic modal logics”, Journal of Logic, Language and Information, 17 (2008): 109–129. DOI: 10.1007/s10849-007-9041-6
• Sorensen, M.H., and P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Amsterdam: North-Holland, 2006.
• Troelstra, A.S., Lectures on Linear Logic, Stanford: CSLI Publications, 1992.
• Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory (2nd ed.), Cambridge: Cambridge University Press, 2000.
• Wittgenstein, L., Philosophical Investigations, Oxford: Blackwell, 1953.

Identifiers

DOI

10.12775/LLP.2013.026