Whether an arbitrary statement in first order logic has a valid model is undecidable. But what if we constrain the domain of discourse to say, integers, or real numbers. I'm thinking of its implication in SMT solver. SMT solver attempts to validate (not prove) FOL theorems over fixed domains (usually integer or reals).



"First order logic" is a bit vague. The propositional calculus, and the one place predicate calculus with quantifiers, or even with identity added, are in fact decidable. The general predicate calculus (with many place predicates in addition to identity) is undecidable. But typically one is interested in a first order theory, not logic, something that introduces special predicates and axioms about them in addition to purely logical axioms. I am also not sure what "statement in first order logic has a valid model" means, on the usual terminology it is the entire theory that does or does not have a model, not individual statements. It probably just means that the statement is satisfiable.

Constraining the domain by first order means is impossible, as follows from Gödel's results, there is no way to rule out unintended models of a (sufficiently rich) theory by using first order axioms. Gödel's incompleteness means that one can always add some statements, as well as their negations, as axioms to such theories, and this will necessarily produce different models. For example, to make sure that only the "intended" integers are included one needs second order arithmetic. Needless to say, second order theories are even more undecidable than first order theories. Of course, the above does not apply if the domain of discourse is finite. Then there is no need for the second order logic to circumscribe it, we can simply list the elements, and there is an obvious decision procedure, just check the formulas on all combinations of them. But this would not work for integers or reals.

"Constraining the domain" sounds promising for simplifying things only on the platonic analogy between physical and mathematical objects. This analogy fails when the domain is infinite, we do not have platonic access to infinite domains. In real terms the "constraining" amounts to embedding the original first order theory into another theory. Even if this larger theory was still first order that would not help with decidability. But to make sure that the domain is "constrained" this larger theory can not even be first order, so this only makes things worse.


According to Wikipedia on Goedel's Incompleteness Theorem, "The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of the natural numbers."

The set of natural numbers is a proper subset of the set of integers (although they have the same cardinality) and also of the set of reals (which has larger cardinality). This means that there will be true statements that can't proven, so those are undecidable.

This has no effect on proof validation, since any proof that can be made can be validated. It does mean that not all true propositions can be proven in the first place.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.