[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 denissables 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