A smart child of Peano's (Q1344434)

From MaRDI portal
Revision as of 03:01, 5 March 2024 by Import240304020342 (talk | contribs) (Set profile property.)
scientific article
Language Label Description Also known as
English
A smart child of Peano's
scientific article

    Statements

    A smart child of Peano's (English)
    0 references
    0 references
    2 July 1995
    0 references
    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.
    0 references
    provability logic
    0 references
    necessitation
    0 references
    0 references

    Identifiers