A formula "F"("x") that contains exactly one free variable "x" is called a "statement form" or "class-sign". As soon as "x" is replaced by a specific number, the statement form turns into a "bona fide" statement, and it is then either provable in the system, or not. For certain formulas one can show that for every natural number n, F(n) is true if and only if it can be proved (the precise requirement in the original proof is weaker, but for the proof sketch this will suffice). In particular, this is true for every specific arithmetic operation between a finite number of natural numbers, such as "2×3=6".