Pushpak Bhattacharyya

CS344: Introduction to Artificial Intelligence

(associated lab: CS386)

Pushpak Bhattacharyya

CSE Dept., IIT Bombay

Lecture–15, 17, 19, 20: Foundations: Axiom, Rule, Concept, Soundness, Completeness, Consistency, Derivability

3^rd, 7^th , 19^th and 21^st March, 2014

(Lecture 13 and 14 were on Logic by Brendan; lecture 16 and 18 were on HMM by Manish )

Theory of CS



Theory A

 Logic



Theory B

 Algorithm an Complexity

Concepts, Axioms, Rule

 Some foundational questions for

Mechanization or Automation of Knowledge Representation and Reasoning:

 What are symbols and concepts (well formed formulae)

 What are the self evident and ground truths in the system (axiomatization)

 What is the validity of the inference (soundness and consistency)

 Is the inference system powerful enough to capture reality (completeness)

 Can it be implemented in Turing machine (derivability and complexity)

Case study: Propositional calculus

Propositions

− Stand for facts/assertions

− Declarative statements

− As opposed to interrogative statements (questions) or imperative statements (request, order)

Operators

AND (/\), OR (\/), NOT (¬), IMPLICATION (=>)

=> and ¬ form a minimal set (can express other operations) - Prove it.

Tautologies are formulae whose truth value is always T, whatever the assignment is

Model

In propositional calculus any formula with n propositions has 2ⁿ models (assignments)

- Tautologies evaluate to T in all models.

Examples:

1)

2)

-e Morgan with AND

P P  

) (

)

(P  Q  P  Q



Example



Prove is a Tautology.



Proof by Truth Table

T T F F T

T F T T T

F T T T T

F F T T T

)

~ (~

) (

~ PQ  P Q

) (

~ P Q

L  

P

Q R ~ P ~ Q ^L  ^R

Formal Systems

 Rule governed

 Strict description of structure and rule application

 Constituents

 Symbols

 Well formed formulae

 Inference rules

 Assignment of semantics

 Notion of proof

 Notion of soundness, completeness, consistency, decidability etc.

Hilbert's formalization of propositional calculus 1. Elements are propositions : Capital letters

2. Operator is only one :  (called implies) 3. Special symbol F (called 'false')

4. Two other symbols : '(' and ')'

5. Well formed formula is constructed according to the grammar WFF P|F|WFFWFF

6. Inference rule : only one Given AB and

A

write B

known as MODUS PONENS

7. Axioms : Starting structures A1:

A2:

A3

This formal system defines the propositional calculus ))

(

(A  B  A

))) (

) ((

)) (

((A  B  C  A  B  A  C )

) )

(((A  F  F  A

Notion of proof

1. Sequence of well formed formulae 2. Start with a set of hypotheses

3. The expression to be proved should be the last line in the sequence

4. Each intermediate expression is either one of the hypotheses or one of the axioms or the result of modus ponens

5. An expression which is proved only from the axioms and inference rules is called a THEOREM within the system

Example of proof

From P and and prove R H1: P

H2:

H3:

i) P H1

ii) H2

iii) Q MP, (i), (ii)

iv) H3

v) R MP, (iii), (iv)

Q P 

Q P 

Q P 

R Q 

R Q 

R Q 

Prove that is a THEOREM

i) A1 : P for A and B

ii) A1: P for A and for B

iii)

A2: with P for A, for B and P for C

iv) MP, (ii), (iii)

v) MP, (i), (iv)

) (P  P

) )

((P P P

P   

)

(P P

P  

))]

( ))

( ((

)) )

