any larger integer X by this definition requires knowing the primality of every integer between 1 and X, which is well defined by this definition. That last point can be proved by induction on X, for which it is essential that the second clause says "if and only if"; if it had just said "if", the primality of, for instance, the number 4 would not be clear, and the further application of the second clause would be impossible. Non-negative even numbers The even numbers can be defined as consisting of 0 is in the set E of non-negative evens (basis clause), For any element x in the set E, x + 2 is in E (inductive clause), Nothing is in E unless it is obtained from the basis and inductive clauses (extremal clause). Well formed formulas It is chiefly in logic or computer programming that recursive definitions are found. For example, a well-formed formula (wff) can be defined as: a symbol which stands for a proposition – like p means "Connor is a lawyer." The negation symbol, followed by a wff – like Np means "It is not true that Connor is a lawyer." Any of the four binary connectives (C, A, K, or E) followed by two wffs. The symbol K means "both are true", so Kpq may mean "Connor is a lawyer, and Mary likes music." The value of such a recursive definition is that it can be used to determine whether any particular string of symbols is "well formed". Kpq is well formed, because it is K followed by the atomic wffs p and q. NKpq is well formed, because it is N followed by Kpq, which is in turn a wff. KNpNq is K followed by Np and Nq; and Np is a wff, etc. See also Mathematical induction Recursive data types Recursion Structural induction Notes References Definition Mathematical logic Theoretical computer science Recursion