The Coq mailing list

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

Le 20/07/12 10:57, Jean Goubault-Larrecq a écrit :
> [...]
> 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.
>
> [...]
> Thm: The truth of the formulae of arithmetic built on 0, 1, +, x,
> =, and, or, \forall, is decidable.

I should probably also add that the truth of the
formulae built on the same language plus any of <=, >=,
<, >, or <> reverts again to undecidable.
This is because one can encode <>, e.g.,
P <> Q is equivalent to P+1<=Q or Q+1<=P.
So having just equality as predicate is important.

-- Jean.