Re: Specifying the Reals in LSL?

Subject: Re: Specifying the Reals in LSL?
From: leavens@cs.iastate.edu (Gary Leavens)
Date: 29 Aug 95 22:44:54 GMT
Newsgroups: comp.specification.larch
Organization: Iowa State University, Ames, Iowa
References: <leavens.809667621@bambam.cs.iastate.edu> <41vci8$rc5@GRAPEVINE.LCS.MIT.EDU>

"Stephen J. Garland" <garland> writes:

>     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.

Thanks for all that and your answers.

I'm sorry our posts crossed, but I do think that the syntax would be
less confusing if you didn't require quantified variables to be
declared outside the scope of the equation in which they appear
in LSL.

	Thanks,

	Gary
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html

Reference(s):

Re: Specifying the Reals in LSL?

From: "Stephen J. Garland" <garland>

Prev: how to get LP to prove things like ~(1 <= 0) and (0 <= 2)?
Next: Re: Specifying the Reals in LSL?
Index: Larch archive index