To define the natural numbers, we extend the language with one contant symbol 0 and one unary function symbol S x. Then the natural numbers are defined by the following predicate I N x
N0.total.N added as introduction rule (abbrev: N0
, options: -i -c
)
S.total.N added as introduction rule (abbrev: S
, options: -i -c
)
case_left.N added as elimination rule (abbrev: case
, options: -n
)
rec.N added as elimination rule (abbrev: rec
, options: )
The introduction rules are added with the command new_intro -c
.
The option -c
indicates that 0 and S are
constructors and the trivial tactic will try to use these rules when
the goal is of the form P 0 or P (S t) even if P is a
unification variable.
The elimination rules are added with the command new_elim
using the option -n
for case.N. This tells PhoX that this
second rule is not necessary for completeness.
The abbreviations are given with the rules. For instance, elim case.N with H
is equivalent to elim H with [case]
and elim N0.total.N
is equivalent to intro N0
.
We add usual axioms of Peano Arithmetic.
We also prove the following left rules for natural numbers (the first one is an axiom ).
./nat.tex ./nat_ax.tex
Products Christophe Raffalli, Paul RoziereEquipe de Logique, Université Chambéry, Paris VII