Sigma-1 completeness ($\mathbb{N}\models \sigma ⟹T⊢\sigma (\sigma \in {\Sigma }_1)$)

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⊢\sigma \to {\mathrm{Pr}}_T(┌\sigma ┐)$. Applying this to a provability assertion, which is itself Sigma-1, gives the third of the Hilbert-Bernays-Löb derivability conditions.