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

the case then you start with not x and if not x leads to contradiction then obviously

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

of logic and another thing which exercises is ah this is the paradoxes paradoxes paradoxes

etcetera so they are all valid arguments but lets something

wrong with those things you can only show that they are considering unsound there is

only be a resolution part this paradoxes or otherwise you are considered to be valid kind

of arguments so in the next lecture we will be talking

about ah semantic tableaux method and how we use it in solving two important puzzles

one is and navy’s puzzles and the second one is tiger kind of problems so these two problems

are very interesting exiting we are up by famous logician rehman and we will be taking

few problems from that particular kind of these two books then we will be trying to

solve those puzzles by using semantic tableaux method

thank you