Conservative definition category of theory statements

[wwitzel]

We can add a third category of statements to our theory packages: conservative definitions in addition to axioms and theorems. Many of our axioms could move over to the “conservative definitions” category. Like axioms, the statements themselves will not be proven – they are asserted definitions. Like theorems, they would require a proof. The statement would not be proven. Rather, you need to prove the unique existence of defined objects. For “simple” conservative definitions (e.g., of the form forall_{x, y, z} L(x, y z) = …), the proof will be trivial and can be implemented automatically. For things like our “x U y” example, it would require some more work. This offers advantages of clarity, flexibility, and a reduction in the axioms that need to be inspected.

[wwitzel]

Here are some specific examples of definitions and required existence proofs.

In the latter example, in order to define union uniquely, we must indicate that it belongs to a class of (unordered) "sets" that are equal whenever they are set-equivalent:

That takes care of uniqueness. For existence, we'd need one of the ZF axioms. Specifically, (Do we need further restrictions to the class of sets? I don't think so, but I'm not sure). Would this [be] better than having our union definition as an axiom the way it is now? I don't know, but it would be more standard.

Here is a more general conservative definition for union: