Arithmetical interpretations of dynamic logic
- 1 September 1983
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 48 (3) , 704-713
- https://doi.org/10.2307/2273463
Abstract
An arithmetical interpretation of dynamic propositional logic (DPL) is a mapping ƒ satisfying the following: (1) ƒ associates with each formula A of DPL a sentence ƒ(A) of Peano arithmetic (PA) and with each program α a formula ƒ(α) of PA with one free variable describing formally a supertheory of PA; (2) ƒ commutes with logical connectives; (3) ƒ([α]A) is the sentence saying that ƒ(A) is provable in the theory ƒ(α); (4) for each axiom A of DPL, ƒ(A) is provable in PA (and consequently, for each A provable in DPL, ƒ(A) is provable in PA). The arithmetical completeness theorem is proved saying that a formula A of DPL is provable in DPL iff for each arithmetical interpretation ƒ, ƒ(A) is provable in PA. Various modifications of this result are considered.Keywords
This publication has 7 references indexed in Scilit:
- Self-Reference and Modal LogicPublished by Springer Nature ,1985
- Interpolation in loop-free logicStudia Logica, 1980
- Algorithm = logic + controlCommunications of the ACM, 1979
- The completeness of propositional dynamic logicPublished by Springer Nature ,1978
- Provability interpretations of modal logicIsrael Journal of Mathematics, 1976
- Semantical Analysis of Modal Logic I Normal Modal Propositional CalculiMathematical Logic Quarterly, 1963
- Arithmetization of metamathematics in a general settingFundamenta Mathematicae, 1960