Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: question (cont.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: question (cont.)


Chronological Thread 
  • From: Cody Roux <cody.roux AT inria.fr>
  • To: Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Re: question (cont.)
  • Date: Fri, 20 Jul 2012 11:30:00 +0200 (CEST)


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.
>



Archive powered by MHonArc 2.6.18.

Top of Page