The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Le 20/07/12 08:00, Arnaud Spiwack a écrit :
> Dear Vladimir,
>
> A gizmo logicians use to spek of this sort of things is the arithmetical
> hierarchy (see for instance:
> http://en.wikipedia.org/wiki/Arithmetical_hierarchy#The_arithmetical_hierarchy_of_formulas
> ).
>
> A formula with just universal quantifiers followed by a non-quantified
> formula is said to be Π₁. So here is a possible reformulation: is the Π₁
> fragment of arithmetic decidable? (the answer is, unfortunately, that it
> isn't, as Cody explained)

Hi,

not exactly: the Pi_1 fragment allows for negations
inside the non-quantified formula, which we are trying
to forbid.
Similarly, Cody's first answer (encoding the Kleene
predicate) requires negation.  So I'm afraid none
of these answers deals with the question that Vladimir
had in mind.

Also, in answering these questions, one should
pay attention to whether we want to decide truth
or provability.

It is well-known that in the fragment of formulae of
the form:
\exists x_1 ... x_n, P=Q
where P and Q are expressions built with 0, 1, +, x
(i.e., polynomials with natural numbers as coefficients),
truth is undecidable.
This is Matiyasevitch's Theorem (ca. 1970),
solving Hilbert's 10th problem in the negative.

It follows that if you forbid negations but still
allow <> (negation of =) as primitive predicate,
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
the situation is very different.
I claim that their truth is decidable, and that
Vladimir's questions can be answered positively.
(Please let me know if I've made any mistake.)

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.