If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures!
Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions.
> Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed
No.
Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals.
If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand.
If I want to prove something arbitrary about real closed fields, I can press a button and go for a run.
Computers are much better at proving things about real closed fields than they are at proving things about integers!
> I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.
One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms.
This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)
If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures!
Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions.
> Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed
No.
Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals.
If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand.
If I want to prove something arbitrary about real closed fields, I can press a button and go for a run.
Computers are much better at proving things about real closed fields than they are at proving things about integers!
> I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.
One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms.
This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)