# Mod-01 Lec-41 Lecture-41-Analytic Tableau for FL

We have just completed presentation of first-order calculus, and then started with the tableau for the first-order logic. We call it FT. Let us give the rules again. It is all the rules of propositional tableau;
then we have some rules for the quantifiers and then, may be, equality. The rules were for all, which looks like,
for each x X, then from this you conclude X x by t, and then repeat the formula. It signals that it can be reused. Earlier we were not writing it; because you
need not reuse. But now, here you can always reuse them. We have something for there exists rules,
existential rules, where you cannot repeat. That is why you should specify. This not for all is an existential rule which
looks like not for each x X, from this conclude not X x by t, where t is new. To start with, we will tell that t is a new
constant. A new constant; ‘new’ means here, new to the
path, where you are developing the tableau. We will see later how to modify it; so that
it will be easier. Or, it will be better to apply. That means the tableau will be shortened,
but to work with that will be bit difficult; because we will be going relax the rules on
this ‘new’. Now, this new constant means the constant
t never occurs in that path of the tableau. Then you can give. Then we have there is rule, which is similar
to not for all. It says there is x X, then you can conclude
X x by t, where again t is new, it is a new constant. Then you have not there is rule, which is
universal. It looks like not there is x X, then you have
not X x by t for any term t; and you can reuse the formula. We have rules for equality. Which is, equality, its reflexivity, which
says anywhere in the tableau you can introduce t equal to t, for any term t. You do not need anything to be present here;
anywhere you can introduce it. Then you have substituvity of equality, which
says that, if you have s equal to t and also another which is having x X by s, s will be
occurring there; then you can introduce X x by t. It is similar to our equality axiom, right,
A7. Let us see some examples, I am not repeating
the PT rule, therefore the connective rules as earlier. Let us see. You can start with the examples as our axioms
of FC, see how the tableau proceeds there. First three things we have verified with PT,
first three axioms. They are the propositional ones; axiom one
like X implies Y implies X. So, go on applying propositional rules. Let us take with the universal rules. So one, our axiom was A4; it looks like for
each x X implies X x by t; this is your axiom. With t here, t should be a term for which
x is free in X. Now, you want to show that this is a tableau
theorem. Again, we will use the same symbol, turnstyle,
to say that it is a tableau theorem. If there is confusion, you can say, as PT
earlier, now, you can write FT. If there is another system and this also,
then you have to give the subscript, otherwise you forget it. Now, we are dealing with w. So, the tableau rules say that, to prove something
to be a theorem, you start with the negation of it, and then see that some tableau closes. For the consequences you take the, all the
premises, negation of the conclusion, in the root. Then show that there is a closed tableau for
it; with the expansion rules. So, we start with not of for each x X implies
X x by t. Then not implies rule is applicable, not p
implies q which is p and not q; both p and not q will be in the same path. So you say, for each x X, not X x by t, right. It is, because of not implies rule; then we
use for all rule. That directly gives X x by t, and that tableau
closes. If you want to mention the rules, here we
are using not implies, here you are using for all, clear. Let us see another axiom. Say, for equality you have another axiom,
for each x X implies Y implies X implies for each x Y, where this variable x is not occurring
in capital X. Let us say, right, x does not occur in X; this is our next axiom. Now, how do you proceed? We want to show that this is a theorem in
X implies Y implies X implies for each x Y. Again, not implies is applicable. So, we take for each x, X implies Y and not
of X implies for each x Y; again not implies; that gives X, not for each x Y. Now, here you have for each x X implies Y
and not for each x Y fine. So, which one to use? This one or this one? Both of them we can use; no problem. We use this one, suppose. What does it give? It gives X Implies Y, some x by t; x may be
occurring in Y; x does not occur in X. Even if you take x by t, it has no effect
on X; it is same. Next, you go for not for each x Y; that gives
not Y, of what form this is? You cannot use t again, because t should be
new to that; but t is already occurring in the path. So, you cannot use. That becomes a stumbling block. Of course, it is not a problem if you can
use s. After using s, you come back to this; use
again for that x, because that can be reused; it is universal. This sort of repetition can be avoided, if
you first do this; using this, then using this. So, these are nice heuristics to be followed
in tableau. Just as in PT you are doing, if it is a branching
rule or a stacking rule, use the stacking rule first. So that branching will be less. Now, it is a sort of branching here; though
in the same path there will be repetitions. If there is a choice between existential rule
and universal rule we have to apply, apply the existential rule first. That will shorten the tableau. So, let us use our not, not for each x Y;
that gives not Y x by t, t is new. We can say constant also c, that is what. Then we can use the for each. For each gives X implies Y x by t; fine. X implies? There is no modus ponens. Yeah? There is no modus ponens in tableau. You have to use tableau rules. So, tableau rules says, it will branch out
now; one with not X another with Y x by t; implies rule. We do not need anything else; that is what
tableau is for; it is complete by its own. Then, this is a path; for not X and X is there. So, this closes. This is a path where Y and not Y are there. So, that also closes. Let us see equality. See, you want to show that t is equal to t. You have to show by tableau rules; right? It is direct; but you have to show the proof. For the tableau formally, you have to start
with negation of that. Show that. With not of t equal t, and introduce t equal
to t, this is your equality r rule; then close it. This is what tableau asked us to do. Then we have the other axiom for equality,
A7. What was that? s equal to t implies x X by s implies X x
by t. You take the negation of the whole thing,
which is s equal to t implies x X by s implies X x by t. Then not implies is applicable. So, we have s equal to t and not of X x by
s implies X x by t. Again not implies. So, X x by s, not X x by t, right. Now, we have s equal to t, X x by s. Therefore, we introduce X x by t; that is
substitutivity of equality. From this s equal to t, X x by s, now it closes. Show that this is a theorem: there is x, well,
will take there is y P y implies P x. Such sentences will never come from natural
languages. but it can come in mathematics. Existential quantifier with implies; it can
be, sometimes. But let us see. How do you proceed? We have just completed presentation of first-order
calculus, and then started with the tableau for the first-order logic. We call it FT.
Let us give the rules again. It is all the rules of propositional tableau; then we have
some rules for the quantifiers and then, may be, equality. The rules were for all, which looks like,
for each x X, then from this you conclude X x by t, and then repeat the formula. It
signals that it can be reused. Earlier we were not writing it; because you need not
reuse. But now, here you can always reuse them. We have something for there exists rules,
existential rules, where you cannot repeat. That is why you should specify. This not for
all is an existential rule which looks like not for each x X, from this conclude not X
x by t, where t is new. To start with, we will tell that t is a new constant. A new
constant; ‘new’ means here, new to the path, where you are developing the tableau. We will
see later how to modify it; so that it will be easier. Or, it will be better to apply.
That means the tableau will be shortened, but to work with that will be bit difficult;
because we will be going relax the rules on this ‘new’.
Now, this new constant means the constant t never occurs in that path of the tableau.
Then you can give. Then we have there is rule, which is similar to not for all. It says there
is x X, then you can conclude X x by t, where again t is new, it is a new constant. Then
you have not there is rule, which is universal. It looks like not there is x X, then you have
not X x by t for any term t; and you can reuse the formula. We have rules for equality. Which
is, equality, its reflexivity, which says anywhere in the tableau you can introduce
t equal to t, for any term t. You do not need anything to be present here; anywhere you
can introduce it. Then you have substituvity of equality, which says that, if you have
s equal to t and also another which is having x X by s, s will be occurring there; then
you can introduce X x by t. It is similar to our equality axiom, right, A7. Let us see
some examples, I am not repeating the PT rule, therefore the connective rules as earlier.
Let us see. You can start with the examples as our axioms of FC, see how the tableau proceeds
there. First three things we have verified with PT, first three axioms. They are the
propositional ones; axiom one like X implies Y implies X. So, go on applying propositional
rules. Let us take with the universal rules. So one,
our axiom was A4; it looks like for each x X implies X x by t; this is your axiom. With
t here, t should be a term for which x is free in X. Now, you want to show that this
is a tableau theorem. Again, we will use the same symbol, turnstyle, to say that it is
a tableau theorem. If there is confusion, you can say, as PT earlier, now, you can write
FT. If there is another system and this also, then you have to give the subscript, otherwise
you forget it. Now, we are dealing with w. So, the tableau rules say that, to prove something
to be a theorem, you start with the negation of it, and then see that some tableau closes.
For the consequences you take the, all the premises, negation of the conclusion, in the
root. Then show that there is a closed tableau for it; with the expansion rules. So, we start
with not of for each x X implies X x by t. Then not implies rule is applicable, not p
implies q which is p and not q; both p and not q will be in the same path. So you say,
for each x X, not X x by t, right. It is, because of not implies rule; then we use for
all rule. That directly gives X x by t, and that tableau closes. If you want to mention
the rules, here we are using not implies, here you are using for all, clear.
Let us see another axiom. Say, for equality you have another axiom, for each x X implies
Y implies X implies for each x Y, where this variable x is not occurring in capital X.
Let us say, right, x does not occur in X; this is our next axiom. Now, how do you proceed?
We want to show that this is a theorem in tableau FT. We start with negation of it,
for each x, X implies Y implies X implies for each x Y. Again, not implies is applicable.
So, we take for each x, X implies Y and not of X implies for each x Y; again not implies;
that gives X, not for each x Y. Now, here you have for each x X implies Y and not for
each x Y fine. So, which one to use? This one or this one? Both of them we can use;
no problem. We use this one, suppose. What does it give? It gives X Implies Y, some x by t; x may be
occurring in Y; x does not occur in X. Even if you take x by t, it has no effect on X;
it is same. Next, you go for not for each x Y; that gives not Y, of what form this is?
You cannot use t again, because t should be new to that; but t is already occurring in
the path. So, you cannot use. That becomes a stumbling block. Of course, it is not a
problem if you can use s. After using s, you come back to this; use again for that x, because
that can be reused; it is universal. This sort of repetition can be avoided, if
you first do this; using this, then using this. So, these are nice heuristics to be
followed in tableau. Just as in PT you are doing, if it is a branching rule or a stacking
rule, use the stacking rule first. So that branching will be less. Now, it is a sort
of branching here; though in the same path there will be repetitions. If there is a choice
between existential rule and universal rule we have to apply, apply the existential rule
first. That will shorten the tableau. So, let us use our not, not for each x Y; that
gives not Y x by t, t is new. We can say constant also c, that is what. Then we can use the
for each. For each gives X implies Y x by t; fine.
X implies? There is no modus ponens. Yeah? There is no modus ponens in tableau. You have
to use tableau rules. So, tableau rules says, it will branch out now; one with not X another
with Y x by t; implies rule. We do not need anything else; that is what tableau is for;
it is complete by its own. Then, this is a path; for not X and X is there. So, this closes.
This is a path where Y and not Y are there. So, that also closes.
Let us see equality. See, you want to show that t is equal to t. You have to show by
tableau rules; right? It is direct; but you have to show the proof. For the tableau formally,
you have to start with negation of that. Show that. With not of t equal t, and introduce
t equal to t, this is your equality r rule; then close it. This is what tableau asked
us to do. Then we have the other axiom for equality,
A7. What was that? s equal to t implies x X by s implies X x by t. You take the negation
of the whole thing, which is s equal to t implies x X by s implies X x by t. Then not
implies is applicable. So, we have s equal to t and not of X x by s implies X x by t.
Again not implies. So, X x by s, not X x by t, right. Now, we have s equal to t, X x by
s. Therefore, we introduce X x by t; that is substitutivity of equality. From this s
equal to t, X x by s, now it closes. Show that this is a theorem: there is x, well,
will take there is y P y implies P x. Such sentences will never come from natural languages.
but it can come in mathematics. Existential quantifier with implies; it can
be, sometimes. But let us see. How do you proceed? We will be starting with negation
of there is x there is y p y implies P x. In fact, if you look at this, this says there
is x goes through, right; this will be equivalent to there is y P y implies there is x P x,
which is simply renaming. This there is goes through this; x does not occur. So, it becomes
there is x there is y P y implies. There is x P x, which is simply renaming; y is renamed
as variable x; that is what on the right side. So, it should be correct now in tableau.
What we do is start with the negation of this. Then it is not implies; that is not applicable
now. So, not there is, take not there is y P y implies say P a, a is new constant. You
may; t can be taken. Let us take a. Now not implies is applicable. That gives there is
y P y and not P a. Next, can you introduce P a? Because a is already occurring, we cannot
introduce. From there is y P y, you have to give P b. Let us go for P b. Where does it
close? It is not closing. But this is a universal formula. It can be reused. So, let us go for
b. That gives not there is y P y implies P b; b new, is it new? Yes, it will be new,
provided we do not have this; but do we require new? We do not require new, right? It is a
universal formula; not there is. It is a universal rule. So, we do not need new, though an existential
occurs, it is occurring after negation. The rule says anything is allowed. So, that is
all right. Fine? Then not there is, not implies, that gives there is y P y and not P b; now
the tableau closes. So, within that you have applied the heuristics, that we use there
is first, for all type of things next. Existential rules first, universal rules next. Still there
is repetition. Sir I did not understand why a new. So, b
new; and b need not be new. Just go back to the tableau rules. In the
tableau rules you have for each operator, there is one. That rule says, for all rule
says, for each x X then introduce X x by t for any term t. But for there is x X, you
have the restriction; you can introduce X x by t provided t is new. Similarly, for the
negations of the those things, fine. Negation of for all, you can introduce t to be new;
negation of there is, there is no need of new.
See, where is the rule which says for all x X then you get X x by t for any term t.
But if it is there x X, then you have to tell X x by t, where t is new; let us say, new
constant. If you introduce a, it would be a new constant to the path. Similarly, when
you go to negation of those things, you get not for all; there you need new, not there
is, no need of new. So, that is the way we have classification of those four things.
Two of them are existential; two of them are universal. Existential is, there is x X, not
for all X x; universal is the other two. So, universal, you can instantiate with any
term; existential, it should be a new constant. Is that ok? But you see; here, we have to
repeat anyway. Not P a is there, and again not P b. The same universal rule has to be
applied twice; universal formula, we have to use twice. It is because of this constant
that this t should be a new constant. But then from the reuse what do we observe? Even
if it is not new, is it not enough to say that it has not been introduced by an existential
quantifier, or the existential rule? See, if you take the other case. For example,
when you take this for each x X implies Y. Suppose you use this rule first, and keep
there is x for the next use. You have followed the heuristic, because it has been repeated,
right. Then what happens there, first for each x, you have used; you have introduced
some constant c. Next, the same constant, you cannot use for the there exists. But if
you use there exists first, then the other one, you can use. There is no problem. So
in essence, the repetition of for all rules can be avoided by choosing the existential
first; that is what we had done. Here now what happens, this constant a has
been introduced by one universal rule. So, it has the potential to be any constant. Why
this a? It could have been any constant. By chance we have just taken a. We could have
taken b also, right. Now, when after this, we are going for some particular thing; with
that particular thing again you introduce. It could have been introduced there also.
Which amounts to telling that a new constant need not be completely new; you can restrict
it. You can say that ‘it is new’ means ‘it has not been introduced by any existential
rule’; that is enough. Such repetitions can be avoided. Now, you see a generalization
of the newness. You say that this constant is a new constant; new means new to the path;
if it has not been introduced to the path by an existential rule.
But this is not sufficient because in the premises also it could have been there, in
the beginning, right. So, you have that anyway. Along with this, we should have also the constant
that it has. It is not occurring in any of the premises used in that path, premises only
anywhere, else it can be used. It can be introduced by one for all rule, no problem. It is not
occurring in any premise used in the path; it is not introduced by any existential rule
previous to it in the same path; that will give the newness.
So, there are really two conditions on this newness. Once you become accustomed to it,
it can make the tableau shorter; that is what it says. But if it is too complicated, you
can forget it. You will again re-instantiate it and then complete it; there is no harm.
Now, with this new things what you can do is, from this part of not, you can change
it. You can just say P a and it closes. You say, a new. Still you have to write a new,
right. But now new means redefinition of new; that condition is to be seen. Now this P a.
Why is it so? Because a is not in the premises; there is no premise here. It is in the negation
of conclusion, there is no premise here. So, it does not occur in the premises, a has not
been introduced by any existential rule. There is no existential rule at all used till now
that is all. Let us see one more example. Let us see how
the tableau proceeds with this. The tableau will start with this, and the negation of
this, right. Let us start there itself. These two are given. Now, you have to develop the
tableau. Our heuristic says, you should use this first, not this; this is universal now;
not there is. So, anything can be instantiated here; some particular things we have to take.
So here, let us start with that. This one in two steps, one, two, three steps. It will
come to: not Q a, not Q b, not Q c, and Q f of f of a comma b c. It will come; this
a, b, c, new; all are there exists. So, let us say, x; when I take x; I can introduce
new constant, all right? That gives, there is y, there is z not Q a, not Q y, not Q z,
Q of f of a y z. Next again, there is y. I have to introduce another constant b. So,
introduce; next, and there is z. So is another constant c; it will come like this. There
it comes; it is not correct to write in one step. You have to write really three steps
here. Finally, it will come to this; is that clear?
Next, we can use this. We want them to close; negation. It looks, we have to go for the
similar substitutions. Let us see this. So, x is a. When x is a, this gives not there
is; this is universal. You can use any constant, same constants I can reuse. Not there is y
not Q a. I am taking steps here, not doing at a time. This comes from this not there
is. Where from that come?
This one? The other one.
This one? Yes.
From the beginning, this entails this one. How to start the tableau? With premises and
negation of the conclusion. But it should be repeated.
Hm, I saved space. We will have to write it again, once more. Take this one, and then
negation of this; right? Now, from this you get not there is y with instantiation x by
a; substitution is x by a, right. Then I go for b. So, that gives not of not Q a and not
Q b, and Q of f of a b. Now, this one is not and rule. So, not and means, it will be branching.
But here it is stacking. So, I should use this first, instead of going for this. Now,
this one if I use, I get not Q a, not in one step, again three steps. Especially they will
take care, right. But anyway, they will stack: not Q b, not Q c, and Q f of f of a b c. From
this you wanted them to close. Now, we have to use this even if it branches.
What are the branchings? In fact, it will be two branches. Now, one is not not Q a,
another is not of not Q b and Q f of a not of P and Q, whole thing is Q now. Not of P
and Q is not P, another branch is not Q. Not of the whole thing. This Q a with not Q a;
that closes. I do not have to write Q a. Now, not Q a in the path, not not Q a; they close.
Now similarly, here we branch out again. That gives not not Q b and not Q f of a b; this
also closes, because we have not Q b on the path. But there it stops; it is not closing.
So, you have to use this rule. Not of that.
This is universal; this can be reused. With what we should reuse?
x as f of a b and y as c. See, we have not of Q of a b, right; it will
close with not not, not not will come from this not and this not. That is why it suggests,
you take x as f of a b. And y as c.
y as c, reason? Because it closes with q of f of a b.
We have this. We also have this; anyone of them might have closed, if you take that way,
right? Because f of a b is already x f of x y. So, this is f of a b f of f of a b. This
y must be closing with c. You have to choose y as c; z, there is no z here, that is gone
already. Now we again reuse in this branch only. That gives not of not Q f of a b x as
a b and not Q c and Q f of x is f of a b y as c. You can write here: x is replaced by
f of a b, y is replaced by c. This is the substitution used; and the only universal
here, on this. Once you use, this is again branching rule.
That gives rise to two branches not not Q f of a b; and again, not of not Q c and Q
f of f of a b c. So, this branch closes; because you have not Q f of a b. Now, this gives rise
to two branches again: not not Q c not Q f of f of a b c. And we have not Q c. That closes;
this also closes; right? See the meaning of reuse; in fact, by the rules we should write
it; we are not rewriting it; we know it is a universal. We will try to reuse it. Let us take one more example. You can try
De Morgan’s example. All horses are animals. Therefore, all legs of horses are legs of
animals. What is the symbolization? For each x H x implies A x; therefore, now we are writing
straight away for the tableau. You have to prove this by tableau. So, next one is therefore,
all legs of horses; for each x if x is a leg of some horse. So, L x and x is a leg of some
horse. There is y H y and L x y. There is a horse of which x will be a leg; then there
is one animal of which x is the leg. We should use RAA.
and the negation of the conclusion. Then which one we should use first? This one. This is the existential rule, not
for all. So, x will be instantiated; a particular instance. So that this can never be used again.
That gives not there is y H y and say L b y implies there is y A y and L b y. Next,
not implies. That gives there is y H y and L b y and not of there is y A y and L b y.
Again, this is existential. So, let us use it first. That gives H b, b is already used;
c and L b c. Well, you could have written that b is new here.
Similarly, c in new. We cannot use the same b, and moreover b is already, has been introduced
to the path by one existential rule. So, it can never be used, even in the relaxed condition.
This gives H c, L b c. Now, there are two rules which we have not used yet; this universal.
Then which one? This is also universal. These two have not been used. So, this. Use the
first one; see what happens. First one says H, what should I take?
c c is coming. So, let us take H c implies A
c. For the universal rule, it becomes an almost unwritten rule that whatever constants have
been used, you use that. For existential it is, do not use that; for the universal use
that, when it might close quickly. This gives rise to two branches, not H c and A c; and
not H c closes. Now, you take up the other one; which was
having A c. In this, we have not used this universal rule. That gives not of?
Not c? We will take c again, is the, and L b c. So,
that gives rise to two branches: not A c not L b c; not A c closes; will L b c? That also
closes. So the set inconsistent. Let me take a total relation, which is irreflexive
and which is transitive. Suppose you want to show this. Once you ask like this; it means
it is equivalent to asking for each x there is y P x y, for each x for each y for each
z P x y and P y z implies P x z. Does this entail there is x P x x? I am not saying that
we are using RAA; the tableau method itself. Tableau method says that when you go for proving
this. You take this and negation of the conclusion. That, it is inconsistent. So, your RAA is
in the definition of the tableau. Both the things are same, both the questions. Now let
us proceed. That means, even if you started with this, you take not there is x X and then
continue. You have now three sentences in the root, for each x there is y P x y, not
there is x P x x, and for each x for each y for each z P x y and P y z implies P x z.
All of them are universal rules. You have to start applying somewhere. So, let us say,
we will apply here, or here? First one.
First one. Will that give rise to there is? That gives there is y P.
A y You want P a y, this itself. Next you will
be getting P a b, b new; this, we have used once; it can be reused of course; it is universal,
this one; this you want to use. Not P a. Not P a, this is your P a. b there we have
started; not P a a, ok. X as a, y as in P x x.
Here x, as we are using, this one x as a. y as b.
b. z as? a.
a. So, this gives rise to P a b; and P b a implies P a a. It will give rise to two branches:
not of P a b and P b a and P a a. This closes. This gives rise to two branches: not P a b,
P a b. Let us take x as b. So, you get there is y P b y; it gives P b a is it, but it is
wrong. Why is it wrong? Problem is this. Is it really inconsistent semantically? Can you
give one example? It is easy here; some infinite domain, where it is satisfiable.
Well, we take the set of natural numbers. Interpret P as every natural number there
is another natural number bigger than it. Then this says transitivity: less than relation
is transitive. This says, a is never less than a; all are satisfiable. So, what tableau
shows here is that you take any finite domain, it will be unsatisfiable. But it does not
prove that it is satisfiable or unsatisfiable. This is a problem with our relaxed criterion.
If you relax that way, then it might give problems. Even if there is repetition, continue
the repetition, forget the relaxing idea, continue with the repetition. Now, the relaxation,
what you have done is not really correct; it is because of that; it is showing to be
inconsistent. Then you cannot prove completeness of the tableau, or soundness of the tableau
rather; it will not be sound even. Because all that it will show: in a finite
domain it is unsatisfiable. But that is not the question. Question is, whether the set
is satisfiable or not, infinite domain only. As to that, it will not be sound, right? Then
we bear with the repetition, and continue. That is the lesson. Suppose you bear with
the repetitions; then what will happen? You cannot introduce this P a b here. That
is what it amounts to. Everywhere else, it is correct; there is no problem. Now, then
what will you do? What will you do here? You have to give another c. So, you say P b c;
that is what you will do then. Then it looks, we will be starting from this. Just
like P a b, it will be starting from P b c again. It will introduce another d and then
it continues. So, tableau never terminates. It never closes and never stops. It remains
open. But tableau does not say anything. It is silent; because once it closes, it will
tell you, it is inconsistent; you stop there. If it does not close, continues infinitely,
it does not say anything. We have to infer from it; tableau does not say anything; tableau
method. That means, it signals that probably there is no finite model of it. Any finite
set we have started with, we see it is not satisfiable. So, probably there is no finite
model; that is what it says. Instead of this, suppose you go for the systematic
tableau. It will be clearer there; because we do not have any non-deterministic choice.
It will systematically find all the domains necessary for it; all the elements in the
domain. Now it shows that probably there is a countable model. That is what we have done.
We could give one countable model for the set; fine. But there is a relaxed criterion
for the new constant. Though the new constant idea we have introduced is not correct, there
is a relaxed criterion for the new constant. That way we have to say, that a introduced,
nowhere it has occurred; you have told nowhere it has occurred. Now you relaxed it too much.
We say that it has not been introduced by any existential rule. In fact what you can
do is, “not occur in any existential formula” that is what we need. Here it occurs in an
existential formula, that is why you are not able to use it, right? With that you can continue.
So, all that we have done today is simply found out how the tableau method is used for
proving some theorems. Then we saw the trace of undecidability in the tableau method itself,
whose answer will be there, somewhere else, as we will discuss in our last lecture.