COMP304 (Knowledge Representation & Reasoning)

Decision Method

It is important to find a decision method for the consistency checking problem.

The tableaux method allows us to solve this problem but only for acyclic knowledge bases.

Using Concepts

An atomic concept $A$ directly uses an atomic concept $B$ if there is a subsumption $A\sqsubseteq X$ or $A\equiv X$ in $\mathcal T$ such that $B$ occurs in $X$.

For example if the following is in $\mathcal T$:

then $\text{grandparent}$ directly uses $\text{person}$ and $\text{parent}$.

An atomic concept $A$ indirectly uses an atomic concept $B$ if there is a finite sequence $A_1, \ldots, A_n$ of atomic concepts such that $A$ directly uses $A_1$, $A_1$ directly uses $A_2, \ldots,A_{n-1}$ directly uses $A_n$ and $A_n$ directly uses $B$.

For example if the following are in $\mathcal T$:

then $\text{mother}$ does not directly use $\text{person}$, but $\text{mother}$ does use $\text{person}$.

Cycles

• A knowledge base $\mathcal K$ contains a terminological cycle if there is a concept that uses itself.
• A knowledge base $\mathcal K$ is acyclic if:
  • $\mathcal K$ contains no terminological cycle
  • Every atomic conept occurs on the left-hand side of at most one subsumption in $\mathcal T$.

Cyclical Example

The Tableaux Method

Let $\mathcal K=(\mathcal A,\mathcal T)$ be an acyclic knowledge base. Consistency of $\mathcal K$ is checked in six steps.

1. Eliminate $\sqsubseteq$

Suppose $A\sqsubseteq X$ occurs in $\mathcal T$:

1. Add a new atomic concept $A^*$ that characterises those $X$ that are $A$.

   $A^*$ is the property that distinguishes those $X$ that are $A$ from those $X$ that are $\neg A$.

2. Replace the concept with $A\equiv X\sqcap A^*$
3. Call the resulting knowledge base $\mathcal K^*$.

2. Expand the TBox

1. If $A\equiv X$ is in $\mathcal T^*$, then every occurrence of $A$ in other concept definitions can be replaced by $X$.

   Replace simple objects with their definitions.

2. Keep replacing until no futher replacements are possible.
3. Call the resulting TBox $\mathcal T^{*e}$.

