LP, the Larch Prover -- Sample proofs: useful kinds of axioms


The axioms in set1.lp fall into several categories:

Induction rules
The first axiom, sort Set generated by {}, insert, asserts that all elements of sort S can be obtained by finitely many applications of insert to {}. It provides the basis for definitions and proofs by induction.

Explicit definitions
The second axiom, {e} = insert(e, {}), is a single formula that defines the operator {__} (as a constructor for a singleton set).

Inductive definitions
The next two pairs of axioms provide induction definitions of the membership operator \in and the subset operator \subseteq. Inductive definitions generally consist of one formula per generator.

Implicit definitions
The final formula, e \in (x \union y) <=> e \in x \/ e \in y, in the first assert command, together with the other axioms, completely constrains the interpretation of the \union operator.

Constraining properties
The second assert command formalizes the principle of extensionality, which asserts that any two sets with exactly the same elements must be the same set.