Transcript Lectures 12 to 14: Soundness and completeness

CS344 : Introduction to Artificial
Intelligence
Pushpak Bhattacharyya
CSE Dept.,
IIT Bombay
Lecture 12, 13, 14- Soundness and Completeness;
proof of soundness; start of proof of completeness
Week of 2/2/09
Soundness, Completeness &
Consistency
Soundness
Semantic
World
----------
Syntactic
World
---------Theorems,
Proofs
*
Valuation,
Tautology
Completeness
*

Soundness


Provability
Truth
Completeness

Truth
Provability

Soundness:


Proved entities are indeed true/valid
Completeness:

Correctness of the System
Power of the System
True things are indeed provable
System
TRUE
Expression
s
Validation
Outside
Knowledge
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
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
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
Syntactic ‘false
Semantic ‘false’
Where F is called ‘false’ and is one of the two
symbols (T, F)
V(F ) = F
V(AB) is defined through what is called the
truth table
V(A)
T
T
F
F
V(B)
F
T
F
T
V(AB)
F
T
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
Soundness
Completeness
FP is a tautology
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
Form
(Content)
Form & Content
painter
logician
musician
Godel, Escher, Bach
By D. Hofstadter
Problem
(P
Q)(P
Q)
A
B
Semantic Proof
P
T
T
F
F
Q
F
T
F
T
P
Q
F
T
F
F
P
Q
T
T
F
T
AB
T
T
T
T
To show syntactically
(P Q) (P
i.e.
[(P
(Q
F ))
Q)
F ]
[(P
F )
Q]
If we can establish
(P
(Q
F ))
F,
(P
F ), Q
This is shown as
Q
F hypothesis
(Q F ) (P (Q
F ⊢F
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 Proof
Hilbert Formalization of Propositional
Calculus is sound.
“Whatever is provable is valid”
Statement
Given
A1, A2, … ,An + B
V(B) is ‘T’ for all Vs for which V(Ai) = T
Proof
Case 1 B is an axiom
V(B) = T by actual observation
Statement is correct
Case 2
B is one of Ais
if V(Ai) = T, so is V(B)
statement is correct
Case 3
.
.
.
Ei
.
.
.
Ej
.
.
.
B
B is the result of MP on Ei & Ej
Ei is Ei
B
Suppose V(B) = F
Then either V(Ei) = F or V(Ej) = F
i.e. Ei/Ej 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:

Correctness of the System
Power of the System
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.
2.
3.
4.
p, ~q |- p(p V q)
p, q |- p(p V q)
~p, q |- p(p V q)
~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 P1, P2, …, Pn are constituent propositions of
A
and if V(A) = T for every model V(Pi) = T/F
then
|- A
We have a truth table with 2n rows
P1
F
F
P2
F
F
P3
F
F
T
T
T
. . .
. . .
. . .
.
.
.
. . .
Pn
F
T
A
T
T
T
T
If we can show
P1’, P2’, …, Pn’ |- A’
For every row where
Pi’ = Pi if V(Pi) = T
= ~Pi if V(Pi) = F
And A’ = A if V(A) = T
= ~A if V(A) = F
Lemma
If row has
P1’, P2’, …, Pn’, A’
Then
P1’, P2’, …, Pn’ |- A’
A very critical result linking syntax with
semantics