5 ms·
Do people talk about "inductive definitions"? I mostly only hear about induction in the context of proofs, in which case I'd say that an inductive proof/argumen
by alecbz 4y ago
Do people talk about "inductive definitions"? I mostly only hear about induction in the context of proofs, in which case I'd say that an inductive proof/argument is one that uses the recursive structure of whatever it's about.
A recursive definition is: "natural numbers are 0 or a natural number + 1". An (abridged) inductive proof that uses the recursive nature of natural numbers: "the sum of all naturals up to n is n(n+1)/2: 0*(0+1)/2 = 0, and (n+1) + n(n+1)/2 = (2(n+1) + n(n+1))/2 = (2n + 2 + n^2 + n)/2 = (n^2 + 3n + 2)/2 = (n+1)(n+2)/2 = (n+1)((n+1)+1)/2"
- cheese_it 4y agoBut how do you know that induction is valid to use on natural numbers? It's because their definition/construction follows a set of rules that makes them inductive. Some languages like Coq make this explicit by providing an 'Inductive' keyword for defining inductive types.
- jlokier 4y ago> A recursive definition is: "natural numbers are 0 or a natural number + 1". Note that this isn't enough by itself to support proof by induction. Consider the definition of a list in Haskell which is analogous to the above definition of natural numbers: "lists are [] or a list with an element prepended". Infinite lists satisfy this definition.