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

It is in the tableau proof; we start with the premise

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.