The Coq mailing list

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

Hello,

     Thank you for these explanations, I may have been to hasty in declaring 
the quantifier-free fragment (without negation) undecidable.



> in the fragment of formulae of the form:
> \forall x_1 ... x_n, P<>Q
> truth is undecidable.  (Yes, I'm cheating.  But
> this shows that you should also be careful in
> defining the primitive predicates you allow
> in your fragment.)

> As for formulae of the form
> \forall x_1 ... x_n, P=Q
> [...]
> I claim that their truth is decidable, and that
> Vladimir's questions can be answered positively.

This is well-known: in any integral domain of infinite cardinality, 
equality of polynomial -functions- is equivalent to formal 
equality of the formulas. Your proof is quite nice though (as usual :).

I suspect Vladimir was hoping for a more general statement than that
though.



All the best,


Cody


> 
> To simplify things, I will reason with equations
> of the form P=0, allowing the coefficients of
> P to be positive or negative.  (But x1, ..., xn
> will still be natural numbers --- not that it
> makes any difference in the end.)
> 
> Given values v1, ..., v{n-1}
> for x1, ..., x{n-1}, let R[xn] be the polynomial
> (in one variable, xn) obtained from P by replacing
> x1 by v1, ..., x{n-1} by v{n-1}.
> 
> By Lagrange interpolation, the equation R[xn]=0 holds
> for every xn in |N if and only if
> R[0]=0 and R[1]=0 and ... and R[d]=0,
> where d is any upper bound on the degree of R[xn].
> (=> is obvious; <= implies that the polynomials,
> not just the polynomial functions, are identical.)
> 
> Now the conjunction R[0]=0 and R[1]=0 and ... and R[d]=0
> is equivalent to R[0]^2 + R[1]^2 + ... + R[d]^2 = 0.
> 
> Now, since this holds for all values v1, ..., v{n-1},
> we have actually shown that
> (1)   \forall x1 ... xn, P=0
> is equivalent (truth-wise) to
> (2)   \forall x1 ... x{n-1},
>       P[xn:=0]^2 + P[xn:=1]^2 + ... P[xn:=d]^2 = 0
> where we take d = the degree of xn in P (this is then
> an upper bound on the degree of R[xn] whatever the values
> v1, ..., v{n-1}), and I hope the notation P[xn:=v] is
> self-explanatory.
> 
> Now (2) has the same form as (1), only with one variable
> less.  So we induct, eventually reducing the question (1)
> to the case where n=0.
> Then P is a polynomial with no variable, which one easily
> decides (by computation) whether it is identically 0 or not.
> 
> This shows that the truth of statements of the form (1)
> is decidable.
> 
> Now it follows that Vladimir's intended question (hopefully)
> can be answered in the positive:
> 
> Thm: The truth of the formulae of arithmetic built on 0, 1, +, x,
> =, and, or, \forall, is decidable.
> 
> Proof.  First move all quantifiers in front.
>    So we are led to decide formulae of the form
> (3)   \forall x1 ... xn, G
>       where G is quantifier-free (and negation-free).
> 
>    We convert G inductively to a formula of the form P=0
>    where P is a polynomial with integer coefficients:
>    - atomic formulae are of the form P=Q, where P and Q
>      are polynomials with natural number coefficients, and
>      can be read off as P-Q=0
>    - conjunctions P1=0 and ... and Pk=0 are converted
>      to P1^2+...+Pk^2=0, as before
>    - disjunctions P1=0 or ... or Pk=0 are converted to
>      P1 x ... x Pk = 0.
>    In the end, we obtain a formula of the form (1), which
>    we have seen how to decide.
> Qed.
> 
> Note that, since truth is decidable, there is a deduction
> system that is sound and complete for this fragment (i.e.,
> truth and provability coincide), and which is axiomatisable
> (i.e., its axioms and rules form a recursively enumerable
> set).  This is trivial: there is no rule, just one axiom
> per true sentence.
> The question whether any particular deduction system is
> sound and complete for this fragment is another, different
> matter.
> 
> This is so simple I'm pretty sure this must have been
> known for ages, but I don't know of any reference off
> the top of my head.
> 
> Finally, since we are on the Coq mailing list, I must say
> that the only non-intuitionistic part that is left in my
> arguments, as far as I can tell, is that you cannot permute
> \forall quantifiers in front of disjunctions (first line
> of proof of Thm).
> 
> -- Jean.
>