1
$\begingroup$

A paper I'm reading asserts that "there is no sound and complete procedure for validity of first-order logic formulas of linear arithmetic with uninterpreted function symbols". By this we mean formulas like $f(x) + 1 > y$, where $+$ and $>$ are interpreted by Presburger arithmetic, and $f$ is uninterpreted. But how is this true? First-order logic is undecidable but complete. Presburger arithmetic is not finitely axiomatisable, but the axioms are recursively enumerable. Due to compactness of first-order logic, we can reduce the problem of finding a proof from the infinite axiom set to finding a proof from some finite subset of the axioms. And Godel's completeness theorem says we can always find a proof, if the formula is valid.

If this is true, then why would "first-order formulas of linear arithmetic with uninterpreted function symbols" (or any first-order formula, for that matter) not have a sound and complete procedure to check validity?

EDIT: The paper is: Ge, De Moura. "Complete instantiation for quantified formulas in Satisfiability Modulo Theories". http://leodemoura.github.io/files/citr09.pdf. The quote is in the first page.

$\endgroup$
4
  • $\begingroup$ I don’t think I understand. You say validity in first order logic is undecidable, but your final paragraph seems to suggest you doubt this. $\endgroup$ Commented Jul 11, 2019 at 15:19
  • $\begingroup$ It is undecidable, but semidecidable. If $A \models \phi$, then $A \vdash \phi$, else the algorithm may not terminate. My question is: if this holds in general, how come it doesn't hold for "first-order formulas of linear arithmetic with uninterpreted function symbols"? $\endgroup$ Commented Jul 11, 2019 at 16:11
  • 2
    $\begingroup$ You should cite the paper you're reading. This would provide more context and allow others to read what is actually written. To be clear, you should always cite texts that you quote from. $\endgroup$ Commented Jul 11, 2019 at 18:21
  • $\begingroup$ Updated with citation $\endgroup$ Commented Jul 11, 2019 at 21:26

1 Answer 1

Reset to default
1
$\begingroup$

This is a different meaning of the terms "sound" and "complete". When we say that a proof system is sound/complete with respect to a semantics, we mean that provability (in the proof system) implies/is implied by validity (in the semantics). This is not what's being discussed here.

Instead, when we have a decision procedure, here for validity of some formulas, we say it is "sound" if when it terminates, it terminates with the correct answer. It's "complete" if it always terminates. See slide 15 here.

The different meanings of these words are largely unconnected.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.