Shappiro's Epistemic Arithmetic

大雑把に言って，言語 `L_arith` に `Box` を入れて様相に関して `S4` にしたものをShappiroのEpistemic Arithmetic `EA` と呼ぶ．

> [!NOTE]
> Gödel変換を $(\forall x. \varphi)^g \mapsto \Box \forall x. \varphi^g$ および $(\exists x.\varphi)^g \mapsto \exists x. \varphi^g$ と定めると，Heyting Arithmetic `HA` と `EA` はmodal companionを成す．

まずはとりあえずHeyting算術 #702 を作る必要があるが．