In defense of epistemic arithmetic (Q1299766)

Epistemic Arithmetic, EA, adds an S4-like epistemic operator, \(K\), to classical first-order arithmetic. It is useful for the formalization of intuitionistic arithmetic, since first-order Heyting arithmetic, HA, can be faithfully translated into EA, and there hold some informal mathematical principles, such as especially Church's Thesis. This article defends EA against two philosophical objections. The first, due to Smoryński, is that EA fails to capture the full idea of effective methods so essential for intuitionistic mathematics. The second, due to Hazen, is that EA is contrary to intuitionism's anti-realism. Both are found wanting, chiefly on grounds that they ask too much of formalization. Here formalization is construed as a theory and so is to be judged by the virtues of any scientific theory. It should not be required that formalization preserve meaning in a strong sense. Beyond this, the article examines how Church's Thesis might be formulated in EA. Standard formulations can be shown to be inadequate, and whether a fully adequate formalization is possible remains an open question, though the author is optimistic. This may, however, require a higher-order epistemic theory, where much work remains to be done.