I've just become aware of some results that updates Tarski's decision procedure for real closed fields. If you add the (real) exponential function to the theory of real closed fields, the theory is probably decidable, but there remain gaps (how come this problem didn't make it onto the Millenium list?). This means in practise that you would be able to reason about _hyperbolic functions_ (sinh, cosh) in a decidable way. Reasoning about _circular functions_ (sin, cos) seems to allow the reasoning about the integers, due to their periodic nature, and thereby enter the undecidable domain. Thus, hyperbolic functions are _easier_ than circular functions. http://en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem http://www.oocities.org/tamara_servi/thesis.html "Undecidable and Decidable Problems in Mathematics - Professor Angus MacIntyre" lecture video http://blip.tv/greshamcollege/undecidableanddecidableproblemsinmathematics_a... At 07:51 PM 10/21/2011, Henry Baker wrote:
The theory of "real numbers" (or at least the theory of algebraic numbers) is easier than the theory of "integers".
The theory of real order is decidable. The theory of real addition & ordering is decidable. The theory of real closed fields (+,*,<; i.e., polynomials with integral coefficients) is decidable. The theory of integers with a single successor function ("1+") is decidable, but harder than that of real closed fields. This is like the integers, but you can only emulate addition/subtraction of constants, and cannot emulate multiplication of 2 arbitrary integers.
The theory of integers (with addition & multiplication) is undecidable.
So, in order to define the integers within the real numbers, you need to add enough additional structure to emulate finite chains (i.e., induction). Most of the emulations I've seen involve things like complex numbers, sines & cosines, so you emulate the integral periodic structure of sines/cosines.
At 06:13 PM 10/21/2011, David Wilson wrote:
How do you show that there is an integer greater than any given real number?
The real question is, given the axioms for the real numbers (Dedekind-complete ordered field), how do you define the "real integers" within them.
Two possibilities spring to mind.
Definition A: The "real integers" are the minimal subset of R that contains 1 and is closed over negation and addition.
Definition B: 1 is a "real integer", and there is a unique "real integer" in every half-open unit interval of R.
Definition A seems more in the spirit of the number theory definition of Z. However, I do not immediately see how it answers my original question.
Definition B immediately answers my original question. For any real number r, there is a unique integer on the half-open interval (r, r+1] which must be greater than r.
Presumably definitions A and B are equivalent. Is the proof easy?