Substitutions and Instantiations - Computer Science & Engineering Video Lecture - Computer Science Engineering (CSE)

so let us start so we did her brain's
theorem so let us actually go back a
little bit and recap those things so
actually let's look at this so we had
this herb blend tree of interpretations
and essentially what we are what we is
saying is that you take firstly our
urban interpretation so this is the set
of all possible interpretations her
brand interpretation so which
essentially means that you take any
theory that you want you do not have any
concrete representations the only
concrete representations you have are in
terms of the terms defined on that
signature and these P naught P 1
etcetera are essentially atomic
predicate symbols applied to ground
terms so which firstly implies that you
do need at least a constant so we are
always talking about a signature which
if it comes without a constant then we
extend it expand it to include a
constant at least so that there are
ground terms otherwise the set of ground
terms would be empty so you have a
non-empty set of ground terms and in
fact if you have even one constant then
if you have even one constant symbol
then you have an infinite collection of
ground terms actually and those ground
terms apply to the atomic predicate
symbols of appropriate arity enumerated
enumerate all those ground formula
ground atomic predicates and essentially
this this capital P naught naught P
naught naught b1 incidence and so on and
so forth essentially signify ground
atomic predicate formally ground atoms
and they're all possible truth
assignments for this so right so this
tree this infinite as of course you have
only accountably infinite
number of them you have only a count of
your language of terms itself produces
only a countably infinite collection of
terms and you anyway have only a finite
number of atomic predicate symbols so
the number of ground terms that you
ground atoms that you have is only
countably infinite and cannot be more
than that so so this so the herb country
of interpretations essentially gives you
all possible gives you a power set of
that so it gives you all possible
interpretations into in the term algebra
itself for all possible atomic
predicates right and what we should we
should the compactness theorem which
notice that this compactness is Wanda
fires for a set of closed quantifier
free formula here and later it is only
for closed formally yeah compartments of
closed formula so we are not really
talking about formulae which have 0
which are open and which have free
variables and so on and so forth so and
what we are saying is that a set of set
5 closed sigma formulae has a model if
and only if every finite subset of Phi
has a model in this fight can only be
countably infinite because we are
constrained by a language so it cannot
be an uncountable set of formula for
example so it is only a countable set of
formulae and there is there is one
possibility which of having things
uncountable which I am now which I have
not actually ever mentioned the only way
you could have a possibly uncountable
number of formulae is actually if your
signature Sigma
has an uncountable number of atoms or
atomic predicates symbols or function
symbols if it does or if it or simply if
it just has an uncountable number of
constants take the rails for example I
think of every real number is a constant
then I have a signature over the rails
which is actually uncountable in which
case then the number of terms that you
have is actually uncountable which also
means that you could therefore have an
uncountable number of formally but but
let us not get into that they're so so
actually so so we so in theory actually
this set Fayyad be uncountable and
provided if you have an uncountable
number of terms for example and you can
have an uncountable number of terms for
example if you have a uncountable number
of constants in your signature but let
us not get into that we will stay with
countability and are infinite Ness will
always be at most countable right so we
prove the compactness theorem yeah
how do you move from that g schoo fire
to go to a fine exit ago this is this is
because of the previous lemma right okay
but from the we found out the financial
side of g5g of qualified and then the
next line we claim is that there exists
a finite subset of five which is not how
to try this one sec okay is this where
you are saying there is a problem
after by lemma makes engine this finite
set is a subset of a finite subset of
five that does not possess some water if
it is a finite set then anyway it is
consists of ground terms okay it is
given that it is a finite set it should
be so there should be only a finite
finite number of so this is a after if
this is a finite set then you are saying
that this finite set need not be a
finite subset of capital Phi okay okay
let us let us look at schoo Phi scoffer
is obtained from capital Phi by Scola my
zhing each of those scholar mazing
findings column functions for the
existence of quantifiers there are any
way all only a finite number of them
right and when you when you find the set
of all ground instances of these all
you're doing is you are replacing all
the variables missing now after having
scala mais they are all just universally
quantified very function universally
quantified predicates and your
instantiate ngui universally quantified
predicates with ground ground terms okay
and your GF I is essentially this and
all this is countable at most all this
is countable at most and with us
assumption that it does not possess a
model means that there is a finite
subset which does not have a model and
it therefore means there is a finite
subset of Jesus co5 which does not have
a model but that G is Koh Phi that
finite subset of Jesus COFA comes from
some finite subset of atoms in five
that's it from some some finite subset
of formulae and Phi and they just some
ground instances of those some finite
set of ground instances of those that's
how you can get a finite subset you
cannot get a finite subset otherwise and
and if that finite subset does not have
a model then it means that you lift it
back to five there is a finite subset of
five which does not have a model right
so so that so that's that's what happens
here hence there is a finite subset of
five which does not have a model which
contradicts our assumption that every
finite subset of fires are model no no
think think of what happens when you go
back from g scoff I so you take a finite
subset of GA 05 which does not have a
martyr ok when you go back from jisko
Phi 2 Phi or when you go back from jisko
fight to find the appropriate elements
in schoo Phi what do you have you have
all Universal quantifiers yeah you have
all Universal quantifiers and you have
found a you have found an instance for
which that Universal quantifier is not
satisfied so that finite subset of scoff
I is not satisfiable because it is all
the all the variables are universally
quantified that scho file would have
come from a finite subset of 5 and so
what you are saying and that might have
its existential quantifiers but if there
isn't what we know is that if there is
not a model for the ground term then
there isn't a model for that that subset
to write so
so that is how this works up here so
okay I am a simple therefore the
interesting thing now but since I was
talking about countability and
countability now it therefore it is
therefore very clear that so there is
this important theorem bilo an immense
column it says that if I set 5 and this
set fight would be infinite has a model
then it has a model with the domain
which is at most countable right so this
set Phi of course again this set fire
satisfies the same constraints they have
not mentioned it here as the compactness
theorem so which means Phi is going to
be closed sigma formula there are no
free variables right so and what you are
what we are saying now is that force if
you are limited therefore what the lower
names columns theorem essentially says
is that if you are limited to a
signature which gives you at most
accountable number of terms okay then
any model of of a set of closed formula
of a countably at most countable of an
innumerable set of closed formula it is
not necessary to look among the
uncountable sense it is sufficient to
look within the countable sets which
essentially means that there for you you
need the limitation of a finite or a
countable Sigma to produce only a
countable number of terms is not
actually a limitation for closed
formerly the moment your formula become
open then the whole theorem crumbles
right so as far as closed formula which
means that if you are looking at very
general purpose theorems even about
things like the real numbers without the
assumption
of an uncountable number of constants
for example if you are looking at very
general theorems which are to be which
have to be which are let us say
universally quantified formally then the
eggs they do have de numerable models if
those theorems are true right so they do
have de numerable models and it is not
necessary to search through an
uncountable set and those de numerable
models are essentially constructible
from your signature yeah and okay so so
let us just quickly look at the proof
this is actually a very simple proof but
it is philosophically it it has a great
deal of influence I mean what it shows
is that we are not particularly limited
even if you are talking about the first
order theory of the rails you're looking
at the first order theory of the rules
and you are looking for theorems which
are of a universal nature then you are
not limited by a language which is only
countable and therefore cannot represent
all of the rails yeah that is that is
the that is actually the important
consequence of this so let us look at
the proof assume Phi has a model right
then scoff I has a model this column is
version of pfizer model by theorem 26.7
or is it has a her brain model that is
basically husband's theorem so it has a
model if and only if it has a husband
model and every her brain model has for
a for a finite or countable signature it
has only of innumerable number of terms
right and and the more the terms the
term language itself is the domain right
and that is countable that is a
countable set right and so if it has a
model if and only if the scoffer has a
model and that's at most accountable
number of formulae and therefore
any this set of closed formula Phi even
if it is countably infinite it has them
if it has a model then I am not
constrained if I just look for terms
within the harbor and universe yeah I
can find I can find a model essentially
in the her brain tree of interpretations
right so so therefore Phi has a model
with at most accountable domain there
are there are extensions of the
aluminum's column theorem actually to
uncountable signatures and finding
uncountable models and so on and so
forth but i think they are not offer of
a practical significance really are a
main concern where when we look about a
look at an accountability is really
things like the rails and complex
numbers so what happens in the first
order theory of rules what happens in
the first order theory of complex
numbers there the theorems are not open
they are always closed familiar and you
are looking at and if you have to find
examples or counter examples which is
what models are about right examples of
counter examples then you are not
constrained by the fact that you have
only a countable language countable
domain you can construct your her brain
terms for the models or or counter
examples from a countable language it is
from a countable construction okay so so
what her bronze theorem and therefore
this colonization in lower name is Colin
theorem all of them they essentially say
is that for any theory that any first
order theory at least that I am
interested in I do not need to have any
concrete models I need to have only a
language of terms if I am interested
only in the in the theorem in theorems
of closed boundary right so so one so
these so the fact that you need to limit
yourself only to a language of terms
essentially therefore makes it possible
to look at first order logic theorem
proving or and therefore logic
programming and so on and so forth as
feasible entities which which you can
work with just in a linguistic framework
you do not actually require full
mathematical frameworks you have a
simple linguistic framework and within
which you can do a programming you can
do a theorem proving and for most of the
closed formally not necessarily the open
formula yeah so for open formula of
course you are there are going to be
limitations and in fact the express
ability of various theorems is going to
be there but closed formula including
existing shal formally actually can be
done entirely within accountable
language which can be freely generated
by a grammar and that is that is
actually the model of the story and from
which the whole concept of theorem
proving or logic programming for
first-order logic actually comes right
so in this so in this yeah this files of
clothes formula i am the if you have
open formula you get into trouble yeah
so actually what happens so so so what
happens is that if you have open
formulae then then you are that that her
brain tree of interpretations is not
sufficient for all the ground terms for
all the ground instances this is it
sufficient just for the closed formally
okay so in this so what it so if you are
going to do things completely
linguistically then clearly the one of
the most important things that we need
to worry about is
notion of substitutions and basically
you look at your ground instances and so
on and so forth all of them actually
deal with substitutions so what i will
do is i will quickly go through the
theory of substitutions and take it for
granted in future yeah basically so and
this so this lecture basically on
substitutions and instantiation is going
to be independent of logic because the
notion of substitutions and
instantiation is extremely general and
whatever we say here is done from a
purely universal algebra framework and
of which your first order logic language
is also just a certain term algebra in a
universal algebra framework right so so
it does not matter whether we are
talking about the lambda calculus the
combinatory logic or first order logic
or whatever or even propositional logic
with substitutions of meta variables by
propositions you take any algebra
essentially any term algebra and you
need to perform substitutions and
first-order logic is no exception yeah
so so we look at the substitutions and
instruction a substitution theory in in
essentially a completely general
framework completely removed from
first-order logic and as far as this
theory is concerned it's just a
first-order logic is just another term
algebra in which the theory of
substitutions can be applied yeah so
that is so okay so the the slides are
not completely well prepared for this
for this lecture because it is a it is a
write-up which I have just imported
straight into this into this thing for
my for the purpose of this lecture so so
you will see certain discontinuities and
so on which I will clean up later okay a
substitution theta as far as we are
concerned is a total function okay in
fundamental to everything every term
algebra which also includes first-order
logic is the set of variables V right
and a substitution is just a total
function I am Here I am a total function
from the set of variables to the set of
terms and this is here the important
thing here in the case of a substitution
is that it is almost everywhere the
identity function which means that you
have a you have an infinite collection
of variables V but there are only a
finite number of variables which you are
actually replacing x terms all other
variables just retain their identity so
the effect of this there is no effect of
the substitution to all of the variables
so that is what i mean by almost
everywhere identity this almost
everywhere is a is a technical term used
in first order logic to say that used in
second-order logic to essentially say
that in all except of finite number of
cases yeah so so so now what we are
saying is so there are only a finite
number of variables which are actually
replaced by some some terms which are
not the same variable themselves and so
this will call the domain of this
substitution whether you shouldn't
confuse this I have you shouldn't
confuse this dog this this is this is
some Dom right wherever it where ever
written so Omega is the signature yeah
so so I use this dumb small do em to
denote only those variables which are
being replaced by other terms other than
themselves so all those variables Y for
which theta of Y is just Y itself I am
excluding from this
so remember the theta is a total
function so as a function its domain is
the whole set of variables and its core
domain is the whole set of terms T Omega
V but this small Dom essentially gives
you this finite set of variables X I
such that theta of X I is different from
X I yeah so that is what here so look at
this theta is represented as a finite
set t4x where theta of X where T is
different from X yeah so that is that is
the theta and corresponding to DOM you
also have this concept of a range here
so range is just this this set of terms
T which act as the image of the
variables which are actually being
replaced ok so there is this identity
substitution the entity substitution of
course is the identity function on way
from variables two variables itself and
therefore it is domain and range of both
empty it is DOM and wrong a range above
the MTI in that the small dormant range
okay in general let us let us skip this
because it is not relevant to first
order logic but you maybe you should
read it we have this usual notion of
admissibility of a admissibility of a
substitution for inner term or in a
predicate yeah so far all the
substitutions that we considered in
first order logic were substitutions of
essentially a single variable by a term
but what I am doing here now is I am
generalizing that notion to a set of
possible variables by a set of possible
terms and these are water this is what
is known as a simultaneous substitution
and it is quite possible that i have a
substitution theta
which replaces expo why and why forex
right okay so if I have a term let us
say f of X Y then the notion of us of
simultaneous essentially means that
theta of F of XY is equal to F of Y of X
is simultaneous and not sequential there
is no particular order it's actually
simultaneous so you look you look at all
occurrence all the occurrences of of
variables which had to be replaced and
replace them simultaneously so that
whereas if you if there was some
sequence you are applied here then you
will you will most likely get f of X X
or F of Y why you will not get F of Y X
you will not be able to switch terms
right so this the notion of simultaneous
important and the notion of and along
with the notion of simultaneity also
comes the notion of admissibility which
needs to be generalized from a single
term for variable substitution to a set
of possible substitutions simultaneous
substitutions so but the basic principle
inadmissibility is still remains the
same you do a simultaneous substitution
and there should be no capture of free
variables but that should be the that is
the basic principle on which it is
defined so in a more general fashion
what we are saying is that also a
substitution theta which replaces a set
of variables let us say x1 to xn by a
respective set of terms t 1 to t n is
admissible if each of them each of the
substitutions in that set is I
admissible right okay then we have the
notion of application of theta 2 s which
is what i said what i have given as it
is by by induction on the structure of
substitutions it has to be simultaneous
but I what I have also taken into
account
the possibility that you might have
bound variables occurring in terms this
is something that we are not we did not
actually think of it in first order
logic in the logic of terms in the
language of terms of first-order logic
there were there was no there were no
binding operators when this treatment
being general enough has to take into
account the fact of binding operators so
this this capital o X is like a typical
binding operator think of it as either a
quantifier in first order logic or think
of it as lambda X and lambda calculus
for example so what what happens to
substitution so it is it is defined by
induction yeah okay so the basic facts
about substitutions are that they are
size non decreasing the effect of a
substitution it can never reduce the
size of the abstract syntax tree on
which it is applied yeah it has to be
either size expanding or the size
remains the same the size remains the
same when you are and this is because
you are replacing our single variable
which is a leaf node of an abstract
syntax tree by a term T which is a tree
in itself right so the only way the size
can remain the same is if you replace a
variable by another variable in all
other cases the size will be increasing
yeah so as I said this whole theory of
substitutions it is not it's meant to be
general generally applicable in a
universal algebra framework yeah so in
so in general if you had if you have an
operator with its own parameterised on a
variable and having a scope which is
what happens in the case
of quantifiers it happens in the case of
lambda and the lambda calculus lambda
obstructions then what does the notion
of an instant apply applying a
substitution mean in that case basically
if any substitution of that bound
variable cannot result in any
substitution because the variable itself
it is just that there is a coincidence
of name in the substitution and in the
binding but actually the two variables
are different right I mean this what I
am saying is if X belongs to the domain
of theta okay that means in theta there
is a replacement for x x 0 term t and i
am applying this theta to a binding term
of the form some operator x s prime then
clearly this X in the binding is
different from the X mentioned in the
theta and therefore the effects should
be that this bound X throughout does not
change in any way so what it means is
that you remove that particular
substitution t4x out of theta treating
the new substitution theta prime as one
which leaves X unchanged and apply that
to the body of this s prime but that is
all that I am j all I am saying is
substitutions when pushed in through a
binding operator should not affect that
bound operate should not affect that
binding in any way yeah they do not have
any effect on that binding otherwise for
all other variables they actually push
through right through the terms which in
the terms in in when you are looking at
absa abstract syntax tree is what you
are saying is when you apply it from the
top to the route they actually filter
down to the sub trees
it is like applying the substitution
uniformly down till you reach the leaves
and then make the replace the leaf by a
corresponding 3t yeah of course if that
leaf is X and X has a binding up stop
there in the syntax tree somewhere like
this then what you are saying is so let
us take this in theta I have some syntax
tree with X occurring here and maybe a
bar X occurring with in a binding so
basically what we are saying is this
entire subtree is in the is in the scope
of this X so if I apply this theta on
this tree then this theta at least can
have no effect on this X on any of the
on on any part of the sub tree which has
X in the leaf theta cannot have any
effect on the other hand if you look at
this so that so that means this y 4x has
no effect on the subtree because X is
bound on the other hand x4 why is nola
is not admissible even if there is no
binding for why because of the fact that
they re by replacing y 4x I might be
capturing a free hour of free occurrence
so this this substitution theta has no
effect at all on this subtree but if
there is some free occurrence of X here
then essentially theta will percolate
down and replace this X by Y for example
so these are these are some basic the
the important I mean these are not
intuitively very hard to understand but
they are something that when you have to
program them you have to be careful
where does the binding take place and
therefore how does it percolate down
what is the effect so the effect of this
so here of course there is a problem of
admissibility because of which x4 why I
cannot be done but so you have to take
care of both admissibility and bound
variables one person have the natural
thing to do is to use alpha conversion
right in which case what will you do you
will replace this X by let us say a
brand new variable Z which means this X
becomes Z here and now this X 4 y
becomes admissible and so any free
occurrence of Y will be get replaced by
X but that X will continue to remain
free y 4x because of the fact that there
is no free X here y 4x has moment yeah
so so that is those are the things so
you so we use alpha conversion quite
intensively in all this to give
uniqueness of names to distinguish bind
bound variables from free variables and
so on okay so the basic fact of life
here is that substitutions are length
and our depth and size non-decreasing
and then we have the usual notion of a
ground substitution if all the terms
which are being substituted so if you
have a set of substitutions simultaneous
substitutions di X I and all the TIR
ground terms then you think then it is a
ground substitution and you also think
of common instances so if I can there
are two terms or there are two or more
terms t 1 to t n which as syntax trees
do not look alike but if there is a
substitution which can be applied
uniformly to all of them
so that the resulting trees look
identical then you will say that this
that resulting e you is a common
instance of these terms yeah I am sorry
there is not a single substitution there
is actually a sequence of substitution
there is a corresponding set of
substitutions theta 1 2 T n theta n such
that you can make all these trees
equivalent to the look the same as you
then you say that you is a common
instance yeah this is slightly different
from that of unified unification which
would come to okay so two terms T and
you are called variance of each other if
i can find two substitutions theta and
tau such that theta applied to one of
them gives me the other and tau applied
to the other gives me the first one
right but more often we will not be
looking at two different substitutions
well what we'll be looking at our so i
can take this i can look at
substitutions so this was simultaneous
substitutions but i can compose
simultaneous two different simultaneous
substitutions together in which case I
have a composition operational
substitutions which I need to define
yeah the effect and basically it is
defined by its effect on this on their
term so so essentially so I supposing I
have two different substitutions theta
and tau and for a given term TI first
apply theta so I get a new term T Prime
and then I apply ow on T prime I get a
new term t double prime so the effect of
doing tau after theta is the composition
so what is the composite effect of what
is the substitution which is which can
be considered the composite effect of
two substitutions yeah performed in
sequence that so that so essentially
this composition operation shows the
substitutions of clothes standard
composition and
there is a huge amount of case analysis
but let me let so this composition is
essentially this so I have sort ow
composed with theta I am just using
since they are like function composition
and just using the function composition
operation so there is a new substitution
Chi such that now what you need to do is
you need to look at the dorms of theta
and tau and since you are performing
things in sequence that you have to
actually perform this source so you take
so you separate out those which are not
in the domain of theta separate out
those variables which are not in the
domain of theta which means that any
application of theta will not disturb
those variables so if those variables
have to be disturbed they will be
disturbed only by tau okay and so so
this second ad end here the second
component of this Union essentially
tells you that all those variables which
are not in the domain of theta get
replaced by whatever tau specifies for
them yeah and if you look at variables
which are in the so now look at the
variables which are in the domain of
theta so theta will first replace each
of those excise by some term SI that s i
will then has its own collection of
variables which tau will again replace
some of them right so so s that is
equivalent to actually taking tau
applied to each of these terms SI and
replacing X I by tau applied to SI ya
and this is for all the excise which are
in the domain of theta for all the
excise which are not in the domain of
theta you just take the appropriate
substitution from tau and this is this p
JY j is just a substitution from town
yeah
and this Union because notice that this
is a the domain of these two
substitutions is disjoint so the union
is the composite substitution and that
is the effect of composing tau theta
yeah and essentially what this means now
is supposing theta and tau for such that
their domains what is joint then their
composition will be exactly the same as
taking the union of the two yeah they
come if their domains and ranges were
all completely disjoint then the
composition will just be the Union
otherwise you will have to apply this
tau 1 each of these a size that is right
now if you look at substitutions
themselves as an algebra with a
composition operation then the
substitution is actually form a monoid
yeah so you you take any signature Omega
you take a an infinite collection of
variables V so and you take the set of
all possible substitutions let us say
some capital s set of all possible
substitutions on this that itself forms
am annoyed with this one as identity
element and the composition of
substitutions is associative that is
something you can prove and you have a
very nice structure like this yeah
notice that I am making a
a monoid is a set which is with a
product operation which is associative
and there is an identity element okay so
the natural numbers are am annoyed and
tradition for example yeah with 0 being
included in the natural see a take take
any set of take any alphabet the set of
all strings forms am annoyed with the
empty string being the entity element
yeah it is not a billion the natural
numbers under addition are a billion
yeah it's not necessary the listeners
yeah so thats so the inverse is may or
may not exist actually so yeah oh this
is the associativity oh okay ha
basically this domain of theta
intersection domain of tau is empty and
domain of tau intersection free
variables of tea all teas which belong
to the range of tau
yes I think it should be the range of
theta okay so there is clearly a mistake
their domain of tau intersection yeah I
think it should be the range of theta
yeah I think it should because we are
looking at @ao composed sita being just
the union right so this has to be theta
definite thanks i will correct that
mistake yeah okay notice that i am
making a clear distinction between the
monoid equality and syntactic identity
yeah most books do not do that and it
makes it quite confusing sometimes okay
so so this is so okay so they this they
form a monoid and then there is there is
a notion of let me see now this may not
be very important for the rest of this
lecture so let's let's skip this
business of pure variable substitution
you can you can actually go and read it
to yourself the most important thing is
I mean there are too many theorems there
which okay yeah so let's actually so
this is this is the notion of
substitution which we want I do not
think we require all these notions of
pure variable substitutions and
substitution change there are lots of
interesting things you can prove which
which we will skip for the moment but
the more important thing is how are we
going to use this notion of
substitutions couple it with the notion
of her brand
with the consequences of the her bronze
theorem and the lower name's Colin
theorem in order to come up with
essentially a programming mechanism yeah
so that so basically we need to be able
to define this we need to be able to use
this notion of substitutions to find
what is known as a correct answer
substitution in a logic program and so
we will work our way now towards
essentially the theory of logic
programming because that that is what
happens theorem gives us the lower names
column theorem also gives us that to
look for models you need to search only
within accountable language of terms you
do not need to go any further yeah so I
have rushed through this notion of
substitutions but please go through it
somewhere but it is really ancillary but
we need to know the notion of
composition of substitutions and we need
to know the notion of simultaneous
substitutions in order to be able to
because in order to be able to actually
deal with the notions or with what is
known as a correct answer substitution
and logic programming so go through it
and we will start that next time yeah
i'll stop here
you