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.