A Pi-1 formula in the arithmetical hierarchy has the form , with 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 , where checks that it has not halted in its first 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.
New to topics? Read the docs here!