= Numeralwise enumeration in arithmetic
{title2=$n\in A\Rightarrow\exists m\ S\vdash P(\bar n,\bar m)$}
A two-variable formula enumerates a <set> $A$ in a <first-order theory>[theory] $S$ when membership supplies a standard <numeral> stage whose instance is provable, while nonmembership makes every standard-stage instance refutable. The notion contains these proof obligations, not merely a syntactic complexity restriction on the formula. With <bounded completeness of an arithmetic theory>[bounded completeness], a bounded formula whose existential closure defines a <computably enumerable set> provides such an enumerator.https://people.cs.uchicago.edu/~razborov/teaching/files/godel.pdf[Incompleteness Theorems, section3, definition of enumeration in a proof system]{ref}
Back to article page
