freely generated inductive set
More generally, fix a non-empty set and a set of finitary operations on . A set is said to be inductive (with respect to ) if is closed under each . This means, for example, if is a binary operation on and if , then . is said to be inductive over if . The intersection of inductive sets is clearly inductive. Given a set , the intersection of all inductive sets over is said to be the inductive closure of . The inductive closure of is written . We also say that generates .
Another way of defining is as follows: start with
Next, we “inductively” define each from , so that
Finally, we set
It is not hard to see that .
By definition, . Suppose is -ary, and , then each . Take the maximum of the integers , then for each . Therefore . This shows that is inductive over , so , since is minimal. On the other hand, suppose . We prove by induction that . If , this is clear. Suppose now that , and . If , then we are done. Suppose now . Then there is some -ary operation , such that , where each . So by hypothesis. Since is inductive, , and hence as well. This shows that , and consequently . ∎
The inductive set is said to be freely generated by (with respect to ), if the following conditions are satisfied:
for each -ary , ;
if are -ary, then .
For example, the set of well-formed formulas (wffs) in the classical proposition logic is inductive over the set of propositional variables with respect to the logical connectives (say, and ) provided. In fact, by unique readability of wffs, is freely generated over . We may readily interpret the above “freeness” conditions as follows:
is generated by ,
for distinct wffs , the wffs and are distinct; for distinct pairs and of wffs, and are distinct also
for no wffs are and propositional variables
for wffs , the wffs and are never the same
A characterization of free generation is the following:
- 1 H. Enderton: A Mathematical Introduction to Logic, Academic Press, San Diego (1972).
|Title||freely generated inductive set|
|Date of creation||2013-03-22 18:51:24|
|Last modified on||2013-03-22 18:51:24|
|Last modified by||CWoo (3771)|