A smart child of Peano's (Q1344434)

Let \(\square\varphi\) be interpreted as ``\(\varphi\) is provable in Peano arithmetic PA'', and \(\Delta\varphi\) be interpreted as ``there exists \(n\) such that \(I\Sigma_ n\) is consistent and proves \(\varphi\)''. Then the logic LF of propositional formulas whose interpretation is provable in PA is axiomatized by the standard axioms for \(\square\) plus the formulas \(\Delta(\varphi\to \psi)\to (\Delta \varphi\to \Delta\psi)\); \(\square \varphi\to \square\Delta\varphi\); \(\square \varphi\to \Delta\square\varphi\); \(\square \varphi\to (\Delta\varphi\vee\square \perp)\); \(\neg\Delta\perp\); \(\Delta\varphi\to \Delta((\Delta\psi\to \psi)\vee \Delta\varphi)\) and necessitation rules for \(\square\) and \(\Delta\). The \(\Delta\)-fragment is obtained by deleting axioms and rules involving \(\square\). If the provability of the interpretation in PA is replaced by its truth in the standard model, then one has to add \(\square\varphi\to \varphi\) and \(\Delta\varphi\to (\varphi\wedge \Delta\Delta\varphi)\) with the standard restriction on necessitation.