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