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).
 A: 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. 
A: *

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

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