((

[(P  P  P  P  P  P  P  P  P

) (P  P ))

( )

(

(P  P  P  P  P )

(P  P

) (P  P

Shorthand

1. is written as and called 'NOT P'

2. is written as and called 'P OR Q’

3. is written as and called

'P AND Q' Exercise: (Challenge) - Prove that

¬P P  F

) )

((P  F Q ^(PQ)

) ))

(

((P  Q  F  F (P Q)

)) (

( A

A   

A very useful theorem (Actually a meta theorem, called deduction theorem)

Statement If

A₁, A₂, A₃ ... A_n ├ B then

A₁, A₂, A₃, ...A_n-1├

├ is read as 'derives' Given

A₁ A₂ A₃ . . . . A_n

B Picture 1

A₁ A₂ A₃ . . . . A_n-1

Picture 2 B

A_n 

B A_n 

Use of Deduction Theorem Prove

i.e.,

├ F (M.P)

A├ (D.T)

├ (D.T)

Very difficult to prove from first principles, i.e., using axioms and inference rules only

)) (

( A

A   

) )

((A F F

A   

F A

A, 

F F

A  )  (

) )

((A F F

A  

Prove i.e.

├ F

├ (D.T)

├ Q (M.P with A3)

P├

├

) (P Q

P  

) )

((P F Q

P   

F Q

F P

P,  , 

F P

P,  ^{(Q  F)  F}

Q F

P  )  (

) )

((P F Q

P   

More proofs

) )

((

) (

. 3

) (

) (

. 2

) (

) (

. 1

Q P

Q Q

P

P Q

Q P

Q P

Q P



























Important to note



Deduction Theorem is a meta-theorem (statement about the system)



P  P is a theorem (statement belonging to the system)



The distinction is crucial in AI



Self reference, diagonalization



Foundation of Halting Theorem, Godel

Theorem etc.

Example of ‘of-about’

confusion



“This statement is false”



Truth of falsity cannot be decided

Soundness, Completeness &

Consistency

Syntactic World ---

Theorems, Proofs

Semantic World ---

Valuation, Tautology

Soundness

Completeness

* *



Soundness

 Provability Truth



Completeness

 Truth Provability



Soundness:

 Proved entities are indeed true/valid



Completeness:

 True things are indeed provable

TRUE Expression

s System

Outside Knowledge Validation

Consistency

The System should not be able to prove both P and ~P, i.e., should not be able to derive

F

Examine the relation between Soundness

&

Consistency

Soundness Consistency

If a System is inconsistent, i.e., can derive F , it can prove any expression to be a

theorem. Because

F  P is a theorem

InconsistencyUnsoundness

To show that

FP is a theorem

Observe that

F, PF ⊢ F By D.T.

F ⊢ (PF)F; A3

⊢ P

i.e. ⊢ FP

Thus, inconsistency implies unsoundness

UnsoundnessInconsistency

 Suppose we make the Hilbert System of

propositional calculus unsound by introducing (A /\ B) as an axiom

 Now AND can be written as

 (A(BF )) F

 If we assign F to A, we have

 (F (BF )) F

 But (F (BF )) is an axiom (A1)

 Hence F is derived

Inconsistency is a Serious issue.

Informal Statement of Godel Theorem:

If a sufficiently powerful system is complete it is inconsistent.

Sufficiently powerful: Can capture at least

Peano Arithmetic

Introduce Semantics in Propositional logic

Valuation Function V Definition of V

V(F ) = F

Where F is called ‘false’ and is one of the two symbols (T, F)

Semantic ‘false’

Syntactic ‘false

V(F ) = F

V(AB) is defined through what is called the truth table

V(A) V(B) V(AB)

T F F

T T T

F F T

F T T

Tautology

An expression ‘E’ is a tautology if V(E) = T

for all valuations of constituent propositions Each ‘valuation’ is called a ‘model’.

To see that

(FP) is a tautology two models

V(P) = T V(P) = F V(FP) = T for both

F P is a theorem

F P is a tautology

Soundness Completeness

If a system is Sound & Complete, it does not matter how you “Prove” or “show the validity”

Take the Syntactic Path or the Semantic Path

Syntax vs. Semantics issue

Refers to

FORM VS. CONTENT

Tea

(Content) Form

Form & Content

Godel, Escher, Bach

By D. Hofstadter

logician

painter

musician

Problem

(P Q)(P Q)

Semantic Proof

A B

P Q P Q P Q AB

T F F T T

T T T T T

F F F F T

F T F T T

To show syntactically

(P Q) (P Q)

i.e.

[(P (Q F )) F ]

[(P F ) Q]

If we can establish (P (Q F )) F ,

(P F ), Q F ⊢ F This is shown as

Q F hypothesis

(Q F ) (P (Q F)) A1

QF; hypothesis

(QF)(P(QF)); A1 P(QF); MP

F; MP

Thus we have a proof of the line we

started with

Soundness and Completeness

proofs

Soundness, Completeness &

Consistency

Syntactic World ---

Theorems, Proofs

Semantic World ---

Valuation, Tautology

Soundness

Completeness

* *

Introduce Semantics in Propositional logic

Valuation Function V Definition of V

V(F ) = F

Where F is called ‘false’ and is one of the two symbols (T, F)

Semantic ‘false’

Syntactic ‘false

V(F ) = F

V(AB) is defined through what is called the truth table

V(A) V(B) V(AB)

T F F

T T T

F F T

F T T

Tautology

An expression ‘E’ is a tautology if V(E) = T

for all valuations of constituent propositions Each ‘valuation’ is called a ‘model’.



Soundness

 Provability Validity



Completeness

 Validity Provability



Soundness:

 Proved entities are indeed valid



Completeness:

 Valid things are indeed provable

Consistency

The System should not be able to prove both P and ~P, i.e., should not be able to derive

F

Examine the relation between Soundness

&

Consistency

Soundness Consistency

If a System is inconsistent, i.e., can derive F , it can prove any expression to be a

theorem. Because

F  P is a theorem

If a system is Sound & Complete, it does not matter how you “Prove” or “show the validity”

Take the Syntactic Path or the Semantic Path

Soundness Proof

Hilbert Formalization of Propositional Calculus is sound.

“Whatever is provable is valid”

Any statement in propositional calculus can be written as

(A

 (A

 (A

 …(A

 B)…) Because,

WFF  F ^{| P | (WFF}  WFF) Statement

Given

A

, A

, … ,A

|- B

V(B) is ‘T’ for all V

for which V(A

) = T

Proof

Case 1 B is an axiom

V(B) = T by actual observation

Statement is correct

Case 2 B is one of A

if V(A

) = T, so is V(B)

statement is correct

Case 3 B is the result of MP on E_i & E_j E_j is E_i B

Suppose V(B) = F

Then either V(E_i) = F or V(E_j) = F

. . . E_i

. . . E_j

. . . B

i.e. E_i/E_j is result of MP of two expressions coming before them

Thus we progressively deal with shorter and shorter proof body.

Ultimately we hit an axiom/hypothesis.

Hence V(B) = T

Soundness proved

Towards Completeness Proof



Soundness:

 Proved entities are indeed true/valid



Completeness:

 True things are indeed provable

Tautology

An expression ‘E’ is a tautology if V(E) = T

for all valuations of constituent propositions Each ‘valuation’ is called a ‘model’.

Necessary results

Statement: (pq)((~pq)q) Proof:

If we can show that (pq), (~pq) |- q Or,

(pq), (~pq), qF |- F Then we are done.

Proof continued

1. (pq) H1 2. (~pq) H2 3. qF H3

4. (~pq) (~qp) theorem of contraposition 5. ~qp MP, 2, 4

6. P MP, 3,5 7. q MP, 6, 1 8. F MP,7,3 QED

How to prove contraposition

To show

(p  q)  (~q  ~p) Proof:

p  q, ~q, p |- F

Very obvious!

An example to illustrate the completeness proof

p q p(p V q)

T F T

T T T

F T T

F F T

Running the completeness proof

For every row of the truth table set up a proof:

1.

p, ~q |- p  (p V q)

2.

p, q |- p  (p V q)

3.

~p, q |- p  (p V q)

4.

~p, ~q |- p  (p V q)

1. p, ~q |- p  (p V q) i.e. p, ~q, p |- p V q p, ~q, p, ~p |- q

p, ~q, p, ~p |- F

|- F  q

|- q

2.

p, q |- p  (p V q)

i.e. p, q, p, ~p |- q

same as 1

3.

~p, q |- p  (p V q)

~p, q, p, ~p |- q

Same as 1, since F is derived 4. ~p, ~q |- p  (p V q)

Same as 1, since F is derived

Why all this?

If we have shown p, q |- A

and p, ~q |- A

then we can show that p |- A

p |- (q  A) also p |- (~q  A)

But (q  A)  ((~q  A)  A)

is a theorem by MP twice

p |- A

General Statement of the completeness proof

If V(A) = T for all models then

|- A

Elaborating,

If P₁, P₂, …, P_n are constituent propositions of A

and if V(A) = T for every model V(P_i) = T/F then

|- A

We have a truth table with 2ⁿ rows P₁ P₂ P₃ . . . P_n A F F F . . . F T F F F . . . T T

. . .

T T T . . . T T

If we can show

P₁’, P₂’, …, P_n’ |- A’

For every row where

P_i’ = P_i if V(P_i) = T

= ~P_i if V(P_i) = F And A’ = A if V(A) = T

= ~A if V(A) = F

If row has

P

’, P

’, …, P

’, A’

Then

P

’, P

’, …, P

’ |- A’

A very critical result linking syntax with semantics

Lemma

Completeness Proof

P₁ P₂ P₃ . . . P_n A F F F . . . F T F F F . . . T T

. . .

T T T . . . T T

We have a truth table with 2

rows

We should show

P₁’, P₂’, …, P_n’ |- A’

For every row where

P_i’ = P_i if V(P_i) = T

= ~P_i if V(P_i) = F And A’ = A if V(A) = T

= ~A if V(A) = F

Completeness of Propositional Calculus



Statement

If V(A) = T for all V,

then |--A i.e. A is a theorem.



Lemma:

If A consists of propositions P

, P

, …, P

then P’

, P’

, …, P’

|-- A’, where

A’ = A if V(A) = true

= ~A otherwise

Similarly for each P’

Proof for Lemma

Proof by induction on the number of ‘→’

symbols in A

Basis: Number of ‘→’ symbols is zero.

A is ℱ or P. This is true as, |-- (A → A) i.e. A → A is a theorem.

Hypothesis: Let the lemma be true for number of ‘→’ symbols ≤ n.

Induction: Let A which is B → C, contain n+1

‘→’

 Induction:

By hypothesis,

P’₁, P’₂, …, P’_n |-- B’

P’₁, P’₂, …, P’_n |-- C’

If we show that B’, C’ |-- A’ (A is B → C), then the proof is complete.

For this we have to show:

• B, C |-- B → C

True as B, C, B |-- C

• B, ~C |-- ~(B → C)

True since B, ~C, B → C |-- ℱ

• ~B, C |-- B → C

True since ~B, C, B |-- C

• ~B, ~C |-- B → C

True since ~B, ~C, B, C → ℱ |-- ℱ

 Hence the lemma is proved.

Proof of Lemma (contd.)

Proof of Theorem

 A is a tautology.

 There are 2ⁿ models corresponding to P₁, P₂, …, P_n propositions.

 Consider,

P₁, P₂, …, P_n |-- A and P₁, P₂, …, ~P_n |-- A

P₁, P₂, …, P_n-1 |-- P_n → A and P₁, P₂, …, P_n-1 |-- ~P_n → A

RHS can be written as:

|-- ((P_n → A) → ((~P_n → A) → A))

|-- (~P_n → A) → A

|-- A

 Thus dropping the propositions progressively we show |-- A