If $\text{

3. Eliminate Defined Concepts from the ABox

Suppose $o:A$ is in $\mathcal A$ and $A\equiv X$ is in $\mathcal T^{*e}$:

1. Then we can replace $o:A$ by $o:X$.

   We replace objects by their definitions.

2. Call the resulting ABox $\mathcal A^e$.

4. Put the ABox in Negation Normal Form

This step removes negations from the ABox.

1. Rewrite formulas in $\mathcal A^e$ in such a way that negations only occur immediatley in front of atomic concepts.
2. Call the resulting ABox $\mathcal A^{en}$.

In order to put formulas in NNF, you can use the following replacement rules:

5. Apply Completion Rules to the ABox

This step builds a tree of sets of concept and role assertions:

• The root of the tree is $\mathcal A^{en}$.

Whenever one of the following rules can be applied to any node $\Gamma$, use them to generate new nodes:

6. Check the Leaves for Contradictions

A set $\Gamma$ contains an immediate contradiction if $o:\bot\in\Gamma$ for some $o$.

If no more rules can be applied, check the leaves (endpoints):

• If all endpoints contain immediate contradictions, $\mathcal K$ is inconsistent.
• If at least one endpoint contains no immediate contradiction, $\mathcal K$ is consistent.

Consistency

The simplest form of error is inconsistency. A knowledge base $\mathcal K$ is inconsistent if it is impossible to satisfy:

• $\mathcal K$ is inconsistent if for every $\mathcal I$ we have $\mathcal I\nvDash\mathcal K$.

In addition to knowledge bases, TBoxes and ABoxes can also be inconsistent by themselves.

Coherence

A concept is coherent if it is possible, according to the knowledge base, for there to be objects satisfying it:

• A concept $X$ is coherent in $\mathcal K$ if there is some interpretation $\mathcal I$ such that $\mathcal I\vDash\mathcal K$ and $X^\mathcal I\neq\emptyset$.

Incoherent concepts are not necessarily errors:

• Incoherence of an atommic concept is almost always an error.
• Incoherence of non-atomic concepts are a warning sign, by often not an error.

Coherence Example

For the following TBox:

• $\text{parent}\equiv\text{person}\sqcap\exists\text{hasChild}.\top$
• $\text{grandparent}\equiv\text{person}\sqcap\exists\text{hasChild}.\text{parent}$

The concept $\text{parent}\sqcap\text{grandparent}$ is coherent, while $\neg\text{parent}\sqcap\text{grandparent}$ is not.

Entailment

An assertion $o:X$ is entailed by $\mathcal K$ if every interpretation satisfying $\mathcal K$ also satisfies $o:X$. This is written as:

A subsumption $X\sqsubseteq Y$ is entailed by $\mathcal K$ if every interpretation satisfying $\mathcal K$ also satisfies $X\sqsubseteq Y$ (this is also true for $X\equiv Y$). We write this as:

Only concept assertions can be entailed, therefore $\mathcal K\vDash (o_1,o_2):r$ is impossible.

Entailment Example

Let $\mathcal K=(\mathcal A,\mathcal T)$ be given by:

We have:

• $\mathcal K\vDash\text{Claire}:\neg\text{parent}$
• $\mathcal K\vDash\text{grandparent}\sqsubseteq\text{person}$

Reductions to Consistency

Coherence and entailment are related to consistency:

• Coherence:
  • $X$ is coherent in $\mathcal K$ if and only if $(\mathcal A\cup\{o:X\},\mathcal T)$ is consistent, where $o$ does not occur in $\mathcal A$.
• Entailment:
  • $\mathcal K\vDash o:X$ if and only if $(\mathcal A\cup\{o:\neg X\},\mathcal T)$ is inconsistent.
  • $\mathcal K\vDash X\subseteq Y$ if and only if $(\mathcal A\cup\{o:X,o:\neg Y\},\mathcal T)$ is inconsistent, where $o$ does not occur in $\mathcal A$.

As a result of the reductions, if we can determine whether a knowledge base is consistent, we can also determine coherence and entailment.

Subsumption

In description logic we want to compare concepts to each other. Comparisons are called subsumptions.

Subsumptions are of the form:

• $X\sqsubseteq Y$

  The objects that satisfy $X$ are a subset of the objects that satisfy $Y$.

• $X\equiv Y$

  The objects that satisfy $X$ are exactly the same as the objects that satisfy $Y$.

TBox

Taxonomy

A categorisation of concepts.

TBox

A finite set of subsumptions that represent a taxonomy.

TBox may only contain subsumptions where the left-hand side is an atomic concept (not a complex concept).

Example TBox

• $\text{parent}\equiv\text{person}\sqcap\exists\text{hasChild}.\top$
• $\text{father}\equiv\text{parent}\sqcap\text{male}$
• $\text{mother}\equiv\text{parent}\sqcap\text{female}$
• $\text{grandparent}\equiv\text{person}\sqcap\exists\text{hasChild}.\text{parent}$

ABox

Sometimes we want to make more specific statements such as “Ann is a parent”. We do this using concept and role assertions.

Concept Assertion

The object with the name $o$ satisfies the concept $X$.

We can write:

• $\text{Ann}:\text{Parent}$

Role Assertions

The objects with names $o_1$ and $o_2$ stand in relation $r$ to eachother.

We can write:

• $(\text{Ann},\text{Claire}):\text{hasChild}$

  This means Ann has a child called Claire.

Therefore an ABox is a finite set of concepts and role assertions.

A knowledge base $\mathcal K$ is a set of A and T boxes:

Satisfaction

Assertion Satisfaction

Let $\mathcal I=(\Delta,\cdot^\mathcal I)$ be an interpretation, and let $\mathcal A$ be an ABox:

• $\mathcal I\vDash o:X\text{ iff } o^\mathcal I\in X^\mathcal I$
• $\mathcal I\vDash (o_1,o_2):r\text{ iff }(o_1^\mathcal I,o_2^\mathcal I)\in r^\mathcal I$
• $\mathcal I\vDash\mathcal A\text{ iff } \mathcal I$ satisfies all assertions in $\mathcal A$

Subsumption Satisfaction

Let $\mathcal I=(\Delta,\cdot^\mathcal I)$ be an interpretation and let $\mathcal T$ be a TBox:

• $\mathcal I\vDash X\sqsubseteq Y\text{ iff } X^\mathcal I\subseteq Y^\mathcal I$
• $\mathcal I\vDash X\equiv Y\text{ iff }X^\mathcal I=Y^\mathcal I$
• $\mathcal I\vDash \mathcal T \text{ iff }\mathcal I$ satisfies all subsumptions in $\mathcal T$

Knowledge Base Satisfaction

Let $\mathcal I$ be an interpretation and $\mathcal K=(\mathcal A,\mathcal T)$ be a knowledge base:

• $\mathcal I\vDash\mathcal K\text{ iff }\mathcal I\vDash\mathcal A$ and $\mathcal I\vDash\mathcal T$

Satisfaction Example

Consider the interpretation from the previous lecture:

graph LR
y[y<br>Bob,person,parent] -->|hasChild| z[z<br>Claire,person]
x[x<br>Ann,person,parent] -->|haschild| z
u[u<br>dog]

• $\mathcal I\vDash \text{Ann}:\exists\text{hasChild}.\text{person}$

• $\mathcal I\nvDash\text{dog}\equiv\neg\text{parent}$

  This is because there are people who are not parents.

Description logic is used to describe ontologies:

An ontology defines objects by their relations to other objects.

We have seen ontologies before in COMP111:

• Derived Assertions Algorithm
• Relations & Non-Unary Rule-Based Systems

Language of ALC

Attribute logic with complement (ALC) is a multi-agent modal logic (with different symbols).

An ALC signature is a triple $\Sigma=(\mathcal O, \mathcal C, \mathcal R)$ where:

• $\mathcal O$ is a set of object names.
• $\mathcal C$ is a set of atomic concepts.
• $\mathcal R$ is a set of relations symbols.

This is comparable to the set of propositional atoms and the set of agents that were used in propositional and modal logic.

Formulas of ALC are called concepts. Concepts are denoted by $X,Y,Z,X_1,\ldots$ and given by:

where $A\in\mathcal C$ and $r\in\mathcal R$.

• An object name $o\in O$ describes a single object. There can be objects without names, but every name refers to exactly one object. No object has multiple names.
  • Ann, Bob; Fido.
• An atomic concept is a single word that describes a number of objects.
  • Parent, father, male, person; dog.
• A concept combines one or more atomic concepts into a more complex description:
  • A parent who is male.
  • A person who has a t least one child that is a parent.

The final two concepts are defined as:

• $\exists r,X$ indicates those objects that stand in the relation $r$ to some object that is $X$:
  • $\exists\text{hasChild}.\text{female}$ is someone who has at least one daughter.
• $\forall r.X$ indicates those objects taht only stand in the relation $r$ to objects that are $X$:
  • $\forall\text{hasChild}.\neg\text{female}$ is someone who only has children that are not $\text{female}$ (a person whose children, if any, are all sons).

Additionally:

• $\top$ defines any object.
• $\bot$ indicates no objects.

ALC Language Examples

• A person who has at least one child:
  • $\text{person}\sqcap\exists\text{hasChild}.\top$
• A parent who is male:
  • $\text{parent}\sqcap\text{male}$
• A person who has at least one child that is a parent:
  • $\text{person}\sqcap\exists\text{hasChild}.\text{parent}$

Semantics of ALC

ALC Interpretations

In description logic we refer to models as interpretations.

Let $\Sigma=(\mathcal O,\mathcal C,\mathcal R)$ be a signatire. An interpretation $\mathcal I$ over $\Sigma$ is a pair $(\Delta,\cdot^\mathcal I)$ where:

• $\Delta$ is a domain (a non-empty set).
• $\cdot^\mathcal I$ maps $\mathcal O$ to $\Delta$:
  • For every $o\in \mathcal O$, $o^\mathcal I\in\Delta$.
• $\cdot^\mathcal I$ maps $\mathcal C$ to $2^\Delta$:
  • For every $C\in \mathcal C$, $C^\mathcal I\subseteq\Delta$.
• $\cdot^\mathcal I$ maps $\mathcal R$ to $2^{\Delta\times\Delta}$:
  • For every $r\in \mathcal R$, $r^\mathcal I\subseteq\Delta\times\Delta$.

and further more $o^\mathcal I_1\neq o^\mathcal I_2$ unless $o_1=o_2$

What are Interpretations

• $\mathcal O$ are a set of names of individuals, $\mathcal C$ a set of names of concepts and $\mathcal R$ a set of names of relations.
• $\Delta$ are things that actually exist.
• The map $\cdot^\mathcal I$ tells us who has which name:
  • $\text{Ann}^\mathcal I$ is the person who has the name Ann.

Drawing Interpretations

Suppose:

• $\mathcal O={\text{Ann, Bob, Claire}}$, $\mathcal C={\text{person, dog, parent, grandparent}}$, $\mathcal R={\text{hasChild}}$
• $\Delta={u,x,y,z}$
• $\text{Ann}^\mathcal I=x$, $\text{Bob}^\mathcal I=y$, $\text{Claire}^\mathcal I=z$
• $\text{person}^\mathcal I={x,y,z}$, $\text{dog}^\mathcal I={u}$, $\text{parent}^\mathcal I={x,y}$, $\text{grandparent}^\mathcal I=\emptyset$
• $\text{hasChild}^\mathcal I={(x,z),(y,z)}$

This can be drawn as:

graph LR
y[y<br>Bob,person,parent] -->|hasChild| z[z<br>Claire,person]
x[x<br>Ann,person,parent] -->|haschild| z
u[u<br>dog]

Lifting Interpretations

Assume the following:

• $A^\mathcal I$ - Interpretation of the atomic concepts $A$

  Those objects that satisfy $A$.

Interpretation $\mathcal I$ can be lifted - we can determine whether $X^\mathcal I$ in the following way:

• $\top^\mathcal I=\Delta$
• $\bot^\mathcal I=\emptyset$

• $(X\sqcup Y)^\mathcal I=X^\mathcal I\cup Y^\mathcal I$

  The objects that satisfy $X\sqcup Y$ are those objects that satisfy either $X$ or $Y$.

• $(X\sqcap Y)^\mathcal I=X^\mathcal I\cap Y^\mathcal I$

  The objects that satisfy $X\sqcap Y$ are those objects that satisfy both $X$ and $Y$.

Additionally we have:

• $(\forall r,X)^\mathcal I={u\in\Delta\mid\forall y\in\Delta:(u,y)\in r^\mathcal I\implies y\in X^\mathcal I}$

  The objects that satisfy $\forall r.X$ are those objects that are related by $r$ only to objects that satisfy $X$.

• $(\exists r,X)^\mathcal I={u\in\Delta\mid\exists y\in\Delta:(u,y)\in r^\mathcal I\text{ and } y\in X^\mathcal I}$

  The objects that satisfy $\exists r.X$ are those objects that are related by $r$ to at least one objects that satisfies $X$.

Lifting Interpretations Example

Considering our previous example:

graph LR
y[y<br>Bob,person,parent] -->|hasChild| z[z<br>Claire,person]
x[x<br>Ann,person,parent] -->|haschild| z
u[u<br>dog]

we can solve the following:

• $(\text{parent}\sqcup\text{dog})^\mathcal I={x,y,u}$
• $(\forall\text{hasChild}.\bot)^\mathcal I={z,u}$
• $(\text{person}\sqcap\text{dog})^\mathcal I=\emptyset$

Common knowledge relates to multiple agents knowing the same thing about each-other:

• People drive on the left because we know that other people know to drive on the left.

Definition of Common Knowledge

We can use $E$ to denote that “everybody knows”:

• $E\phi$ means $K_a\phi\wedge K_b\phi\wedge\ldots$

Fixed Point Definition

A formula $\phi$ is common knowledge, denoted by $C\phi$, if and only if:

• Everybody knows $\phi$ (so $E\phi$)
• Everybody knows that $\phi$ is common knowledge (so $EC\phi$).

This definition is circular, so can’t be proven.

Transitive Closure Definition

A formula $\phi$ is common knowledge, denoted by $C\phi$, if and only if:

• Everybody knows $\phi$ (so $E\phi$)
• Everybody knows that everybody knows $\phi$ (so $EE\phi$)
• Everybody knows that everybody knows that everybody knows $\phi$ (so $EEE\phi$)
• $\vdots$

This one is linear to can be determined.

Semantics of “Everybody Knows”

• $M,w\vDash E\phi$ if and only if every successor of $w$ satisfies $\phi$ (regardless of which agent defines the successor)

• Additionally:

  \[M,w\vDash E\phi\iff M,w\vDash K_a\phi\wedge K_b\phi\wedge\ldots\]

Semantics of Common Knowledge

• A world $w_2$ is reachable from $w_1$ if $w_2$ is a successor of a successor of $\ldots$ a successor of $w_1$.
• $M,w_1\vDash C\phi$ if $\phi$ holds on every world that is reachable from $w_1$.

flowchart LR
w7 ---|a| w8
w1 ---|a| w2
w2 ---|b| w3[w3<br>p] & w4
w3 ---|a| w5[w5<br>p]
w4 ---|a| w6
w3 ---|b| w4

• $M,w_1\nvDash C\neg p$, since $w_3$ and $w_5$ satisfy $p$ and are reachable from $w_1$.
• $M,w_1\vDash C(p\implies K_ap)$, since every reachable world satisfies $p\implies K_ap$.
• $M,w_7\vDash C\neg p$, since every world reachable from $w_7$ (namely $w_7$ and $w_8$) satisfy $\neg p$.

Public Announcements

You can never gain common knowledge by using imperfect communication channels.

A public announcement is an event that provides new information to the agents in such a way that:

• All the agents receive the same information.
• The received information is true.

• It is clear to all the agents that everyone receives the information without error.

  Other agents should observe other agents observing.

Notation: $[\phi]\psi$ meaning “after $\phi$ has been publicly announced, $\psi$ is true.”

Semantics of Public Announcements

• The public announcement operator $[\phi]$ is a dynamic operator:
  • This means that to determine whether $M,w\vDash[\phi]\psi$ we have to look at a different model $M*\phi$

1. This model $M*\phi$ is obtained by removing all $\neg\phi$ worlds from $M$.
2. All arrows to and from removed worlds are simply deleted.

A public announcement has to be true. If $\phi$ is false we consider $[\phi]\psi$ to be trivially true.

We define public announcements like so:

Let $M=(W,\mathbf R, V)$ be a model and let $w\in W$. Then $M,w\vDash[\phi]\psi$ if and only if either $M,w\nvDash\phi$ or $M*\phi,w\vDash\phi$ where:

There are many examples of public announcment models starting at slide 12

The correspondence of:

• Reflexivity and truthfulness
• Transitivity and positive introspection
• Euclidity and negative introspection

This proof system is known as $S5$.

Truthfulness

Knowledge is truthful, therefore:

This axiom corresponds to reflexivity. This means that there is an arrow from each world to itself (for each agent).

Positive Introspection

Generally assumed of knowledge: everyone knows which things they know. Therefore:

This axiom corresponds to transitivity. A multi-agent model $M=(W,\mathbf R, V)$ is transitive if for every agent $a$ and every three worlds $w_1,w_2,w_3\in W$: if $(w_1,w_2)\in R_a$ and $(w_2,w_3)\in R_a$ then $(w_1,w_3)\in R_a$.

This means that a model is transitive if there are always shortcuts in a chain of three worlds.

Negative Introspection

If and agent $a$ doesn’t know $\phi$, then $a$ knows that they don’t know $\phi$. Therefore:

This corresponds to euclidity. A multi-agent model $M=(W,\mathbf R, V)$ is euclidean if for every agent $a$ and every three worlds $w_1, w_2, w_3\in W$: if $(w_1, w_2)\in R_a$ and $(w_1,w_3)\in R_a$ we then $(w_2,w_3)\in R_a$.

A minimum example of this would look like so:

graph TD
subgraph Euclidean
w1 --> w2
w1 --> w3
w2 --> w3
end
subgraph not euclidean
ww1[w1] --> ww2[w2]
ww1 --> ww3[w3]
end

$S5$

The proof system $S5$ has the following axioms:

• $T$ - All (substitution instances of) validities of propositional logic.
• $K$ - $K_a(\phi\implies\psi)\implies(K_a\phi\implies K_a\psi)$
• $M$ - $K_a\phi\implies\phi$
• $4$ - $K_a\phi\implies K_aK_a\phi$
• $5$ - $\neg K_a\phi\implies K_a\neg K_a\phi$

and the following two rules:

• MP - If you have derived $\phi$ as well as $\phi\implies\psi$, derive $\psi$.
• Necc - If you have derived $\phi$, derive $K_a\phi$.

In epistemic logic we can write $\square$ as $K$ and $\lozenge$ as $M$ to denote we are reasoning about knowledge.

If $\phi$ is derivable in $S5$, we write $\vdash_{s5}\phi$.

Models of Epistemic Logic

We also make the following model restrictions:

A model of epsitemic logic is a triple $M=(W,\mathbf M,V)$ where:

• $W$ is a set of world.
• $\mathbf R={R_a\mid a\in\mathcal A}$
• For every agent $a$, the relation $R_a\subseteq W\times W$ is reflexive, transitive and euclidean.
• $V:\mathcal P\implies 2^W$ is a valuation.

Symmetry

To simplify models of epistemic logic we can make the following assumption:

• A model is reflexive, transitive and euclidean if and only if it is:

  • Reflexive
  • Transitive
  • Symmetric

Symmetric models only use arrows with heads at both ends.

Example Model of Epistemic Logic

In order to simplify drawing a model of epistemic logic we take shortcuts. The following model:

flowchart LR
w1[w1<br>p] <-->|a| w2
w2 <-->|a, b| w3
w1 <-->|a| w3
w2 <-->|b| w4
w3 <-->|b| w4
w1 -->|a, b| w1
w2 -->|a, b| w2
w3 -->|a, b| w3

can be drawn like so in epistemic logic:

graph LR
w1[w1<br>p] ---|a| w2
w2 ---|a, b| w3
w1 ---|a| w3
w2 ---|b| w4
w3 ---|b| w4

We don’t draw:

• Transitive loops.
• Arrowheads, as all are double-ended.

The Meanings of $\square$

Consider the epistemic meaning of $\square$:

I know that $\phi$ is true.

and also the following model:

stateDiagram-v2
direction LR
w1 --> w2:a
w2 --> w1
w2:w2<br>p

From this graph we have:

• $M,w_1\vDash \square_ap$
• $M,w_1\nvDash p$

This is bad as agent $a$ knows something that is false.

We can consider this for all meanings:

Due to the above contradictions, $\square$ doesn’t capture all the properties of those circumstances. As a result we should make the following changes to our logic:

• Add axioms to the proof system.
• Restrict the class of models that are allowed.

Additional Axioms

We can use the following axioms to solve this issue:

There are additional axioms, and related model restrictions, that are required for epistemic logic.

Additional Models

We can give the following restrictions to our model to ensure that the above axioms are complete and sound:

Correspondence

The relation between the axioms and models above is called correspondence:

• $\square_a\phi\implies\phi$ corresponds to reflexivity.

We can define this as so:

An axiom $\psi$ (e.g. $\psi=\square\phi\implies\lozenge\phi$) corresponds to a property $\mathcal C$ (e.g. $\mathcal C=\text{seriality}$) if and only if:

• For every model $M$ that satisfies $\mathcal C$ and every world of that $w$ of that model, we have $M,w\vDash\psi$.
• For every model $M=(W,R,V)$ that does not satisfy $\mathcal C$ there are some alternative valuation $V’$ and some world $w\in W$ such that $(W,R,V’)$, $w\nvDash\psi$.

Importance of Correspondence

A proof system should be sound (everything that can be derived is valid) and complete (everything that is valid can be derived):

• If $\psi$ corresponds to property $\mathcal C$, then $\mathbf K+\psi$ is sound and complete with respect to the models that satisfy $\mathcal C$.

  There are some additional predicates that are required for this to be true that won’t be discussed.

This also works for multiple axioms and properties:

• $\mathbf K +\psi_1+\ldots+\psi_n$ is sound and complete with respect to the models that satisfy $\mathcal C_1,\ldots,\mathcal C_n$

Formula games are formal games between two players:

• The “game board” is the formula.
• The Yes player tries to show that the formula is true.
• The No player tries to show that the formula is false.

There is always a winning strategy for one of the players.

Formula Games for Propositional Logic

Games are defined as so:

• There is a game state: formula $\phi$ and a valuation.
  • So for every atom $p$, it is known whether $p$ is true.
• If $\phi=p$ then one player immediately wins:
  • If $p$ is true then Yes wins.
  • If $p$ is false then No wins.
• If $\phi=\neg\psi$, then the players switch places and continue to play with $\psi$.

• If $\phi=\psi_1\vee\psi_2$ then the Yes player chooses $\psi_1$ or $\psi_2$, the game continues with that formula.

  We want to try and choose the one which we can prove to be true.

• If $\phi=\psi_1\wedge\psi_2$ then the No player choose $\psi_1$ or $\psi_2$, the game continues with that formula.

  We want to try and choose the one which we can prove to be false.

• If $\phi=\psi_1\implies\psi_2$ then the Yes player chooses $\neg\psi_1$ or $\psi_2$, the game continues with this formula.
• If $\phi=\psi_1\iff\psi_2$, then the No player chooses $\psi_1\implies\psi_2$ or $\psi_2\implies\psi_1$, the game continues with that formula.

Example Game 1

Formula: $p\iff (p\wedge q)$
Valuation: $p$ is true, $q$ is false

1. P2 (No): chooses $p\implies(p\wedge q)$
2. P1 (Yes): chooses $\neg p$
3. Players switch places and game continues with $p$.
4. P2 (Yes): $p$ is true to Yes wins.

Player 2 started out as No, and both players played optimally. So $p\iff(p\wedge q)$ was false.

If either player chose the other option then their strategy would be suboptimal and you then can’t use the outcome of the game to determine whether the formula is true.

Formula Game in Modal Logic

A formula game in modal logic is defined like so:

• Game state: a formula $\phi$ and pointed model $M,w$.
• If $\phi=p$, then Yes wins if $w\in V(p)$.
  • No wins if $w\notin V(p)$.
• If $\phi=\square\psi$ then No chooses a successor $w_2$ of $w$. The game continues with $\psi$ and $M,w_2$.
  • If no successor exists, Yes wins.
• If $phi=\lozenge\psi$ then Yes chooses a successor $w_2$ of $w$. The game continues with $\psi$ and $M,w_2$.
  • If no successor exists, No wins.

The rules from propositional logic also apply.

Example Game 2

stateDiagram-v2
direction LR
w1: w1<br>p, q
w2: w2<br>q
w3: w3<br>p
w1 --> w2
w1 --> w3
w2 --> w4
w3 --> w1
w3 --> w4

Game Start: $w_1$
Formula: $\lozenge\square(\square p\vee\lozenge r)$

1. P1 (Yes): chooses successor $w_2$. Game continues on $M,w_2$ with $\square(\square p\vee \lozenge r)$.
2. P2 (No): chooses successor $w_4$ (they have no choice). Game continues on $M,w_4$ with $\square p\vee\lozenge r$.
3. P1 (Yes): chooses $\square p$. Continues on $M,w_4$ with $\square p$.
4. P2 (No): can’t choose a successor. Yes wins.

Both players played optimally, so Yes wins because $M,w_1\vDash\lozenge\square(\square p\vee\square r)$

The proof system $\mathbf K$ has the following axioms:

• $T$ - All the (substitution instances of) validities of propositional logic.
• $\mathbf K$ - $\square(\phi\implies\psi)\implies(\square\phi\implies\square\psi)$.

and the following two rules:

• MP - If you have derived $\phi$ as well as $\phi\implies\psi$, then derive $\psi$.
• Necc - If you have derived $\phi$, then derive $\square\phi$.

We write: if $\phi$ is derivable in $\mathbf K$, we write $\vdash_K\phi$.

Example of a Proof in $\mathbf K$

We want to show: $\vdash_K\square(p\wedge q)\implies\square p$

Reasoning: Allowed because it is obtained from 2 and 3 using the rule MP.

Abbreviations & Conveniences

As $\lozenge\phi$ is an abbreviation for $\neg\square\neg\phi$, we can switch between writing $\lozenge$ and $\neg\square\neg$ at will.

We don’t need a justification to do this.

Additionally, as proofs in $\mathbf K$ tend to contain very long formulas, we can substitute line numbers instead of expressions:

You should keep this to a minimum in order to keep the proof readable.

Soundness & Completeness

The system $\mathbf K$ is well-designed:

• If $\vdash_k\phi$ then $\vDash\phi$
  • So $\mathbf K$ is sound.
• If $\vDash\phi$ then $vdash_K\phi$
  • So $\mathbf K$ is complete.

We don’t have to prove any questions like this in the exam.

Strategies for Finding Proofs in $\mathbf K$

If your expression can’t be proven using an axiom or rule, then the following rules can be helpful:

Suppose you want to show that $\vdash_K\phi$, and that $\phi$ cannot be derived using $T,K$ or Necc. Therefore you must prove $\phi$ using MP.

This means we must:

1. Choose a formula $\psi$
2. Derive $\psi$.
3. Derive $\psi\implies\phi$.

It may help to work backwards in a situation like this.

Completing a lot of examples is the best way to gain an understanding of how to derive $\psi$. However, the following can also help:

• $\psi\implies\phi$ is often an instance of $T$.
• $\psi$ tends to have lots of $\square$ and $\implies$, few $\lozenge$ and $\neg\square$.

Additional Example of a Proof in $\mathbf K$

Show $\vdash_K\lozenge p\implies\lozenge(p\vee q)$:

This is proven in reverse and hence the steps are in reverse. We will have to renumber the table for this to be a valid proof.

Validity in Modal Logic

Like in propositional logic, some formulas are always true. These formulas are valid. We can write this as:

• $\vDash \phi$

Formally we write:

• $\vDash \phi$ if and only if $M,w\vDash \phi$ for every pointed model $M,w$.

Modal Logic Validity Example

Consider the formula:

To prove this is valid we will show that:

We know nothing about $M$ other than it is a model and $w$ is a world of that model. Therefore $M$ is a stand-in for every model.

We can prove this via case distinction:

1. If $M,w\nvDash\square p\wedge\lozenge q$, then $M,w\vDash(\square p\wedge\lozenge q)\implies q$.
2. If $M,w\vDash\square p\wedge\lozenge q$ then:
   1. $M,w\vDash\lozenge q$ so $w$ has some successor $w_2$ such that $M,w_2\vDash q$
   2. $M,w\vDash\square p$, and $w_2$ is a successor of $w$, so $M,w_2\vDash p$.
   3. So $w$ has at least one successor $w_2$ satisfying $p$.
   4. Therefore $M,w\vDash\lozenge p$.

Therefore it follows that $M,w\vDash(\square p\wedge\lozenge q)\implies\lozenge p$ and in either case it is true.

Strategies for Proving Validity

So you want to prove whether $\phi$ is valid. Follow this process:

1. Make a guess.

   This doesn’t have to be right.

2. Act on your guess:

   • If you think that it is valid, take any pointed model $M,w$ and try to show that $M,w\vDash\phi$.
   • If you think that it is not valid, begin drawing a counterexample.

If you get stuck, then change your guess.

Modal Logic Counterexamples

In modal logic, non-valid formulas have a counterexample. If $\nvDash\phi$, then a counterexample is a model $M,w$ such that $M,w\nvDash \phi$.

Modal Logic Counterexample Example

Consider we have the formula:

Counterexample:

stateDiagram-v2
direction LR
w3: w3<br>p
w1 --> w2
w1 --> w3

Therefore we have:

Satisfiability

A formula $\phi$ is satisfiable if there is some $M,w$ such that $M,w\vDash \phi$.

Therefore there is some pointed model in which $\phi$ is true.

Satisfiability & Validity

There is a duality between satisfiability and validity.

• $\phi$ is valid if and only if $\neg\phi$ is not satisfiable.
• $\phi$ is satisfiable if and only if $\neg\phi$ is not valid.

Language of Multi-Agent Modal Logic

Currently we can say $\square\square\phi$ “I know that I know that $\phi$”. If we want to say “I know that you know that $\phi$”, with multiple agents, then we can annotate our boxes to define who knows what.

To define this, we can use the following:

• A set $\mathcal P={p,p_1,\ldots,p_n}$ of propositional atoms.
• A set $\mathcal A={a,b,c,\ldots,a_n,b_n,c_n}$ of agents

Therefore the language of multi-modal logic is:

Multi-Agent Models

These are very similar to single-agent models, however each relation has a label for which agents that relation is valid. We can define this as:

Multi-Agent Model: $M=(W,R,V)$ where:

• $W$ is a set of worlds
• $R={R_a\mid a\in\mathcal A}$
• For every agent $a\in\mathcal A,R_a\subseteq W\times W$ is a relation
• $V$ is a valuation

Example Multi-Agent Model

We can write a multi-agent model like so:

• $W={w_1,w_2,w_3}$
• $R_a={(w_1,w_2),(w_3,w_1)}$
• $R_b={(w_1,w_2),(w_3,w_1),(w_3,w_2)}$
• $V(p)={w_1}$

We should, specify relations for all agents, and the valuation for every atom. If we don’t specify them, they are assumed to be empty.

stateDiagram-v2
direction LR
w1:w1<br>p
w1 --> w2:a
w3 --> w1:a
w1 --> w2:b
w3 --> w1:b
w3 --> w2:b

We can merge the arrows and write the agents in a comma separated list.

Semantics of Multi-Agent Modal Logic

If $M=(M,R,V)$ is a multi-agents model and $w\in R$, then you determine whether $\phi$ holds $M,w$ in the following way:

• $M,w\vDash p$ if and only if $w\in V(p)$
• $M,w\vDash\neg\phi$ if and only if $M,w\nvDash \phi$
• $M,w\vDash\phi_1\wedge\phi_2$ if and only if $M,w\vDash\phi_1$ and $M,w\vDash\phi_2$

• $M,w\vDash\square_a\phi$ if and only if, for every $w_2$ such that $(w,w_2)\in R_a$, we have $M,w_2\vDash\phi$

  The only difference here is that we verify $\square$ and $\lozenge$ only against relations defined by that agent.

If $(w,w_2)\in R_a$ then $w_2$ is called an $a$-successor of $w$.

Therefore $\square_a\phi$ holds in $w$ if and only if $\phi$ holds in every $a$-successor of $w$.

A possible world is a description of a possible state of the universe, or at least those parts of the universe that we care about.

Possible Worlds Simple Example

Suppose we only care about whether it is currently raining in Liverpool. Then there are two possible worlds:

• $w_1$ it is raining
• $w_2$ it is not raining

We can relate this to a truth formula:

Let $p=\text{it is raining}$
Then: $p$ is true on $w_1$, false on $w_2$

We can also draw this in a graph:

Say that we are in a box and we can’t see the weather. If it is raining or not, we can’t tell the difference. Therefore, you could be in either world:

stateDiagram-v2
direction LR
w1:p<br>w1
w1 --> w2
w2 --> w1
w2 --> w2
w1 --> w1

• Arrows define possibility dependant on observation.

Possible Worlds Model

A model $M$ is a triple $M=(W,R,V)$ where:

• $W$ is a set of possible worlds.
• $R\subseteq W\times W$ is a relation on $W$
  • $R$ is a set of pairs $(w_1,w_2)$ where $w_1$ and $w_2$ are in $W$.
• $V:\mathcal P\implies 2^W$ is a valuation
  • For ever $p\in\mathcal P$, $V(p)$ is the set of worlds where $p$ is true.

Drawing a Model

• $W={w_1,w_2,w_3}$
• $R={(w_1,w_2), (w_2,w_3),(w_3,w_2),(w_3,w_1)}$
• $V(p)={w_1}$, $V(q)={w_1,w_2}$

stateDiagram-v2
direction LR
w1: w1<br>p,q
w2: w2<br>q
w1 --> w2
w2 --> w3
w3 --> w1

Worlds where $p$ and $q$ are not true are implicitly labeled with $\neg p$ and $\neg q$

Semantics of Modal Logic

Modal logic is evaluated with respect to a pointed model:

• A pointed model is a pair $M,w$ where $w$ is a world view of $M$.

We can use the following notation:

• $M,w\vDash\phi$ if $\phi$ is true in $M,w$.

A modal logic formula $\phi$ is valid (denoted $\vDash\phi$) if $M,w\vDash\phi$ for every pointed model $M,w$.

Determining Validity

If $M=(W,R,V)$ is a model and $w\in W$, then you determine whether $\phi$ holds in $M,w$ in the following way:

• $M,w\vDash p$ if and only if $w\in V(p)$
• $M,w\vDash\neg\phi$ if and only if $M,w\nvDash\phi$
• $M,w\vDash\phi_1\wedge\phi_2$ if and only if $M,w\vDash\phi_1$ and $M,w\vDash\phi_2$
• $M,w\vDash\square\phi$ if and only if, for every $w_2$ such that $(w,w_2)\in R$, we have $M,w_2\vDash\phi$

If $(w,w_2)\in R$ then $w_2$ is called a successor of $w$.

If there is an arrow from one world to another in a graph then the second is the successor of the first.

Therefore, $\square\phi$ holds in $w$ if and only if $\phi$ holds in every successor of $w$.

Validity Example

Consider we have the following model:

stateDiagram-v2
direction LR
w1:p<br>w1
w2:¬p<br>w2
w1 --> w2
w2 --> w1
w2 --> w2
w1 --> w1

We can define the model $M=(W,R,V)$ as:

• $W={w_1, w_2}$
• $R={(w_1,w_1), (w_1,w_2),(w_2,w_1),(w_2,w_2)}$
• $V(p)={w_1}$

From this we can evaluate the following expressions:

• $M,w_1\vDash p$
  • True, as $w_1$ is in the set where $p$ is true.
• $M,w_2\vDash p$
  • False, as $p$ is not true in $w_2$.
• $M,w_1\vDash\square p$
  • False, as $w_2$ is a successor of $w_1$ and $p$ doesn’t hold there.

Semantics of $\lozenge$

$\lozenge$ is an abbreviation for $\neg\square\neg$. Therefore:

• $M,w\vDash\lozenge\phi$ if and only if $M,w\vDash\neg\square\neg\phi$

We can write this as:

$M,w\vDash\lozenge\phi$ if and only if there is some successor $w_2$ of $w_1$ such that $M,w_2\vDash\phi$.

Successor Trick Question

Consider the following model:

stateDiagram-v2
w1

• $M,w_1\vDash\square p$
  • True, as every successor of $w_1$ satisfies $p$. Even if there are none of them
• $M,w_1\vDash\lozenge p$
  • False, as there is not at least one successor of $w_1$ that satisfies $p$.

Possible World Semantic Example

Consider we have the following model:

stateDiagram-v2
direction LR
w3: w3<br>q
w1 --> w1
w1 --> w3
w3 --> w3
w3 --> w2
w2 --> w4

$M,w_3\nvDash\square\lozenge\lozenge\top$ (does $\square\lozenge\lozenge\top$ hold in $w_3$)?

We can complete the following checks to verify this:

graph TD
1["M,w3⊭□◊◊⊤"] --> 2 & 3
2["M,w3⊨◊◊⊤"] --> 4 & 5
3["M,w2⊭◊◊⊤"] --> 6
4["M,w3⊨◊⊤"] --> 7 & 8
5["M,w2⊨◊⊤"] --> 9
6["M,w4⊭◊⊤"]
7["M,w3⊨⊤"]
8["M,w2⊨⊤"]
9["M,w4⊨⊤"]

As $w_4$ has no successors $M,w_4\vDash\lozenge\top$ is false. This results in the original expression evaluating to false as not every successor is true.

Truth-Functionality

The connectives of propositional logic are truth-functional:

• This means that the truth of $\phi\wedge\psi$ is fully determined by the truth of $\phi$ and $\psi$.

If a proposition is not truth-functional we can describe it like so:

We are not sure whether $\phi$ will continue to be true.

Language of Modal Logic

In modal logic we have an extra unary connective:

$\lozenge\phi$ is an abbreviation for $\neg\square\neg\phi$.

The Meaning of $\square$

$\square \phi$ has many meanings depending on the circumstance:

The Meaning of $\lozenge$

$\lozenge \phi$ has many meanings depending on the circumstance:

Converting Language to Modal Logic

Modal Logic to English Examples

• Temporal: $\square\lozenge p$:
  • At every point in the future, $p$ will be true some late time.
• Deontic: $\square p\implies\lozenge p$:
  • If $p$ is mandatory then it is also permitted.
• Legal: $\neg\lozenge\square\neg p$:
  • It is not permitted to forbid $p$.
• Epistemic: $\square p\implies\square\square p$:
  • If I know $p$, then I know that I know $p$.

English to Modal Logic Examples

• “I know that Today is Thursday”:
  • $p=\text{today is Thursday}$
  • $\square p$
• “If it it legal to walk here then is it legal to stand here”:
  • $p=\text{walk here}$
  • $q=\text{stand here}$
  • $\lozenge p\implies\lozenge q$

There are also quotes which can be parsed multiple ways:

• “I know that it is Monday or it is Tuesday”:
  • $\square p\vee q$
• “I know that it is Monday or it is Tuesday”:
  • $\square (p\vee q)$

When translating an ambiguous sentence to logic, choose a disambiguation. All disambiguations will be acceptable in the exam.

Language

This is what defines a well formed formula (wff) in a particular logic.

We start with a set $\mathcal P$ of atoms, $\mathcal P = p, q, p_1, p_2,\ldots$

These represent basic facts that we don’t analyse further.

The atoms determine the level of detail that we consider.

Well Formed Formulas

• Every $p\in \mathcal P$ is a wff.
• If $\phi$ and $\psi$ are wffs, then $\neg\phi,(\phi\wedge\psi),(\phi\vee\psi), (\phi\implies\psi),(\phi\iff\psi)$
  • Each wff includes these brackets.
  • Negation binds stronger than other connectives as it is unary.
• We can omit brackets if this does not cause ambiguity.

Symbols

Semantics

Not $\neg$

Or & And $\vee, \wedge$

Implies $\implies$

If and Only If $\iff$

Validity

Contingent Formulas

This is the case if you can change whether a formula is true or false by changing the inputs.

Valid Formulas $\vDash\phi$

Formulas where only true is returned, no matter the input.

You can also write this as $\emptyset\vDash\phi$.

Valid Inference ${p,q}\vDash p\wedge q$

This is where a set of premises guarantee the truth of the conclusion.

Truth Tables

To find whether an inference is true then we can draw a truth table for all the premises:

${p,p\implies q}\vdash q$

We can then use the table to prove by example/counterexample.

Proof System

Axioms of Propositional Logic

Derivation

You can use the following justifications to form your derivation:

• It is a premise.
• It is an instance of an axiom.

• If we have derived $\phi$ and $\phi\implies\psi$ then we can use $\psi$.

  This is the rule MP.

By combining our derivations (MP) and the axioms we can create a proof system $\mathfrak P$

Proof Example

$\Gamma\vdash_\mathfrak P\phi$ if $\phi$ can be derived $\Gamma$ in $\mathfrak P$.

For example we can prove the commutativity of $\wedge$:

Soundness and Completeness

• If $\Gamma\vdash_\mathfrak P \phi$, then $\Gamma\vDash\phi$. So we can only derive valid inferences.
  • This is called soundness.
• If $\Gamma\vDash\phi$, then $\Gamma\vdash_\mathfrak P\phi$. So every valid inference can be derived.
  • This is called completeness.

A proof system is only considered useful if it is sound and complete.

This is to say we want our proof system $\mathfrak P$ to be complete and inline with the logics of mathematics.

Abbreviations

$\bot$ and $\top$

• $\top$ represents something that is always true (such as $p\vee\neg p$)
• $\bot$ represents something that is always false (such as $p\wedge\neg p$)

$\wedge$, $\implies$ and $\iff$

We can also define some of our connectives as abbreviations:

• $\phi\wedge\psi$ can abbreviate $\neg(\neg\psi\vee\neg\psi)$
• $\phi\implies\psi$ can abbreviate $\neg\phi\vee\psi$
• $\phi\iff\psi$ can abbreviate $(\phi\implies\psi)\wedge(\phi\implies\psi)$

Language Definition

As we can abbreviate our original atoms: $\neg,\vee,\wedge,\implies,\iff$ we can redefine the language of propositional logic as: