3.6. The Model Existence Theorem 61
3. A Propositional Consistency Property that is subset closed can be extended to one of finite character.
Finally, being of finite character is enough to guarantee the existence of limits. More precisely, suppose C is a Propositional Consistency Property of finite character, and Sl, S2, S3, … is a sequence of members of C such that Sl <:;;: S2 <:;;: S3 <:;;: •••• Then Ui Si is a member of C.
The argument for this goes as follows. Since C is of finite character, to show Ui Si E C, it is enough to show every finite subset of Ui Si isinC.So,suppose{A1,.•.,Ak} <:;;: UiSijweshow{A1,•.•,AdEC. For each i = 1, ... ,k, Ai E Sni for some smallest integer ni. Let N = max{nl, ... , nd. It is easy to see each Ai E SN. But SN E C, and C is subset closed, hence {A1, ... , Ad E C.
Copyright By PowCoder代写 加微信 powcoder
Now for the heart of the proof. Suppose S belongs to a Propositional Consistency Property C. By Items 1 and 3, every Propositional Consis- tency Property can be extended to one that is of finite character. We may assume this has already been done, and so C is of finite character.
Since the list of propositional letters is countable, the entire set of propo- sitional formulas is countable as well. This is a standard result of set theory, and we do not prove it here. Let Xl, X2, X3, ••• be an enu- meration of all propositional formulas in some fixed order. We define a sequence, Sl, S2, S3, … of members of C as follows:
if Sn U {Xn} E C otherwise
Then every Sn E C, and also Sn is a subset of Sn+1. Finally, let H = Sl U S2 U S3 U …. Trivially, H extends S. Also, since C is of finite character, it is closed under chain unions, and hence H E C.
H is maximal in Cj that is, if H <:;;: K for some K E C, then H = K. Reasons: Suppose H is a proper subset of K, where K E C. Then for some propositional formula Xn, we have Xn E K but Xn f/. H. Since Xn f/. H, Xn f/. Sn+1, which implies SnU{Xn} f/. C. But SnU{Xn} <:;;: K, since Sn <:;;: H, and H <:;;: K, and also Xn E K. Since C is subset closed, Sn U {Xn} E C, and we have a contradiction.
H is a Hintikka set. Reasons: Suppose 0 E Hj we show 01,02 E H. Since o E H and H E C, H U {0l,02} E C. But this set extends H, which is maximal, hence it must be identical with H, which means 01,02 E H. The other conditions are verified similarly.
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
3. Semantic Tableaux and Resolution
Theorem 3.6.3
Now, by Hintikka's Lemma, H is satisfiable, hence, so is S, since S ~ H.O
Mathematically, it is often of interest to work with languages having an uncountable set of propositional letters. The Propositional Model Exis- tence Theorem is still true when using such languages, though the proof we gave will not work. This proof explicitly makes use of countability. Alternate proofs based on the Axiom of Choice or Zorn's Lemma can be given instead. We do not do so here.
We illustrate the power of the Model Existence Theorem by proving two of the fundamental theorems of propositional logic. Both are semantic in nature; neither mentions a proof procedure. The first is the Compactness Theorem; we will need it later.
(Propositional Cmnpactness) Let S be a set of propositional formulas. If every finite subset of S is satisfiable, so is S.
Proof Assume every finite subset of S is satisfiable. Let C be the fol- lowing collection of sets of propositional formulas: Put a set W in C, provided every finite subset of W is satisfiable. Trivially, S is in C. We claim C is a Propositional Consistency Property. Once this is shown, satisfiability of S follows immediately from the Propositional Model Ex- istence Theorem.
Suppose WEe, but both A and -.A are in W, where A is a propositional letter. Then {A, -.A} is a finite subset of W, but it is not a satisfiable set. Consequently, we can not have both A and -.A in W.
SupposeWEeanda EW.WeshoweveryfinitesubsetofWU{aI,a2} is satisfiable and hence that W U{al, a2} is in C. Now, a finite subset of W U{aI, a2} mayor may not include al and a2. If it includes neither, it is a finite subset of W alone and hence is satisfiable because WEe. The argument for the cases where it includes one ofal or a2 is similar to the argument for the case where it includes both, so we consider only that one. Suppose we have the set Wo U {aI, a2}, where Wo is a finite subset of W . Now, Wo U {a} is also a finite subset of W , hence it is satisfiable. But any Boolean valuation mapping every member of Wo U {a} to t must map a to t, hence both al and a2 must also be mapped to t. That is, Wo U {a,al,a2} is satisfiable, hence so is its subset Wo U {al,a2}.
The rest of the proof is similar and is left as an exercise. 0
Our second application of the Model Existence Theorem is Craig's In- terpolation Theorem. This result has important model-theoretic conse- quences, and we will consider it more fully once first-order logic has been introduced.
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
Definition 3.6.4
Theorem 3.6.5
Exercises 63
A formula Z is an interpolant for the implication X J Y if every propo- sitionalletterofZ alsooccursinbothX andY andifX J Z andZ J Y are both tautologies.
Forexample,(PV(Q1\R))J (PV"Q)hasPVQasaninterpolant; (P 1\ ,P) J Q has ~ as an interpolant.
( ) If X J Y is a tautology, then it has an in- terpolant.
Proof We write (8), as usual, to denote the conjunction of the members of 8. Call a finite set 8 Craig consistent, provided there is a partition of8intosubsets81 and82 (thatis,8= 81U82 and81n82 = 0) such that (81) J ,(82) has no interpolant. Let C be the collection of all Craig-consistent sets. C is a Propositional Consistency Property (Exer- cise 3.6.5).
Now we show the theorem in its contrapositive form. Suppose X J Y has no interpolant. Let 8 be the set {X, ,Y}, and consider the partition 81 = {X}, 82 = {,Y}. If ({X}) J ,({,Y}) had an interpolant Z, then Z would also be an interpolant for X J Y, hence it does not have an interpolant. Then 8 is Craig consistent, and so by the Model Existence Theorem, 8 is satisfiable. It follows that X J Y is not a tautology. 0
3.6.1. Show that every Propositional Consistency Property can be ex- tended to one that is subset closed. Hint: Let C be a Propositional Con- sistency Property. Let C+ consist of all subsets of members of C, and show C+ is also a Propositional Consistency Property.
3.6.2. Show that every Propositional Consistency Property of finite character is subset closed.
3.6.3. Show that a Propositional Consistency Property that is sub- set closed can be extended to one of finite character. Hint: Let C be a Propositional Consistency Property that is subset closed. Let C+ consist of those sets 8 all of whose finite subsets are in C. Show that C+ is a Propositional Consistency Property and extends C.
3.6.4. Finish the proof of the Propositional Compactness Theorem by showing in detail that C is a Propositional Consistency Property.
3.6.5. Complete the proof of Theorem 3.6.5 by showing that the col- lection of Craig-consistent sets is a Propositional Consistency Property.
3.6.6. ShowthatifX J Y isatautologyandX andY haveno propositional letters in common, then one of ,X or Y is a tautology.
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
64 3. Semantic Tableaux and Resolution
Tableau and Resolution Com pleteness
Definition 3.7.1 Lemma 3.7.2
3.6.7. Let C be a Propositional Consistency Property and let B be a set of propositional formulas. We say C is B compatible if, for each SEC and for each X E B, S U {X} E C. Prove that ifC is a propositional consistency property that is B compatible, and if SEC, then SUB is satisfiable.
Now that the Model Existence Theorem is available, completeness results are easy to prove, at least for the non-strict versions of tableau and resolution. In the next section we take up the completeness of tableau and resolution with restrictions that are useful for implementation. At that point the Model Existence Theorem can no longer be used.
A finite set S of propositional formulas is tableau consistent if there is no closed tableau for S.
The collection of all tableau consistent sets is a Propositional Consis- tency Property.
Proof We must establish that the conditions of Definition 3.6.1 are met. Items 1 and 2, requiring consistency at the atomic level, are trivial. For the closure conditions 2 through 5, all are rather similar, so we treat only one. It is easiest to work in the contrapositive direction. Suppose a E S, but S U {aI, a2} is not tableau consistent; we show that S is not tableau consistent either.
Since SU {aI, a2} is not tableau consistent, there is a closed tableau for SU{aI,a2}'aIsoneofthemembersofS;sayS= {a,XI,...,Xn}. Then we have a closed tableau that looks like the following.
rest of closed tableau
To show S itself is not tableau consistent, we must produce a closed tableau beginning with a, XI, ... ,Xn . But this is easy. Start with these formulas, apply the a-rule to add al and a2, and then continue the tableau construction exactly as before. 0
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
Theorem 3.7.3
3.7. Tableau and Resolution Completeness 65
(Completeness for Propositional Tableaux)
If X is a tautology, X has a tableau proof.
Proof We show the contrapositive. If X does not have a tableau proof, there is no closed tableau for {,X}. Then {,X} is tableau consistent, hence satisfiable by the Propositional Model Existence Theorem 3.6.2, and so X is not a tautology. D
If we change the definition of tableau consistency for a finite set S to no tableau for S is atomically closed, then nothing essential changes in the proofs we have given, because condition 1 of Definition 3.6.1 required only no contradictions at the atomic level. Thus, we have the stronger result: If X is a tautology, X has a tableau proof in which the tableau is atomically closed.
The Model Existence Theorem, as it stands, is still not enough to get us the completeness of strict tableaux. It is possible to strengthen the Model Existence Theorem for this purpose, but the strengthened version still does not apply readily to resolution. Consequently, we leave this approach to you in the Exercises and treat strict versions of tableaux and resolution by quite different techniques, in the next section. In the rest of this section, we use the Model Existence Theorem to prove completeness of resolution without a strictness requirement. It will be convenient to first introduce some special terminology.
Let S be a set of disjunctions. A resolution derivation from S is a se- quence of disjunctions, each of which is a member of S, or comes from an earlier term in the sequence by one of the Resolution Expansion Rules, or comes from earlier terms by the Resolution Rule. We say a disjunc- tion D is resolution derivable from S if D is the last line of a resolution derivation from S.
If {AI, ... , An} is a set of formulas, a resolution expansion for this set, and a resolution derivation from {[AI], ... ' [An]} amount to the same thing. The notion of resolution derivation is more general though, since it allows us to start with any family of generalized disjunctions.
Let X be a propositional formula. We say both disjunctions [X, AI, ... , An] and [AI, ... ,An] are X -enlargements of [AI, ... ,AnJ. If S is a set of disjunctions and S* is the result of replacing each member of S by an X-enlargement, we say S* is an X-enlargement of S.
{[AI, A2,X], [BI ,B2,B3,X]} and {[AI ,A2], [BI ,B2,B3,X]} are both X- enlargements of {[AI, A2J, [BI ,B2,B3]}.
Definition 3.7.4
Definition 3.7.5
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
3. Semantic Tableaux and Resolution
Lemma 3.7.6
Suppose 8 1 and 8 2 are sets of disjunctions, and 8 2 is an X -enlargement of 81 . If the disjunction D1 is resolution derivable from 81 , then there is an X -enlargement D2 of D1 that is resolution derivable from 82 •
Proof The informal idea is quite simple: carry-along occurrences of X at appropriate points in the resolution derivation from 81. A formal proof is by induction on the lengths of resolution expansions. Length 1 is trivial.
Suppose the result is known for resolution derivations from 81 of length < n, and we now have a resolution derivation of length n. Say the last line came from an earlier line using the ,6-Resolution Expansion Rule. Then the resolution derivation from 8 1 looks like:
Since [,6, AI, ... , AkJ occurs at a line earlier than line n, by the induc- tion hypothesis, there is a resolution derivation from 82 ending with an X-enlargement, one of [,B,A1, ... ,AkJ or [X,,6,AI, ... ,AkJ. In the first case, [,6I, ,62, AI, . .. , AkJ follows by the ,6-rule, and in the second case, [X,,6I, ,62, AI, ... , AkJ follows, still by the ,6-rule. Either way, the result is established for line n in the ,6-case.
This takes care of one case. There are several more, depending on the rule used to add the nth line. We leave the other cases as an exercise. 0
A finite set 8 of propositional formulas is resolution consistent if there is no closed resolution expansion for 8.
An equivalent version of this definition follows: {XI, ... , Xn} is resolu- tion consistent if there is no resolution derivation of the empty clause from {[X1J, ... , [Xn]}.
The collection of all resolution consistent sets is a Propositional Consis- tency Property.
Proof Again we must establish that the conditions of Definition 3.6.1 are met. Items 1 and 2, requiring consistency at the atomic level, are straightforward and are the only ones that directly involve the Reso- lution Rule. Of the closure conditions 3 through 5, we consider only
Definition 3.7.7
Lemma 3.7.8
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
Theorem 3.7.9
3.7. Tableau and Resolution Completeness 67
the a-case and the (3-case. As with tableaux, it is easiest to show the contrapositive.
Suppose a E Sand S U {aI, a2} is not resolution consistent. We show that S itself is not resolution consistent. Say S = {Xl, ... , X n , a}. Since S U {aI, a2} is not resolution consistent, there is a resolution derivation, call it D, of [] from {[Xl],... ' [Xn], [a], [al]' [a2]}. Now, a verification that S is not resolution consistent can easily be produced as follows. Start a resolution derivation with [Xl],... ' [Xn], [a]. Apply the a-rule to add [all and [a2], and then continue with the steps of D.
Next, suppose (3 E S and neither S U {(3l} nor S U {(3d are resolution consistent. We show S is also not resolution consistent. This time things are just a little trickier.
SayS={(3,Xl,...,Xn}. Applyingthe(3-ruletoaresolutionderivation beginning with [Xl]' ... , [Xn] , [(3] allows us to add [(31, (32]. It follows that to show S is not resolution consistent, it is enough to show there is a resolution derivation of [] from [Xl],... ' [Xn], [(3], [(31, (32].
Since S U {(3d is not resolution consistent there is a resolution derivation of [ ] from {[Xl], ... ' [Xn],[(3], [(3l]}. Then by Lemma 3.7.6, there is a derivation from {[Xl], ... , [Xn], [(3], [(31, (32]} of either [ ] or [(32]. In the first case we are done immediately; the second possibility requires a little more work. Since S U {(3d is not resolution consistent, there is a resolu- tion derivation, call it D, of [ ] from {[Xl], ... , [Xn],[(3], [(32]}. All these disjunctions already occur as lines in the derivation from {[Xl], ... ' [Xn], [(3], [(31, (32]} that we have produced thus far, and we can use these lines again, since we are not imposing a strictness requirement, so simply con- tinue by adding the lines of D to produce a derivation of [ ] directly. 0
(COlnpleteness for Propositional Resolution) If X is a tautology, X has a resolution proof.
Proof Exactly as with tableaux: If X does not have a resolution proof, there is no closed resolution expansion for {,X}. Then {,X} is resolu- tion consistent, hence satisfiable by the Propositional Model Existence Theorem 3.6.2, so X is not a tautology. 0
Just as before, we can change the definition of resolution consistency for a finite set S as follows: There is no closed resolution expansion for S in which all applications of the Propositional Resolution Rule are atomic. This does not affect the proof of Theorem 3.7.9, and so we have the stronger result: If X is a tautology, X has a resolution proof in which all applications of the Propositional Resolution Rule are atomic.
Fitting, Melvin, and . First-Order Logic and Automated Theorem Proving, edited by . Schneider, Springer New York, 1995. ProQuest Ebook Central, http://ebookcentral.proquest.com/lib/warw/detail.action?docID=3077179.
Created from warw on 2022-04-26 11:58:13.
Copyright © 1995. Springer New York. All rights reserved.
68 3. Semantic Tableaux and Resolution
3.7.1. Call a set U of propositional formulas upward closed if 1. Z E U => -,-,z E U.
2. al E U and a2 E U => a E U. 3. (31 E U or (32 E U => (3 E U.
Show that any set S has a smallest upward closed extension. (We call this the upward closure of S and denote it SU.)
3.7.2. Using the notation of Exercise 3.7.1, show that for any sets of propositional formulas:
1. (SU)U = SU.
2. Sl <;;; S2 => St <;;; S7f.
3. Sl <;;; S7f => St <;;; S7f.
4. If L is a literal, L E SU {o} L E S.
5. If -,-,Z rf. S then Z E SU {o} -,...,Z E Suo
6. If a rf. S then a E SU {o} al E SU and a2 E SU. 7. If (3 rf. S then (3 E SU {o} (31 E SU or (32 E SU.
3.7.3. Let C be a collection of sets of propositional formulas. We call C a strict propositional consistency property if it meets the following conditions for each SEC:
1. For any propositional letter A, not both A E S and -,A E S.
2. ..1 rf. S; -,T rf. S.
3. -,-,Z E S => S- U {Z} E C, where S- is S with …,-,zremoved.
4. aES=>S-U{al,a2}EC,whereS-isSwitharemoved.
5. (3 E S => S- U {(3d E C or S- U {(32} E C, where S- is S with (3 removed.
Show the following: If C is a strict propositional consistency property, and SEC, then S is satisfiable.
Hint: Suppose C is a strict propositional consistency property. Let CU = {SU I SEC}, and let C* be the subset closure of Cu. Show C* is a propositional consistency property. Exercise 3.7.2 will be useful.
3.7.4. Use Exercise 3.7.3, and show every tautology has a strict tableau proof.
3.7.5. Complete the proof of Lemma 3.7.6
Fitting, Melvin, and
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com