[opentheory-users] numerals

[rda at lemma-one.com]

> The OpenTheory inference system shows a clear bias in favour of HOL Light.
> This is manifest in the amount of extra work developers of other systems
> would
> need to do to write article readers and writers compared to of HOL Light.
> But
> I think that is OK because the HOL Light inference system is clean and
> minimal-looking.
>
> However, the bias evident in the standard library numerals is not so
> great.
> Norrish numerals (bit1 and bit2) are "clearly superior" to binary (bit0
> and
> bit1) because the representations are unique. There are other options too,
> such
> as lists of decimal digits. Possibly the standard library doesn't need
> numerals
> at all (i.e. use unary numerals with suc and zero), if we don't anticipate
> very
> large natural number constants actually appearing in theorems.

I don't think that unary numerals would be a very prudent decision.

>
> My main purpose in writing is to start a discussion, because I'm not
> particularly aware of the issues and trade-offs regarding numerals but I
> see
> there might be a possibility for improved design. I also don't know the
> extent
> of the effects of making the right choice for the standard library. Maybe
> it is
> too small to be worth the effort?

I think it is safe to assume that systems that implement article readers
will come equipped with decision procedures for formulas made from numeric
literals using the usual arithmetic operations and predicates. So one
option would be to omit the proofs of any theorem whose conclusion is a
true instance of such a formula and mark such a theorem when it appears as
antecedents to an inference rule (so that the reader knows to apply the
decision procedure).

This makes the representation of numeric literals not very important,
although I would have a preference for strings of decimal digits as being
more comprehensible to someone trying to debug an article reader or
writer.

If we could agree what constitues a rational or real literal then a
similar approach might be beneficial for them. The same idea would also
allow a writer to omit proofs of propositional tautologies.

Regards,

Rob.