Mod-01 Lec-19 Lecture-19-Compactness & Analytic Tableau

So, let us start with one consistent set of
proposition sigma. Then we could extend it to sigma prime, which
we proved to be maximally consistent. This fact, that a consistent set can be extended to a maximally consistent set is called Lindenbaum Lemma. That may not happen in every system. In this system it happens. That means, Lindenbaum Lemma holds in PC. Next, we have proved some of the properties
of sigma prime, this maximally consistent set, it just, essentially, capture the connectives. So, our last four properties, one for negation
that either p or not p belongs to sigma prime, for any proposition p, and then the other
three for the implications. Those properties, if a set, holds; in a set
if those three-four properties hold, then we would say that the set is a Hintikka set. There are many technicalities here. That means, we have proved that there exists
a Hintikka set, which happens to be your maximally consistent set sigma prime. We are almost over in proving the completeness
of PC. The formulation was if sigma is consistent
then it should be satisfiable, right? What about sigma prime? Sigma prime is consistent. Can we show that it is satisfiable? In fact, that is the technique, that is why
we had extended sigma to sigma prime, and that sentence, that statement says that if
sigma is consistent, it is also satisfiable; this is called the Model Existence Theorem. There exists a model for a consistent set. This is what we want to derive next. This says, if sigma is consistent, then it
has a model. I will say that then sigma is satisfiable. Its proof is easy now. What we have to do is, find a model for sigma. Here only we are connecting PC to PL, consistency
is a PC concept, coming out of proofs, this depends on proofs, and satisfiablity comes
from the semantics, truth and falsity; here we are connecting now. So,
What we do is, let sigma be consistent; then consider sigma prime. Now, sigma prime is maximally consistent
and it, along with it, it satisfies all those properties. What happens, you define one function, define
some function i from the set of all propositions. Now, in the set of all propositions, we do
not have those connectives: and, or, if and only if, and then we do not have top and bottom
also, right? There is no, not these symbols in PC, that
is our PROP now, which is appropriate to PC. Define from the set to 0, 1, a function by
taking i of any proposition, say u equal to 1, if u belongs to sigma prime, it is 0, otherwise. Now is it not obvious? Let this i be a model of sigma prime, it is
because by definition it is 1, but we have to verify that it is really a Boolean valuation. It is a function that is fine, but it has
to be a Boolean valuation in order that it is a model, that is why we have done all this
work. Now, it should be obvious that it is also
a Boolean valuation because of this 4 properties. If we take any proposition u, either u is
in sigma prime, or not u is in sigma prime, right? So, either it is given 1 or its given 0 with
respect to the negative sign, negation sign; and what about other properties? The other three properties capture the implication,
right? If q belongs to sigma prime, that is, if i
of q is equal to 1, then p implies q belongs to sigma prime. So, i of p implies q is equal to 1, right? That is the first property of implication. Next, if not p belongs to sigma prime, that
is, if p is given the truth value 0, then p implies q is also given a truth value 1,
it belongs to sigma prime, right? That is the next property of an implication. Then you see that if p is true q is false,
that is if p belongs to sigma prime and q does not belong to sigma prime, then p implies
q should be false, that is also true: p implies q does not belong to sigma prime, that is
your last property, right? We just see from these, that i is a Boolean
valuation, due to last four properties, which were that 5 to 8 of sigma prime? And that is all, that is the end of the proof. i is a model of sigma prime and sigma is a
subset of sigma prime, so i is a model of sigma. i satisfies sigma prime, sigma is a subset
of sigma prime, so, i is a model of sigma. Easy consequence. Once you have sigma prime, there is nothing
to prove, and there by you have also proved adequacy of PC to PL. In fact, strong adequacy, right? Let us mention that. So, adequacy really means what? Sigma entails w if and only if sigma semantically
entails w. This is your strong adequacy. If you do not have strong-ness, you say w
is a theorem if and only if w is valid, without any sigma’s, right? Its proof is easy, because this is, this holds
if and only if sigma and not w is inconsistent, and this holds if and only if sigma union
not w is unsatisfiable. Now, consistency and satisfiability are equivalent. Model existence theorem says one part, soundness
theorem says the other part, right? In fact adequacy means soundness plus completeness,
both the things are there, is that clear? There is a nice consequence of it; it says
something like: you start with one infinite set. Suppose that it is unsatisfiable. Then you can prove that there exists a finite
subset of it which is unsatisfiable. That is what compactness means, right? Which means. Same construction will prove it, but we do
not have to prove it once more, because you have adequacy, and in PC we have finiteness. Immediately you can come to it. So, if you want see, for, this says, it looks
simple now for all these, but it is not a very simple concept. We just start with one infinite set, infinite
set of propositions. Now, you take all its finite subsets, right? Suppose, if you claim that each of the finite
subsets has a model, right? Can you construct a model for the whole infinite
set? This is the problem. Do you see it? as a particular case suppose you have sigma which have w1, w2, w3 and so on. Now, for w1, you have a model for w1,
w2, you have a model, w1, w2, w3 also have a model and so on, right? But not only these, we are assuming something more. There are, assume every finite subset of it has a model. Now, how to construct a model for the whole set? The clue is, when you say that every
finite set, subset, has a model, it is not necessarily the same model it is not the same I it can be different I It need not be an extension from a subset to a super set of it, it can be completely different Still from that you can always construct one model for the whole infinite set. That is what compactness says, right? Let us write that compactness for PL. It says: let sigma be an infinite set; if each finite subset of sigma is satisfiable, then sigma
is satisfiable. The proof is easy. What you have to say is, proof is by contradiction;
if sigma is unsatisfiable then there exists a finite subset of sigma which is unsatisfiable.
Which finite subset, we do not know, but we can show there exists one. So, suppose sigma
is unsatisfiable. Then by strong completeness theorem or model existence, whatever you take,
we want only completeness; you see that sigma is also consistent. Now, you are trading between
PL and PC. If sigma is satisfiable then sigma is also consistent. You will have : if sigma
is unsatisfiable, then it is also inconsistent. Now, suppose sigma is inconsistent; so that
means sigma entails p sigma entails not p, but some proposition p. Now, again you tread
between PC and PL. You say, sigma semantically entails p, sigma semantically entails not
p. But, wait a minute. From the PC itself, when you say it entails, you have a proof
of it, but that proof contains only finite number of propositions. So, both the proofs
have only finite number of propositions, each. So, there union is also a finite subset of
sigma, now you concentrate on that finite subset and tread between PC and PL. Call that
as sigma 0, which is the union of all those used in both the proofs or either of the proofs
rather, right? You have to take the union. Then sigma 0 entails p, sigma 0 entails not
p, semantically, sigma 0 is unsatisfiable. That is the proof, yeah?
All the properties are not compact properties, that is why it becomes non-trivial. For example,
suppose in natural numbers, you take any finite subset of natural numbers, it will have the
maximum, but the whole set of natural numbers does not have a maximum. So, taking a maximum
is not a compact property. But here it is; satisfiability is a compact property. That
is what it says; that is why it becomes non trivial. Though in PC it is very trivial,
that definition is through a finiteness property, the proof is a finite sequence. That is why
when you say PC and PL are adequate, it gives some more information, it is not just I have
started with some axioms and proved it, fine? If we get some time, we will do some applications
of compactness. Right now, we will not, we will resist the temptation.
See in PC, what happens, you are looking at the proofs now. Construction of proof is not
effective, as we have seen; but but not proved it. Why it is not effective? All that we have
seen, from our experience, that the idea of proof, notion of proof is effective. You can
always check whether some sequence of propositions is a proof or not, but how to construct a
proof depends on your cunningness. It is not mechanical. Can you have a mechanical method?
Something like that, resolution; it was somewhat mechanical; when? But you had to use cnf conversion,
that is again mechanical. So, there is a hope, mechanically something can be done, right?
And it is mechanical from the beginning. Suppose, you have a finite set of propositions,
you can always find out whether it is consistent or inconsistent, mechanically, we have very
crude procedure, construct its truth table, right? It is very long, it does not matter,
there exists a method. That, that concept is called decidability of a theory. So, in
propositional logic the thing is decidable, whether something is consistent or inconsistent
is decidable, provided you have that for a finite set. For infinite sets, you do not
know. What to do? Now, we will see that there is still, there
are still some other methods, which can be very easy, and will present one such method.
In fact the method is so easy and so intuitive, at the same time it is so formal, that logicians
become addicted to it. Once you say this is consistent or not, immediately they will go
for that. Yes? We will see why is it so. it is very simple observation. Suppose, I take p and q, one proposition;
now, how do I decide whether this is true or false? Well, first thing is, p and q is
true, if both of them are true, right? So, you just construct a tree, if p and q both
are true then p and q will be true. Suppose I take p or q, a similar construction, p or
q will be true if at least one of them is true, right? I have now two cases, just the
way you did from your childhood. There are two cases, one of the cases will succeed,
then I say that p or q is true, right? So, I will branch into two parts p, q; I just
keep it, I do not know what will happen to this p or q, but this can happen, right? This
gives a method, how to proceed, but this says that preliminary conversion is required for
and, or but we will not do that way. What we will do is, we will try to identify the
forms of propositions. The propositions can be in which form? Suppose,
all the connectives are used. Then, let us see what can be the forms of the propositions.
This is required because by De Morgan, say, not of p and q, though I know p and q is true.
When both of them are true I can make a tree with both p and q in this same path, right?
But if it is not p and q, now it is equivalent to not p or not q. I know it is equivalent
to not p not q, then I should have crossed out with one as not p, another as not q, which
says not of p and q is true, if one of this is true.
Now, you see even if and is there, because of negation sign, some proposition can be
just and of something or negation of and of something. Similarly, from each connective
or; the four connectives, you will get eight such cases, right? A proposition can be in
that form or negation of that form, is it? And then, you have top and bottom, you have
to do something for that; you have double negation. It can be not not, any number of
not’s can be there, right? So, recursively you should have a rule for not not also. Then
this expanding propositions in such a fashion is called a tableau; you go on finding the
tableau. How it is going, finding out the cases when it can be true, and so on.
These types of trees are called Beth’s semantic trees. Sematically, we are just completing
a tree, making a tree, finding out what are the possibilities when it can be true, right?
Propositions at the root can be true, when, that is what the trees answer this. Trees
have been modified to make a proof method, that is what we are going to present. These
tableau will have certain rules depending on the forms of the propositions; we just
write the rules first. Let us see, we will have rules of this form.
If it is in the form not not, you get p. Again we will write in this fashion, fractions.
This means, if not not p is there, this will be true. If this is true, semantically it
looks like, but when we construct a true proof system it can be semantically motivated where
there is no trace of semantics there. It is mechanical; that is what do; we want to make
just like our PC. So, you just construct them as rules. Now, think of them as rules for
getting the semantics, whenever need will come, we connect them, right?
Now, if it is in the form not top, we can write a bottom. If it is p and q, we will
have p, we will also have q. If it is not of p and q, then we will have two children,
one is not p, another is not q. If it is p or q, we have again two children. This can
be written as a fraction, this is a straight, this way, when you construct the tableau we
will be constructing the trees. Then p or q will have p on one side, q as the other
side, right? See if you do not like the fractions, you can simply connect by vertical bars or
slanted bars. It does not matte; we have not of p or q, which will be not p, not q; both
are in the same path, right? Next, you may have p implies q, which will have, again,
two children, one is not p, another is q. See the semantics, p implies q is equivalent
to not p or q. Next you have not of p implies q, which is equivalent to p and not q, right?
So, we will have p, not q in the same path. Next, if and only if, p biconditional q, this
is true when both of them are true or both of them are false. So, we will keep in one
branch p, q, both, on another, not p, not q. Then negation of p if and only if q. That
is equivalent to either p or q, right? Exclusive or, this is true when one is true, the other
is false. That gives rise to p, not q, not p, q.
These are all the tableau rules. Any proposition can be in these forms, or there can be another
form like bottom only. We have to give some where this rule. We have take care of that,
how only bottom can be handled, okay? That is only missing here, fine?
Now, as it says, as our heuristic says, if a proposition is given, you are going to apply
the tableau rules and then branch out, construct the tree. Construct the tree as we can, as
far as you can go, continue. After the construction, what are you going to do? That is the point
where we have to write something about the rules. How to use the rules; that we know
now, for the construction of the tree, for the expansion; then after you expand what
you are going to decide? Well, it is also easy. For example, I take
p and not p, I know this to be unsatisfiable, okay? Now, for the tableau rules, it gives
me p, not p both. Semantically this says, in order that this will be true, this will
be evaluated to 1, both p and not p should be evaluated to 1, which is not possible,
right? As a child, if it is not possible I will cross
it, right? It is not possible. This is what we are going to introduce in the tableau.
If, in a path of a tableau we find that there are two complimentary pair of literals, there
is a pair of complimentary literals, then you close that path with a cross, provided
that you had applied the tableau rules on every situation wherever it is applicable.
Then you will end in literals. But you may not end in literals. If you end in a proposition
p and also its negation, then also it is fine, whatever way we expand, they will close, is
that clear? For example? Let us see. I have p or q and
not of p or q. Then once I apply the tableau rule, it will give me p or q, and again not
of p or q. Now, not of p or q gives me not p, not q. And p or q gives me p, q as different
children, okay? Now, I see the path. The path you can see either from the root to leaf or
from leaf to root, does not matter. Let us take root to leaf as usual. So in this path,
you see that p is there, not p is there. So, this path closes. In the other path, I see
not q is there, q is there; that also closes. Now, the question is why should I go this
far? I have already got the proposition u and not u. Whatever way I expand they will
close, right? This is the shortcut we will be going to work with. Instead of going to
the level of literals, whenever you find the proposition and its negation, stop there,
close the branch, is it okey? That is why we did not have a rule for the
bottom; this is what we are going to write. If you find in a path a proposition or its
negation, you close it or if you find in a path bottom is occurring, close it; because
that will tell you: in order that the propositions in that path are true, bottom should be true;
it can never be. So, that path also closes, right? That is how we are tackling this bottom;
all others are given in the rules. Our rule will be: if in a path you get a proposition
and its negation, okay? That is one case. Second case is: if you find a bottom then
close the path. Now, suppose you take a proposition and construct a tableau for it using the tableau
rules. You see that every path closes, then what do you conclude? It is unsatisfiable.
If every path does not close? We are getting the literals.
See from the begging itself, I could have told that p and not p are satisfiable. I do
not expand it, I become lazy. p and not p, I do not expand it, I keep there. Now, this
also a tableau by definition, it is open, it is not closed. So, it is really satisfiable,
but that is not the case, right? That means to take a decision that one open path really
gives rise to a model which will make it satisfiable, you have to see that all the compound propositions
have been expanded. So, compound means all those propositions in the forms of the numerators
in our rules, right? They are the compound propositions.
So, you should have applied a rule on the compound propositions, in that path; if it
is done, still the tableau remains open, then it will be satisfiable. We have to make certain
definitions for all these situations; to take care of the situations, then it can start.
Let us give a definition for whatever we need there. First thing is, you have the tableau
rules, then you have to say how to expand the tableau so that a proposition at the root
of the tableau can give rise to a tableau. These were criptically written; it says start
from a proposition, then apply the rules if it is compound, and continue; that is what
it says, recursively, right? But then there is one simple question. The question is this:
let us look at the tableau, we have constructed here from the third proposition, we got not
p and not q instead of the third, suppose I go for the second. What will happen? I have p or q, I have not
of p or q, now I first apply or rule, I would get p, another as q, now I want to apply this.
See that. that is the point. That is the subtle point, while you are completing the, going
for the tableau expansion. Once you take one proposition at the top level, which is beyond
all these branching and you want to apply tableau rule on that, then you have to add
on every leaf. Because, tableau are expanded path-wise, you have to concentrate on each
path, because we are going for a construction of a model along that line, right?
So, in programming, it can be is easy, because you can expend all these things path-wise,
continue, if it does not close, you stop there; if it closes you backtrack; that can be done.
But while doing it manually, usually you apply it breadth-first way, not this way path-wise.
Once you do breadth-first way, be careful about that. If you apply a rule, you think
that I have already applied, but that is guaranteed if you have added it every where. Let us take
it, I have not used it; to use this, I have to add not p, not q in both the branches.
This is what it says. Now you can see all the paths will be the same, same literals
here, same literals also here, is it clear? Now, you have to define all these things formally. A tableau is expanded or it is constructed
path wise, in a path rules are applied on the compound propositions. In this sense,
the tableau rules are really tableau expansion rules; they are used to expand the tableau,
right? That is how it is constructed throughout. Sometimes you need have to concern with the
whole tableau; somewhere you find p and not p is there, for some proposition p; you close
it. There is no need to go further. If we want to go further, then you should give a
name for that kind of tableau, right? Say that, the path is, so path means path
from root to leaf, wherever you are now, that is current leaf, a path is called closed if
it contains p and also not p for some proposition p, or it contains bottom. Otherwise, you say
the path is open. These open and close, they are dynamic; up to some level a path can be
open, but once you apply another, one of its paths can be closed, even both of them can
be closed later. It is a dynamic thing. A path is called complete, called complete,
if it can no more be expanded, right? That means on each of the compound propositions
occurring in that path, a rule has been applied, right? If on each compound proposition occurring
in that path, a tableau expansion rule has been applied. See, some times you say I do
not have to complete the path, I can take decision before it. So, we will also include
one term for that. We will say that a path is completed, if it is closed or it is complete.
That means, it is essentially complete, right? Nothing can be done for it; you know it is
closed, you have decided for it, or it remains open. Nothing more can be done by using the
tableau expansion rules. In fact, we wanted this completed path to take any decision,
right? Then you come for the tableau itself. Let us leave it here. A tableau is closed if all its paths are closed.
This is what, should give us an unsatisfiable proposition at the root. Similarly, we say
a tableau is complete if all its paths are complete, not one, complete, everywhere compound
propositions have been resolved, those have been expanded. Similarly, you say tableau
is completed if all its paths are completed, right? So, closed or complete or completed,
all these hold. Now, comes the next one, a tableau is open
if, here you require that, if at least one of its paths is open, not every, right? You
do not need every, if at least one of its paths is open. For taking decision
whether this is satisfiable, you may need an open completed tableau, right? It should
be completed; if it is not complete, but only open, a decision cannot be taken. It can still,
further be expanded and found to be closed, okay? So, we need a completed tableau for
that. Then you should define the syntactic part of all those things. We cannot say satisfiable
or unsatisfiable here because it has nothing to do with the truth or falsity, though it
is semantically motivated, but as a proof system it may not have any semantic content,
right? A tableau for a proposition w is a tableau
with root as w. You have to define everything almost. Once you say a tableau for a proposition,
that means you start the tableau with the root as w, then continue expanding it. Similarly,
we can say a tableau for a set of propositions, say, sigma, is a tableau with all propositions
of sigma at the root. Now, we define the theorem, a tableau theorem
or we say, propositional tableau, PT, for propositional tableau, is a, or we can say
what is a theorem. We start with a proposition. We say w is a PT theorem if what happens,
if there exists a closed tableau for not w. Now, you see reductio ad absurdum is inbuilt
in the definition, okay? You start with not w, then expand it, find that the tableau closes.
See, a tableau may not be unique; it depends on which order, we are using the rules, it
can become very different. So, all that you need is there exists a closed
tableau, fine? Then similarly for a set of propositions. We say that sigma is inconsistent,
in fact we should write PT inconsistent, inconsistent in the system PT, if there exists a closed
tableau for sigma. Start with all the propositions at the root and then continue by using tableau
expansion rules, see that it closes; if it is closes, you say that it is inconsistent.
Similarly, you say sigma entails PT w, right? If sigma union not w is inconsistent, PT inconsistent.
So, inconsistent here means PT. Slowly, since you have become matured, we forget this PT,
always writing, you will say inconsistent, PT theorem as theorem and so on. Once we are
in the context of tableau, it will be interpreted as tableau consistency, not PC consistency,
okay? Let us see one a example, at least how to show something is inconsistent or not.
Let us see whether this happens or not. In fact, you should have PT here, as a subscript,
in PT only, we are deciding. So, that means some times will say that sigma entails w has
a tableau proof, that is also used. Now, how to proceed? You simply start with
sigma union not w. So, p implies not q implies r, p entails not q not of p implies r. Suppose,
if we write in different propositions vertically, because you want to apply the rules, right?
They will be on the same path, so it is more logical to start with vertical things, than
comma and then write it. Now, we have to apply the rules. See, I want to apply a rule on
this first, why? If I start from this, then it will branch out from the beginning; then
at every branch I have to add this. If I start with this one it will be stalking, it is not
branching. So, it will be helpful, okay? In all those rules wherever you get two children
they are called the branching rules, others are called the stalking rules. They are just
stalking the propositions one after another, the other ones are branching out. Now, it
is helpful as a heuristic that if there is a choice, go for the stalking rules instead
of the branching rules; that will make the tableau shorter.
Now if I apply not implies rule, I can give names to all the rules. Let us call these
rule as not not, that is the form of proposition, we will be meeting. This one will be not top,
this is and, this is not and, this is or, this is not or. Similarly, this is implies,
this is not implies, this is biconditional, this is not biconditional. That says the form
of the proposition directly. Now, if I apply not implies rule it gives
you p not r, is that right? Next, which one? Well, I can go for the middle one, instead
of these, that will I can branch out. So, this gives implies rule, I use. That gives,
what? So it is often easier for you if you go for a book keeping device. Once I use this,
I tick it; it will not come further. Then, what about p implies not q? It will branch
out to not p, not q. Now, I close it. Instead of applying this, I will close it here, because
I have already got p and not p in this path. So, I close it. And on this not q, the other
path, not q, not r, p and so on. And I have one on which I have not applied a rule, the
tableau expansion rule. This, I have to apply, implies rule, so that gives me not p and then
not q implies r, they come in this path; I find not p, not q, not r, p. So, p and not p are there; that path also
closes. Then I look, what, q implies r, all the things have been used in this path, there
is another compound proposition where I have not used the rule. So, I branch out to not
not q and r. If we use double negation it will go to q, but I do not need that. I have
not q, here not not q. You can further take q, but does not matter. That also closes.
And here not r and r, also closes. So it is closed. Therefore, the set of propositions
is inconsistent. We do not have to say that, we just say, this is true by tableau method;
because our definition says: if there is a close tableau for sigma and not w, that we
have taken directly. Now, as an exercise, you can try all the axioms
of PC and MP also. See, how do they go in tableau rules? Slowly you should get acquainted
with this; very quickly you can decide what happens, that helps. So, today we have done
tableau. No, we have done also completeness of PC and compactness and then the tableau rules. We will discuss again tableau next time.

One Reply to “Mod-01 Lec-19 Lecture-19-Compactness & Analytic Tableau”

Leave a Reply

Your email address will not be published. Required fields are marked *