Skip to main content
MathOverflow

Return to Question

Became Hot Network Question
added 4 characters in body
Source Link
Sidharth Ghoshal
Sidharth Ghoshal
  • 2.7k
  • 19
  • 32

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See here

Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).

Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).

So I was curious, do we know ANY other relations which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.

I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.

But that is just wishful thinking for now ^ 

I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See here

Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).

Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).

So I was curious, do we know ANY other relations which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.

I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.

But that is just wishful thinking for now ^ I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See here

Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).

Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).

So I was curious, do we know ANY other relations which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.

I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.

But that is just wishful thinking for now ^ 

I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.

Source Link
Sidharth Ghoshal
Sidharth Ghoshal
  • 2.7k
  • 19
  • 32

What theories are larger than the real closed field but still decidable?

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See here

Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).

Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).

So I was curious, do we know ANY other relations which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.

I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.

But that is just wishful thinking for now ^ I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.