Prime-divisibility coding of a finite set (source code)

= Prime-divisibility coding of a finite set
{title2=$e\in F\iff p_e\mid d$}

An internally finite subset of $\{0,\ldots,c-1\}$ can be represented in <Peano arithmetic> by a product of distinct <prime numbers>: multiply the $e$th <prime number> exactly when $e$ belongs to the subset. Divisibility by that prime recovers membership. Arithmetic induction proves existence of this code even for a definable subset with a nonstandard cutoff in a <Nonstandard model of Peano arithmetic>.