LP, the Larch Prover -- Sample proof: axioms for finite sets

The next several commands in set1.lp axiomatize the properties of finite sets of elements.

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

The set command directs LP to assign the names setAxioms.1, setAxioms.2, ... to the axioms introduced by the subsequent assert commands. When multiple axioms are asserted in a single command, they are separated by semicolons.

The axioms are formulated using declared symbols (for sorts, variables, and operators) together with logical symbols for equality (=), negation (~), conjunction (/\), disjunction (\/), implication (=>), logical equivalence (<=>), and universal quantification (\A). LP also provides a symbol for existential quantification (\E). LP uses a limited amount of \llink{precedence} when parsing formulas: for example, the logical operator <=> binds less tightly than the other logical operators, which bind less tightly than the equality operator, which bind less tightly than declared operators like \in and \union.