The Coq mailing list

[Cody Roux <cody.roux AT inria.fr>]

Dear Vladimir,


    I'm sure other users of this list can answer much more eloquently than I 
can, but it is useful to bear the following fact in mind when asking 
questions about decidability of fragments of arithmetic:

 (Kleene?:) It is possible, when given access to definitions of + and * on 
the natural numbers, to define a (unbounded-)quantifier-free formula

       Q(n, m, k)

Which is true if and only if the Turing machine with godel code n runs on 
input m for k steps without halting.

The satisfiability of this formula is undecidable. Therefore, whatever the 
situation with quantifiers and induction, if you can write something along 
the lines of the Q predicate, you are most likely dealing with an undecidable 
fragment of arithmetic.

Two common restrictions that make arithmetic decidable:

- No multiplication. Presburger showed that this calculus is decidable. 
However it is possible to form a predicate M(n,m,k) which expresses:

k = n * m if n, m <= K and K depends only on the size of the formula M. This 
allows us to form a restricted version of the Q predicate above and prove the 
beautiful result:

Any decision procedure for multiplication free arithmetic operates in time 
O(2^2^(c*k)) where c is a constant and k is the size of the formula you are 
trying to decide.

You see that even restricted multiplication poses problems to the 
decidability of a theory.

- Quantification over real numbers instead of natural numbers:

This one is really mind-bending (to me at least): surely the natural numbers 
is just a subset of the real numbers, so the theory of real arithmetic is 
strictly MORE expressive than that of natural numbers? Nevertheless, Tarski 
proved that there is a decision procedure which decides the truth of 
first-order sentences over real numbers with multiplication and addition (it 
breaks down if you add exp and log...).

This has the surprising consequence: there is no predicate which defines the 
natural numbers in real arithmetic, i.e. no formula NAT(x) such that
NAT(x) is true iff x is in N

Note that this is all false if you allow quantification over subsets of real 
numbers as well.

My (probably flawed) intuition is that real arithmetic is too "smooth" to 
define discrete mechanical things like Turing machines. More concretely, 
finding zeros of polynomials P(x,y,z,...) in natural numbers can be quite 
hard even in one variable: P(x), where there is no method much better than 
testing a bunch of candidate solutions, whereas in the reals you can use 
Sturm sequences along with the simple fact that a polynomial which changes 
signs on an interval [a,b] has a zero in that interval. Things are harder 
with arithmetic. Note that it is undecidable in general whether a polynomial 
in several variables has a solution in the natural numbers.


Hope this helps,


Cody



----- Mail original -----
> De: "Vladimir Voevodsky" 
> <vladimir AT ias.edu>
> À: 
> types-list AT lists.seas.upenn.edu,
>  "Coq Club" 
> <coq-club AT inria.fr>
> Cc: "Vladimir Voevodsky" 
> <vladimir AT ias.edu>
> Envoyé: Jeudi 19 Juillet 2012 17:16:38
> Objet: [Coq-Club] Re: question (cont.)
> 
> 
> > Don't you have False (as 0=1 for instance) hence not A (as
> > A ->False) hence exA (as forall notA -> False), hence everything?
> 
> Thanks to everybody who pointed this out to me. I'll have to think
> whether my question has a more sensible reformulation.
> 
> Vladimir.
> 
> 
>