= Pi-1 formula
{c}
A <Pi-1 formula> in the <arithmetical hierarchy> has the form $\forall n\,R(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 t\,R(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>.
Back to article page
