Proof theory of epistemic logic of programs
DOI:
https://doi.org/10.12775/LLP.2013.026Keywords
epistemic logic, dynamic propositional logic, structural proof theory, labelled sequent calculus, epistemic paradoxAbstract
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.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.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 747
Number of citations: 4
