\doc{Sample proof: axioms for finite sets}
\ref{sample-axioms}

The next several commands in \dflink{set1.lp}{set1.lp} axiomatize the
properties of finite sets of elements.

\begin{verbatim}
set name setAxioms
assert
  sort S generated by {}, insert;
  {e} = insert(e, {});
  ~(e \in {});
  e \in insert(e1, x) <=> e = e1 \/ e \in x;
  {} \subseteq x;
  insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y;
  e \in (x \union y) <=> e \in x \/ e \in y
  ..
set name extensionality
assert \A e (e \in x <=> e \in y) => x = y
\end{verbatim}

The \clink{set} command directs LP to assign the \dlink{../misc/name}{names}
\f{setAxioms.1}, \f{setAxioms.2}, ... to the axioms introduced by the 
subsequent \clink{assert} commands.  When multiple axioms are asserted in a
single command, they are separated by semicolons.
\p
The axioms are formulated using declared symbols (for sorts, variables, and
operators) together with \llink{connective}{logical symbols} for
\llink{equality}{equality} (\f{=}), negation (\f{~}), conjunction (\f{/\}),
disjunction (\f{\/}), implication (\f{=>}), logical equivalence (\f{<=>}), and
universal \llink{quantifier}{quantification} (\f{\A}).  LP also provides a
symbol for existential quantification (\f{\E}).  LP uses a limited amount of
\llink{precedence} when parsing formulas: for example, the logical operator
\f{<=>} binds less tightly than the other logical operators, which bind less
tightly than the equality operator, which bind less tightly than declared
operators like \f{\in} and \f{\union}.