by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic & Semantics, Entry Directory]
[David Agler, entry directory]
[Agler’s Symbolic Logic, entry directory]
[The following is summary. Boldface (except for metavariables) and bracketed commentary are my own. Please forgive my typos, as proofreading is incomplete. I highly recommend Agler’s excellent book. It is one of the best introductions to logic I have come across.]
Summary of
David W. Agler
Symbolic Logic: Syntax, Semantics, and Proof
Ch.7: Predicate Logic Trees
7.4 Undecidability and the Limits of the Predicate Tree Method
Brief summary:
When we deal with the problem of universal instantiation causing us to repeat over and over a combination of existential and universal decomposition rules, we can instead apply the following new existential decomposition rule.
(Agler 318)
Summary
[In the language of propositional logic (PL), we can determine logical properties with truth trees using a finite number of steps. This means that we say it is decidable. However, in the language of predicate logic (RL), we cannot always do that, and for this reason we say that it is undecidable.]
Unlike PL, RL is undecidable. That is, there is no mechanical procedure that can always, in a finite number of steps, deliver a yes or no answer to questions about | whether a given proposition, set of propositions, or argument has a property like consistency, tautology, validity, and the like. For some trees, the application of predicate decomposition rules will result in a process of decomposition that does not, in a finite number of steps, yield a closed tree or a completed open branch.
(Agler 317-318)
1 | (∀x)(∃y)(Pxy) | P |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay | 1∀D |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ | 1∀D |
3 | Pab | 2∃D |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ | 1∀D |
3 | Pab | 2∃D |
4 | (∃y)Pby | 1∀D |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ | 1∀D |
3 | Pab | 2∃D |
4 | (∃y)Pby✔ | 1∀D |
5 | Pbc | 4∃D |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ | 1∀D |
3 | Pab | 2∃D |
4 | (∃y)Pby✔ | 1∀D |
5 | Pbc | 4∃D |
6 | (∃y)Pcy✔ | 1∀D |
7 | Pcd | 6∃D |
. | ||
. | ||
. |
(Agler 318, with checkmark added – perhaps mistakenly – to line 6)
Notice that in the above tree, the decomposition procedure will continue indefinitely since every time an (∃D) is used, another use of (∀D) will be required, followed by another (∃D), followed by another (∀D), and so on. This indefinite process of decomposition thus does not yield a completed open branch and so the truth-tree method does not show that ‘(∀x)(∃y)(Pxy)’ is consistent.
(Agler 318)
Agler explains how this rule works:
A use of (N∃D) requires that whenever we decompose an existentially quantified proposition ‘(∃x)P,’ we create a separate branch for any substitution instance for any substitution instance P(a1/x), P(a2/x), ..., P(an/x), already occurring in the branch containing ‘(∃x)P’ and branch a substitution instance ‘P(an+1/x)’ that is not occurring in that branch.
(Agler 318)
We will now redo the tree above, which previously did not produce for us a completed open branch.
1 | (∀x)(∃y)(Pxy) | P |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay | 1∀D |
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ / \ | 1∀D |
3 | Paa Pab | 2N∃D |
4 | O |
|
1 | (∀x)(∃y)(Pxy) | P |
2 | (∃y)Pay✔ / \ | 1∀D |
3 | Paa Pab | 2N∃D |
4 | O (∃y)Pby / | \ | 1∀D |
5 | Pba Pbb Pbc O O . . . | 4N∃D |
[I might be getting the idea here wrong, so I will quote what Agler says afterward. As far as I understand, if the model is finite, that means if we keep reiterating N∃D, and eventually the process will terminate, as we will run out of constants. I am not sure if that means we really do need to run through them all in the tree or if we can take the pattern of redudancy to inductively show that in the end the final one will be open or closed. Probably we need to run through them all I suppose. But the idea also seems to be that if the model is infinite, not even this revised decomposition rule will determine a completed open or a closed branch. Agler then notes that this issue of undecidability is not a prevalent problem in RL, so we need not attend to much to it at this introductory level. As I missed the point, I will need to quote for your interpretation.]
While another round of (∀D) and (N∃D) yields additional completed open branches, which will allow for the construction of finite models, the right-hand branch does not close. This indicates that the revision of (∃D) as (N∃D) will ensure that the truth-tree method can determine whether a set of propositions has a logical property provided that set has a finite model. In cases where a set of propositions has only an infinite model, the truth-tree method will neither yield a completed open branch nor a closed tree.
Although we have touched on the undecidability of predicate logic in this section, the proof of this feature of RL is a topic in meta theory and so is not discussed in this introduction to logic. Nevertheless, despite the undecidability of predicate logic, this undecidability only affects a small fraction of propositions in RL, and so the truth-tree method remains a useful method for determining logical properties.
(Agler 319)
[To be honest I am still confused by how this new rule makes the situation better. When we do not use it, and the model is finite, we need to run through all the constants and redo the universal quantifier for each one too. As far as I understand, we do not invent constants that are not in the domain. So this process is long but finite. Using this new rule, do we not still need to run through all the constants? If so, then it would not seem to be more efficient. In fact it would seem to be less so, as it involves proliferating branches. But if we do not need to run through all the constants, then I do not understand how we know when to terminate the repeating procedure and how to determine if any of the remaining unexplicated branches are closed or open. Let us look at the example again and let us suppose our domain has one million constants. So it is finite, but decomposing it is impractical. Perhaps there is some way to show that since there are no negated forms in the system nor any new ones that can possibly be derived in the system, we can stop the procedure early on and assume all branches are open. I must be missing something about how this rule works.]
.
No comments:
Post a Comment