[FOM] Primitive symbols in the theory of real closed fields
Andre Platzer
aplatzer at cs.cmu.edu
Wed Apr 28 19:20:33 EDT 2010
There is a discussion of addition and multiplication with restricted forms of distributivity in the following article that could help
Avigad, J. & Friedman, H.
Combining decision procedures for the reals.
Logical Methods in Computer Science, 2006, 2
Andre
On Apr 28, 2010, at 6:56 PM, Rafael Grimson wrote:
> Adding the binary relation symbol "<" to the vocabulary <+, x, 0, 1>
> Tarski [Tar51] obtained a theory, R, for real closed fields that
> admits quantifier elimination (and the symbol < is insdispensable to
> obtain this).
>
> In his article [Tar31] Tarksi also shows that the product symbol, x,
> is indispensable, i.e., the set of formulas that do not involve this
> symbol has less expressivle power than the complete language.
>
> Does someone know if it is proven that the addition symbol is also
> indispensable?
>
> Best egards,
> Rafael Grimson
>
>
>
> [Tar31] A. Tarski, Sur les ensembles denissables de nombres reels, Fundamenta
> Mathematicae 17 (1931), 210-239.
> [Tar51] , A decision method for elementary algebra and geometry, second
> ed., Univ. of California Press, Berkley, CA, 1951.
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
More information about the FOM
mailing list