22 Jun 2016

Agler (7.4) Symbolic Logic: Syntax, Semantics, and Proof, "Undecidability and the Limits of the Predicate Tree Method", summary

 

by Corry Shores

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

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

7.4 new existential decomposition

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

 
Agler shows us an example where a combination of a proposition with an existential quantifier with one with a universal quantifier means that we must endlessly give a new constant for the one and repeat it with the other.
 

1

(∀x)(∃y)(Pxy)

P

 
[We have just one option, the main operator, which is a universal quantifier.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay

1∀D

 
[We now decompose the existential quantifier.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay✔

1∀D

3

Pab

2∃D

 
[With the way we have been making our trees, we would seem to be done. But Agler’s point seems now to note that we never completed line 1. We only found one instance. But by adding the constant ‘b’ in line 3, we now have to go back and re-decompose the universal quantifier in line 1.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay✔

1∀D

3

Pab

2∃D

4

(∃y)Pby

1∀D

 
[And we then will do this new existential quantifier.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay✔

1∀D

3

Pab

2∃D

4

(∃y)Pby✔

1∀D

5

Pbc

4∃D

 
[Uh-oh. Now we have another constant, and thus it seems we need again to re-decompose line 1, which presents the same situation and the same need to continue repeating without end.]
 

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)

 
For finite models, that is, for ones whose domains are finite, we can formulate the rule for existential decomposition differently to show that such a branch is indeed open. [I am not sure if this matters but it seems now we might need to determine in advance whether our domains are infinite or not before using this new rule.]
7.4 new existential decomposition
 

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

 
[Again, our only option is to do the universal quantifier.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay

1∀D

 
[Previously here we just decomposed line 2 for a single new constant, ‘b’. But now we will apply our new existential decomposition rule. It calls for us to make branches. We need branches for all the constants we have used so far. So one of them will be for substituting ‘a’ for y. But we also need a branch for another constant we have not used. So, we will also make one for the constant ‘b’.]
 

1

(∀x)(∃y)(Pxy)

P

2

(∃y)Pay✔

/                 \

1∀D

3

Paa                  Pab

2N∃D

4

O                         

 

 
[Now, at this point we seem to have the same problem as before. We now have the ‘b’ constant to decompose. So let us first use it for the universal decomposition and then apply the same new existential decomposition rule. This time we will need three branches. Two for the existing constants, and one for a new one, ‘c’.]
 

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

 
 
Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman & Littlefield, 2013.
 
 
Some changes to the book quotations may have been made, as based on: http://markdfisher.com/wp-content/uploads/2014/02/PHIL_012_ONLINE_SYLLABUS_SP14-3-1.pdf .

 

.

No comments:

Post a Comment