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