Defining

In Problem Set 2 we were shown how to inductively define sets. Starting with a universe, , we can construct a set of rules: Recall also that a set is -closed if , the set inductively defined by can then be defined as the least -closed set.

Example. Given sets and , let and define,

We can now define to be the infinite set of rules:

Discussion. There are two things to note about this definition. Firstly, we have tagged each variable and constant with the words var and const respectively. This enables us to tell the rule with which each formula was generated, and also to differentiate between variables (or constants) which we would like to treat as such, and those which we would like to consider as propositions. The construction of a set through rules is deterministic if each element can be built from a unique set of rules. The construction of is deterministic. It is also useful to preserve determinism in defining datatypes such as A list. There, we would like to differentiate between elements of A, and elements of A list of length 1. That is, we should have rules of the form and NOT of the form to represent lists of length one. We will want to have this property of determinism in defining recursive types as well.

Secondly, note that we needed to use an infinite number of rules in order to generate . This requirement stems from that fact that each element to be derived must have have its' own rule. Moreover, we cannot a priori be sure of which antecedents will be generated by the rules. This means that we must include rules that ``intuitively'' we know will never be used to generate anything. Since ML (not surprisingly) does not allow infinitely long definitions, we will need an alternative way to convey the least, closed characteristics of .