[Prev][Next][Index]

Re: Specifying the Reals in LSL?

leavens@cs.iastate.edu (Gary Leavens) wrote:
>Is it possible to specify the Real numbers in LSL?

     As W. O. D. Griffioen notes, the syntax errors in Gary's trait can be
eliminated by using \A for the universal quantifier and \E for the existential
quantifier.  An additiona semantic error can be removed by restricting m and n
to be greater than n0.

     Even with these changes, it is unlikely that this approach to specifying
the reals will be very useful in practice.  Defining the reals in terms of
Cauchy sequences is akin to implementing an abstract data type.  The definition
"works" because Cauchy sequences satisfy the properties we expect of the reals,
but we want to use those properties (and not an exposed representation) when
reasoning about the reals.

     What are those properties?  I suspect that for most applications, it's
enough to axiomatize the reals as an ordered field, that is, as a field with an
ordering relation that satisfies the axioms
    x < y => (x + z) < (y + z)
    0 < x /\ 0 < y => 0 < (x * y)
Of course, these axioms do not distinguish the reals from the rationals.  If
you want to do that, you could add an axiom
     0 < x => \E y (x = y * y)
to ensure that every positive real has a square root, as well as axioms that
ensure that every polynomial of odd degree has a root.  (A polynomial trait
would come in handy here.)  

     Now you've got the axioms for what is known as a real closed field, and
you are almost home, because Tarski showed that the first-order theory of the
reals is equivalent to the theory of real closed fields of characteristic zero.
Thus you can finish the axiomatization by adding axioms that define an
injection of the naturals numbers into R.

     In classical first-order logic, there is no finite axiomatization of the
theory of the reals: it takes infinitely many axioms to express the fact that a
field has characteristic zero, and it takes infinitely many to express the fact
that every polynomial of odd degree has a root.  However, because the
generated-by construct in LSL is equivalent to an infinite set of formulas, it
is possible to provide a finite axiomatization in LSL, as described above.
Follow-Up(s):