Arithmetical Interpretations of Dynamic Logic
Hajek, Petr
J. Symbolic Logic, Tome 48 (1983) no. 1, p. 704-713 / Harvested from Project Euclid
An arithmetical interpretation of dynamic propositional logic (DPL) is a mapping $f$ satisfying the following: (1) $f$ associates with each formula $A$ of DPL a sentence $f(A)$ of Peano arithmetic (PA) and with each program $\alpha$ a formula $f(\alpha)$ of PA with one free variable describing formally a supertheory of PA; (2) $f$ commutes with logical connectives; (3) $f(\lbrack\alpha\rbrack A)$ is the sentence saying that $f(A)$ is provable in the theory $f(\alpha)$; (4) for each axiom $A$ of DPL, $f(A)$ is provable in PA (and consequently, for each $A$ provable in DPL, $f(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 $f, f(A)$ is provable in PA. Various modifications of this result are considered.
Publié le : 1983-09-14
Classification: 
@article{1183741330,
     author = {Hajek, Petr},
     title = {Arithmetical Interpretations of Dynamic Logic},
     journal = {J. Symbolic Logic},
     volume = {48},
     number = {1},
     year = {1983},
     pages = { 704-713},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183741330}
}
Hajek, Petr. Arithmetical Interpretations of Dynamic Logic. J. Symbolic Logic, Tome 48 (1983) no. 1, pp.  704-713. http://gdmltest.u-ga.fr/item/1183741330/