Sigma-1 formula

A ${\Sigma }_1$ formula is equivalent to $\exists \mathbf{y}\delta$ with $\delta$ bounded. A ${\Pi }_1$ formula is equivalent to $\forall \mathbf{y}\delta$ with $\delta$ bounded.

If a total single-valued numerical function has a Sigma-1 graph, the complement of that graph is also Sigma-1. An input-output pair is outside the graph exactly when some different output is in the graph. Totality and uniqueness are essential to that equivalence. Stage-comparison separation of enumerations of the graph and its complement then gives weak definability of a numerical function in a bounded-complete arithmetic first-order theory.

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.

A Pi-1 formula in the arithmetical hierarchy has the form $\forall nR(n,\mathbf{x})$, with $R$ a decidable predicate; several universal number quantifiers can be combined by coding tuples. In a formal arithmetic presentation, the matrix is taken to have bounded quantifiers, with equivalent computable-predicate normal forms obtained by coding computations.

For example, the assertion that a fixed Turing machine never halts is $\forall tR(t)$, where $R(t)$ checks that it has not halted in its first $t$ steps. A false such assertion has a finite counterexample, while a true one need not have a finite computational certificate. Negating a Pi-1 formula gives a Sigma-1 formula.