# Semantic Tableaux Method for Propositional Logic: General Examples

welcome back in the last lecture we discussed
syntax and then the in the in the next lecture we talked about semantics of propositional
logic and basically we are trying to cover a kind of crash course on ah propositional
logic because it is consider to be the most important thing for doing modal logics because
modal logic is considered to be an extension of classical logic so in this lecture i will
be talking about some of the important definition that we have left left it out or we need to
discussing somewhat more detail ah they are logical consequence consistency satisfiablity
etcetera with some examples and then i will quickly move on to one of the important methods
that we will be using it in our course that is it is also considered to be a decision
procedure method which is called semantic tableaux method
so before that let me begin with ah the definition of logical consequence so the notation goes
like this if you take gamma as some set of formulas and we use gamma for that particular
kind of thing which includes all the formulas that exist more propositional logic and a
ah a is any kind of propositional formula and if you write gamma and union a ah it is
set of all formulas together with a given formula if that is the case then ah gamma
is set to be valid in a any given model m that means n satisfies gamma if and only if
a is considered to be logical consequence in that model m it happens for every formula
that is a n which exist in a given to the formulas set of formulas gamma and in all
interpretations given formula is true then it is consider to be ah a tautology and all
tautologies are considered to be valid formulas so we define we denote this thing as n ah
any other letter a as something like that and when we say that gamma is considered to
be done set of formulas that we have that is considered satisfiable if and only if they
exist in model m such that gamma is considered to be logical consequence in that particular
kind of model m and it is refutable if and only if their exist in model m such that m
ah gamma ah gamma doesn’t follow from m a gamma is considered to be valid which is denoted
by gamma ah follows from something ah gamma follows in a model m it happens for every
model m and it is considering unsatisfiable if it is not satisfiable at so basically talking
about three important things logical consequence satisfiablty tautology etcetera
now why we stress little bit on logical consequence because logical consequence occupies central
position in any logical system see in classical logical we defined logical consequence like
this if a b formula and gamma is some set of formulas and it’s it happens in this way
that in very if very modal that validates gamma also validates whatever is there on
right hand side that is a then we say that ah gamma entails a or a is a logical consequence
of gamma since that the formula is gamma so a is considered to be a prepositional needs
this is the set of formulas formulas or formula is considered to be valid as it is writtened
in the sense a is logical consequence ah especially where a abbreviates less thing we dont try
to anything on the left hand side means a has to be obtained from empty side so that
means it has to be tautology that means a does not require any ah kind of do for anything
values so it is a it is considered to be tautology so in the same way a is considered to be contradiction
especially when ah both is consequence of a given formulas if and two formulas are set
to be logically equivalent each other especially when ah b is logical consequence of a and
the same way a is also logical consequence of b or rather way found of saying this is
that a if and only if b has to be valid or a if an only b as to be a tautology
in classical logical we mean tautologies are considered to be valid formulas and valid
formulas are also considered to be tautologies there are a two other important things which
you come across a while doing any logical’s these are like this soundness and completeness
usually an argument can be valid ah any given argument which considering to be valid and
it also has two premises then it is considered to be sound argument if any given argument
is valid but it has i mean one of the premises is considered to be false then it is considered
to be unsound argument as for as the argumentation is concerned
so in propositional logic soundness is defined this sense ah particularly when ah whatever
is proved is also consider to then the system is considered to be sound and the system is
have to be consistent when all the usually you required this thing for this reason that
in we want all the prove all the truths to be provable and all the provable things are
considered to be true at tautologise so proof theoretic consequence relation ah
single constant have used two symbols single constant double constant ah which is considered
to be sound with respect to a semantic consequence of relation ah double constant if and only
if every possible set of premises let say p one p two p three etcetera and every possible
conclusion q p one p two p three from that q follows then q is the has to be logical
consequence of p one p two p three so in a nut shell what it says this is the ah if q
ah is reduced from gamma it implies that q has to be true then q has to be logical consequence
of gamma so if a is ah the ways from gamma then a is
the semantic consequence of gamma a is considered to be logical consequence of gamma it means
all provable things are considered to be true and the completeness is like this a proof
theoretic consequence relation ah single constant is considering to be complete with respect
to a semantic consequence relation ah double constant if and only if for every possible
set of premises p one p two p three etcetera and every possible conclusion q and this q
has to be semantic consequence of all those thing p one p two p three that means all this
premises should make ah the conclusion true it is like has been as saying that a given
a argument is valid especially when it is impossible for premises
to be true and the conclusion to be false if you it happens in such a ah it happens
in a way that your premises are true and conclusion is false if the given argument is invalid
so ah this is the this is also it can be viewed as it can also viewed has relationship between
syntax and semantics in the syntax we talked about single constant and semantics we talked
about double constant the relationship between these two ah if you want to have a relationship
between these two we need to have soundness and completeness property but the basic ideas
is that whatever you have proved ah at the end of the day your proves have to be true
and what all considered to be true if a nano matrix etcetera i have to have a proofs ah
but this is objectionable kind of thing that in ah then as come up within an interesting
a his incompleteness theorems you came up with a view that ah this cannot be the case
they are obvious truths but they are not provable any given formal system which is ah following
it’s own rules etcetera but he cannot sure that it is consider to be complete it means
all ah all truths cannot be provable so a basic questions we asked in the formal
logic or this things the soundness of the deductive system any given formal logical
system we will be asking this questions how sound it is ah that means no provable formula
ah has to be invalid that means it as to be false if something is proved it has to be
true and the completeness of the deductive system all valid formulas have to be provable so we ask this important question that is
the system is consistence is the system is complete or sound etcetera there are two important
things ah for the logicians some other things are considered to be very important let us
consistency completeness etcetera ah these these two are considered to be the most important
questions at logicians we would be asking or working in any kind of logic
so there is another important thing which we need to know all this things which will
be using it in the modal logic while discussing about the modal logic so these are the terms
that you come across even there also what do you when do you say that ah system is considered
to be formal logical system is considered to be maximally consistent a set of formulas
again gamma is set to be maximally consistent if and only if it as to be consistent and
there is one more requirement that is further more given any formula ah this is important
requirement ah that is gives back either a has to be provable or it has to be provable
not a is the case but definitely not both the things there are
some logical systems for example in the case logics etcetera ah suppose if you cannot prove
a it cannot even true not a then we have to withdraw your fundamental principles of logic
one of the fundamental laws of logic that is law of law of means tell us that either
p is the case or not p is the case one excuse the other one ah if you cannot prove p and
it cannot prove even not p there is no way in which we can ah validate this fundamental
law of logic that is the law is excluded middle so for the maximal consistency either a as
to be derivable or not a as to be the case but it should not be a case that both are
derivable from a given system in maximally consistent sets are considered to be closed
for derivability that is given a maximally consistent set gamma and given a formula a
a is reduced from gamma implies that a has to be in that particular kind of set of formulas
gamma so while we talked about maximally consistent
set because when we discuss about ah some other concepts like possible words etcetera
ah in the case of model logic you required this maximally consistent sets the possible
world- there is defined in the sense that ah it is considered to be maximally consistent
set of sentences ah they are considered to be possible worlds in that contexts we need
to know little bit about maximal consistency ah there is supporting theorem that is lambda
that is is that if gamma is considered to be consistent then there exists gamma prime
which is super set of gamma so is that gamma prime is considered to be maximally consistent
i am just for superficially i am talking about some of the important theorems it is possible
to discuss all this things in ten twenty minutes like that all this things require a rigorous
proves etcetera ah there are very interesting books and ah rechecked to introduction to
logic ah there you will find this integrate one best text book is that introduction to
mathematical logical by mendel’s this is a good starting point for understanding all
this ah the theorems and laminars so another important thing we need to notice
is that gamma is set to be consistent if if and only if it is satisfiable ah that is also
we need to note ah there are some important properties of this entailment relation ah
and it is like this i dont want to going to the retails of all this things but i will
quickly switch on to the ninth one that is gamma is set to be inconsistent if and only
if you derive contradiction form in a given formula gamma other wise it is said to be
consistent this is the one which will be using it in
our method ah decision procedure method is semantic tableaux method ah gamma is to be
consistent then either a as to be ah gamma union a as to be the case or gamma union is
not a as to be case but not definitely not both if any system in which you derived the
both things a and all b also in that particular kind of system is considered to be inconsistent
and these are some of the important properties that any classical logic follow base in particular
so particularly there is one interesting property that we need to highlight ah here so that
is monotonicity property that is second one if a is logical consequence of gamma when
you can ah you can add ah some further statements gamma and see and from that also ah a follows
ah but in most of the cases may not happen ah for example if is if you represent it like
this in the case of conditional statement that we are going talk about little bit later
suppose if you say that if there is a sugar in the coffee and would be tasty obviously
it is case that sugar makes a coffee tasty ah some of us and then if you say that in
a addition of new information such as if there is a sugar in coffee and then -kerosene in
coffee then it will be tasty so from a implies b one of the logical consequence of a implies
b is is that a and c implies b where c is considered to be the new information there
ah so that need not have to be the case in non monotonic logics where in you need to
drop this particular kind of ah thing is follow in classical logic that is a monotonicity
property in the ah whole lot of logics that are emerged from this one they come under
the category of non monotonic logics now let us get back to this important method
that is semantic tableaux method i will be highlighting this method because you will
be using ah this method and we will be extending this method for modal laplace etcetera it
will be later ah this is consider to be one of the important methods and easy to use and
this method is used to it’s like a decision procedure method with which you will be able
to tell when a given proposition formula is valid formula or a tautology and when two
formulas are said to be consistent to each other or when two formulas are said to be
logically equivalent each other ah many things you can talk about ah when two formulas are
said to be a formula to be satisfiable etcetera so they are independently it worked out by
many ah the three important logicians any one claims that ah method is due to them only
so it’s started with beth’s works ah and it is further simplified by hintikka in the in
his model sets and raymond smullyan ah also used ah is considered to be the founder of
this particular kind of method it doesnt matter of who as ah come of this method but this
method is very interesting ah here what we do is in a what we essentially
do is that given any formula which are in the propositional logic we draw it’s corresponding
tree diagram ah a semantic tree which is called as semantic tree semantic tree is considered
to be a device for displaying all the valuations and given ah set of formulas are considered
to be true ah the basic idea is that one of the important things which you will need to
notice is that truth table method is also considered to be decisions procedure method
but it is going to be difficult for us to track all the rows are truth table especially
when the number of variables increases if they are three variables we have eight entries
in the truth table it is easy to manage and the number is increases n is equal to seven
or eight then we have one twenty four increase very difficult to monetised those things it
is difficult for us but the computer can do it easily but it is difficult for us
so semantic tableaux method simplifies the those things so the basic idea here is is
that any inference is considered to be valid if and only if their exits no counter example
in argument is considered to be invalid if i have counter example like a premises are
true in conclusion is false then it is set to be invalid kind of argument so the same
way ah suppose if you have well formed formula something x and if you denied the formula
and it leads to contradiction then that ah not x is considered to be unsatisfied unsatisfiable
that means x as to be satisfiable x as to be valid argue unsatisfiability of not x guarantees
that x is considerable to the valid argument so we need to ensure that if you want to show
that x is valid you have to show that not x is unsatisfiable so these are some of the
basic ideas that we will be will be using it here ah the basic ideas is that any invalid
arguments as true premises and a false conclusion so this method involves a rule based construction
of a counter example for a given inference so what we do start with negation of the formula
in a given formula and then we will construct tree diagram for the given formula and then
we will see ah if all the paths of the particular kind of tree closes or not this whole thing
is called as tableau and this is also called tableau method
so when the tableau method closes after denying the formula that means not x is considered
to be unsatisfiable and that guarantees such that x is considered to be valid it is kind
of reduction- add up certain kind of method suppose if you are asked to show that x is
that is not x is considered to be the unsatisfiable that means x as to be valid ah truth these
are considering one of the most efficiency base are checking semantic properties of propositional
formulas like truth tautology etcetera validity all those things and in particular it gives
very easy way of checking the validity of sequence especially when the member increases
four five etcetera propositional variables increase then it definitely help us the basic
idea of truth is that we give ah graphic way of usually say the picture say side- inverse
ah it if this is the effects whether or not set of formulas is set to be consistent or
inconsistent etcetera so this is some of the rules that we used
for constructing tableau ah as you seen in this tableau rules this three ah tableau ends
with atomic formulas it is most important which we need to note for not p it is same
as not p when when you have a compound formula p r q ah it is a branch living to p q and
if we are appealing to both p and q have to be true p implies q has this particular kind
of structure not p or q and p is a negative q it is written as p and q and as a not p
and not q ah these are considered to be alpha rules
now beta rules exactly a negotiate of that one are like that not not p is same as p not
of p and q that use demorgan’s laws and not p and not q so that’s why you have a trunk
of the tree and not of p and q is not p not q
so we just considered one example and then we will see ah whether from p plus q and r
are not q and not of p forgets or not so here p is considered to be ah the conclusion so
it is like this ah then ah p r q r r not q and then not r and then whether p follows
from this r not so we want to check whether the p is at consequence of this r not so in
the semantic tableaux method what you do the first initial step is is that you deny the
conclusion so this is what is denial of conclusion that means you are trying to construct a counter
example here so now ah what you do is you simplify this
formulas with alpha semantic trees that we we use the so now if you apply on the this
one the tree diagram for this one r r not q it is to be like this r not q so it’s a
branch that’s why it looks like this so now you write the same bit of information here
ah r not q now this is over that’s why we checked it so that’s why we put a tick mark
right here over here now the formula left first is this one so
this can be written like this not p r q so this particular piece of information needs
to be written under all open branches so this branch not yet closed so branch will be closed
only when a literal hence negation after symbolic branch then we have to close the branch so
now same bit of information you need to write here
so now we need to see whether ah this branch closes r not so we have p plus q r r not and
we exhausted all the things and ultimately we have ended up with only atomic propositions
so now this branch remains open because you know in which has ah this branch gets closed
here because r and not r is here so this gets closed here this remains open this sides also
closed because r and not r is there now here we have not p not q and all so this
branch remains open where as this gets closed so now what kind of situation is that ah denial
of the conclusion ah doesnt lead to contradiction so that means we cannot ah surely say that
x is considered to be a valid argument so what what essentially we are trying to do
here is this the ah if i want to know that p is logical consequence of the given formulas
we are starting with negation formula and then we construct a tree diagram for these
things and then ultimately we we are trying to see whether not x leads to contradiction
so there is a principle in logic ah which is considered to be reductio and up seven
and this is like this if from not x leads to some kind of contradiction so then it should
not be not x but it should be not of not of x so this is same as x one so that ensures
such that x is construct to be valid but in this case it appears to be the case that after
exhausting the tree rules here i mean you under go with the automatic formulas you did
not come up with the branch closer so branch closer suggests that not of x is
unsatisfiable if not x is unsatisfiable ah then x is considered to be valid so that means
your counter example did not work there so in the next lecture we will be talking about
this semantic tableaux method in greater detail and ah we will be using this semantic tableaux
method for solving solve the important puzzles ah these are the some other which are considered
to be very interesting and exciting logic as a subject matter with particularly interesting
especially when you study this puzzles try to solve this puzzles by using the basic concepts