Is a valuation of a logic formula always a trivial task? I.e. is it practically executable?

For a given structure for a quantified theory, is the valuation of any formula always practically executable?

In the case of propositional calculus, where every formula has a certain degree, this is the case as there you can simply climb down to atomic propositions (for which the truth values are determined by the structure/assignment) to validate the whole expression. I don't know if this is also as easy for predicate logic though. It's known that there isn't always a proof, but does this relate to the valuation?

Argument against it: If it's true that for a given structure you can automatically evaluate any given formula (or at least sentence with no free variable), then I don't see why finding a proof (e.g. writing down the sequence constructed in say a Hilbert style system) - or rather the possibility not to be able to find one - would be such a big of a deal. To do the valuation means confirm the truth or falsity, which just seems like a proof in a way. Is executing a validation equivalent to finding a proof? On the other hand.

On the other hand, I don't know where the problem with the evaluation would kick in (maybe related to there being more possible variables for a formula).

-

1. Trying out a valuation is much easier than finding a proof. In the propositional case, for example, you can check the validity of a given evaluation in time linear to the formula size. On the other hand, checking whether a formula has a satisfying valuation is NP-complete, and hence, finding a proof in any proof system will be NP-hard.

2. In predicate calculus, you can have, e.g., structures with uncomputable predicates, so checking whether a structure satisfies a formula is undecidable in general. In fact, finding decision procedures for given first-order theories and sub-logics of first-order logic is an active field of research.

-
Even if the structure is effective (and thus has no uncomputable predicates), the valuation function is still likely to be uncomputable. The normal procedure,of course, is to assume the structure is effective and look for the Turing degrees that compute a valuation. Then the general result is obtained by just relativizing to the Turing degree of an arbitrary structure. – Carl Mummert Aug 29 '12 at 11:48
Okay so if I understand you correctly: To (1), if the set of propositions has $n$ elements, there are "only" $2^n$ validations, right? So after you tried these you know if it's satisfiable. And (2), this means the structure (or model) doesn't fix the semantics of a theory after all. – NikolajK Aug 29 '12 at 12:01
@CarlMummert: True. Thing is, I wanted to give an answer that requires less background. – Johannes Kloos Aug 29 '12 at 18:42
@NickKidman: The fact that you "only" need to test $2^n$ valuations (actually, less than that, but this is leading too far) should clue you in that finding a model is already much harder than checking whether a valuation is a model. Regarding your remark on (2), I'm not quite sure what you mean. A structure will, of course, give a fixed meaning to all elements of a formula, but there is no algorithm that, given an arbitrary structure, will check whether that structure is a model. This is only possible for certain types of structures, and often only partially. – Johannes Kloos Aug 29 '12 at 18:46
Isn't the only thing that's different between a structure and a model that a model satisfies the axioms? – NikolajK Aug 29 '12 at 19:44

No, in general there is no effective way to determine whether a formula is true or false in an effective first-order structure. A key example is $\mathbb{N}$; in that context Post's theorem shows exactly what Turing degrees are needed to evaluate the truth or falsity of arithmetical formulas with quantifiers. It turns out that the nesting of the quantifiers is the key factor in making the decision problem difficult. The canonical oracle that can compute the valuation function for an effective structure is the $\omega$th Turing jump of the empty set, $\emptyset^{(\omega)}$.

The question whether a formula is provable in an effective logical system is also undecidable in general, but it is just a $\Sigma^0_1$ question regardless of the complexity of the formula, and so this problem can always be solved by using a $\emptyset'$ oracle, unlike the problem of computing a valuation which requires stronger oracles.

-
Okay thank you. The terminology is beyond me, but I'll look into computable functions. How do the validation and the deduction system relate though: Does having a proof for a formulate at hand imply that I can valuate that formula? I guess the answer might be "yes, if the deduction system is sound", but I'm not sure if the notion of truths in the definition of soundness coincides with the one determined by a validation. – NikolajK Aug 29 '12 at 12:07
@NickKidman: Yes, having a proof for a formula implies that you can easily determine its truth value, because it will necessarily be "true" in any interpretation (which satisfies the axioms) (if the formal system is sound). – Henning Makholm Aug 29 '12 at 12:12
@HenningMakholm: Okay so soundness and there being a proof implies that you can validate a formula. Putting 1 and 1 together, this means the fact that "having a structure doesn't always mean you can check the truth of a formula" was only known after it was figured out that there are theoems without proof? If incompleteness was a surprise to people, this means they thought a structure would always fully determine the semantics, right? – NikolajK Aug 29 '12 at 12:33
@Nick: We need to tread a little carefully here. A structure always does determine a semantics, in the sense that we can prove that for every structure $\mathfrak A$, there is exactly one function from wffs to $\{\mathrm{true},\mathrm{false}\}$ that agrees with $\mathfrak A$ in such-and-such way. However, showing that this function exists (and is unique) is not the same as being able to determine one of its values concretely. How to think about that is something of a philosophical question, but one possible viewpoint is that we simply don't understand the structure well enough. (contd.) – Henning Makholm Aug 29 '12 at 12:45
(... contd.) For example, consider the structure $(\mathbb N,0,1,{+},\cdot)$. We know exactly how each element of $\mathbb N$ looks and how to find the truth value of any atomic formula, so in some sense we explicitly known "everything" about the structure. on the other hand, this still hasn't enabled us to devise any way to determine the truth value of the formula that states "there is an upper bound for all twin primes". So in that sense we don't know everything after all. – Henning Makholm Aug 29 '12 at 12:48