= Sigma-1 completeness
{c}
{title2=$\mathbb N\models\sigma\Longrightarrow T\vdash\sigma\quad(\sigma\in\Sigma_1)$}
= Sigma-1 complete
{c}
{synonym}
An arithmetic theory is <Sigma-1 complete> when it proves every true <Sigma-1 formula> that is a sentence. A genuine finite proof gives a true existential assertion that a code is a proof; Sigma-1 completeness therefore supplies the external necessitation clause for the usual <arithmetical provability predicate>. Its formalized version says that, for each Sigma-1 sentence $\sigma$, $T\vdash\sigma\to\operatorname{Pr}_T(\ulcorner\sigma\urcorner)$. Applying this to a provability assertion, which is itself Sigma-1, gives the third of the <Hilbert-Bernays-Löb derivability conditions>.
Back to article page
