1
$\begingroup$

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

2 Answers 2

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

  • 1
    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.2012-08-29
  • 0
    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.2012-08-29
  • 0
    @CarlMummert: True. Thing is, I wanted to give an answer that requires less background.2012-08-29
  • 0
    @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.2012-08-29
  • 0
    Isn't the only thing that's different between a structure and a model that a model satisfies the axioms?2012-08-29
  • 0
    Yes. This is exactly the definition of a model.2012-08-30
4

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.

  • 0
    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.2012-08-29
  • 0
    @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).2012-08-29
  • 0
    @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?2012-08-29
  • 1
    @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.)2012-08-29
  • 1
    (... 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.2012-08-29
  • 0
    A different (and more formalist) approach would be to claim that writing $(\mathbb N,0,1,{+},{\cdot})$ doesn't actually define a structure uniquely, because the meaning of doing so depends on the essential incompleteness of the axioms that underlie the _metalevel_ we're using to speak about the structure.2012-08-29
  • 0
    @HenningMakholm: Okay, thank you!! Let's say I call a formula M-true if its structure M determines it's true, I call it P-true if it has a proof or if it's valuation is computable or both (so P-true => M-true), and X-true if it is not P-true (but maybe M-true). Now tell me if I get the following right: By my definition, provability of a formula means that it is P-true. So completeness and soundness imply: logically valid <=> P-true. The Gödel sentence and its negation are not provable, so they are not logically valid. Moreover, they are both X-true and one is M-true and the other one is not.2012-08-29
  • 0
    @Nick: I'm not quite sure what you mean by "or if it(')s valuation is computable". Any _particular_ formula will evaluate to either true or false, so that is certainly computable (though we may not know _which_ program computes its valuation). In any case, suppose there's a formula that is _not_ provable, but satisfies "its valuation is computable". Because it is not provable (and I assume a standard FOL proof system), it is not logically valid either, because every logically valid formula is provable. So your $\Leftrightarrow$ cannot be right, unless "its valuation is computable" is vacuous.2012-08-29
  • 0
    @HenningMakholm: Does "uncomputable function" here mean that the given function doesn't evaluate if I give it some input, or does it mean that I can't find out what the function is (I used it here in the second interpretation)? --- You say "Any particular formula will evaluate to either true or false, so that is certainly computable (though we may not know which program computes its valuation)." while Carl Mummert, in the other answers comment says "Even if the structure is effective (and thus has no uncomputable predicates), the valuation function is still likely to be uncomputable."2012-08-29
  • 0
    @Nick: The difference is that Carl is speaking about he function _from all formulas_ to truth values. This is either computable or not. I'm speaking about the situation where you have already chosen _one particular_ formula you want a valuation for. Then there is certainly a computable function that answers correctly for _that_ particular formula (but possibly goes wrong for many others). In general it is only really meaningful to ask whether a function is computable _as a function_, not whether it is computable _for a specific input_.2012-08-29
  • 0
    let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/4670/discussion-between-nick-kidman-and-henning-makholm)2012-08-29
  • 0
    Thanks, @CarlMummert. Helped me quite a bit, I just accepted the other answer for accessability reasons.2012-08-29