Modal-epistemic variants of Shapiro's system of epistemic arithmetic (Q1344441)

Shapiro's Epistemic Arithmetic, EA, adds an operator, \(K\), to classical first-order arithmetic; this operator, interpreted informally as `is provable in principle', has an S4-like (Barcan-free) modal structure. First-order Heyting arithmetic, HA, can then be translated naturally into EA so that a formula \(A\) is provable in HA iff its translation is provable in EA. Here a Modal-Epistemic Arithmetic, MEA, is defined in which Shapiro's \(K\) is divided into a modal component, \(\diamondsuit\), for possibility, and an epistemic component, \(P\), for `is proved by some mathematician'. \(\diamondsuit\) has an S5-like modal structure (with Barcan) plus the axiom \(\diamondsuit A\to A\) when \(A\) is non-modal. Further postulates are given for \(P\) and combinations of \(P\) and \(\diamondsuit\). It is then shown that there is a translation from EA to MEA and hence a translation from HA to MEA such that \(A\) is provable in HA iff its translation is provable in MEA. A possible-worlds semantics is provided for one system of MEA and, although, of course, no full completeness theorem can be proved, the pure logical fragment of MEA is said to be semantically complete.