A smart child of Peano's
type: Item
instance of: scholarly article
title: A smart child of Peano's
zbMATH Open document ID: 0815.03011
author: V. Yu. Shavrukov
published in: Notre Dame Journal of Formal Logic
publication date: 1995-07-02T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 721963
zbMATH Keywords: provability logic
zbMATH Keywords: necessitation
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1094061859
OpenAlex ID: W1972536043
DOI: 10.1305/NDJFL/1094061859
description: scientific article; zbMATH DE number 721963