Soundness and Completeness - Cognitive Science Department

Download Report

Transcript Soundness and Completeness - Cognitive Science Department

Formalizing Alpha:
Soundness and Completeness
Bram van Heuveln
Dept. of Cognitive Science
RPI
Overview
• This presentation discusses:
–
–
–
–
Formal Syntax of Alpha
Formal Semantics of Alpha
Soundness of Alpha
Completeness of Alpha
Formalizing Alpha
Formal Syntax
Alpha Graphs are recursively defined as follows:
1.
2.
is an Alpha Graph.
P
is an Alpha Graph, with P an atomic statement.
3.   is an Alpha Graph, with  and  Alpha Graphs.
4.

is an Alpha Graph, with  an Alpha Graph.
Formalizing Alpha
Formal Semantics
A truth-assignment h is a function that assigns either True
or False to any Alpha Graph in accordance with:
1. h(
2. h(
) = True.
P
) = True or False.
3. h(   ) = True iff h(  ) = True and h(  ) = True.
4. h(

) = True iff is h(  ) = False.
Formalizing Alpha
Consequence
• Let us use the following notation:
– h |=  iff h() = True
– |=  iff for any truth-assignment h: h |= 
• Let us define:
–  is a truth-functional consequence of  iff for any
truth-assignment h: if h |=  then h |= .
Formalizing Alpha
Soundness and Completeness
• Let us use the symbol TF to indicate truthfunctional consequence:
–  TF  iff  is a truth-functional consequence of .
• Let us use the symbol EG to indicate truthfunctional provability in Alpha:
–  EG  iff there exists a formal proof from  to .
• We will show two things:
– Alpha is truth-functionally sound:
• For any  and  : if  EG  then  TF 
– Alpha is truth-functionally complete:
• For any  and  : if  TF  then  EG 
Soundness
Proving Soundness
• A straightforward way to demonstrate the soundness of
some system S is to demonstrate that each of the inference
rules of S is sound.
• If the inference rules deal with subproofs, such a proof can
actually become rather technical, even if the soundness of
each inference rules is intuitive clear (see e.g. proof of
soundness of F in “Language, Proof, and Logic”).
• The good news is that Alpha does not deal with subproofs.
• However, the bad news is that, except for double cut, the
soundness of Alpha’s inference rules is not intuitive.
• To make the soundness of the inference rules more
intuitive, we use the notion of a recursive conditional
reading as well as 3 less commonly used inference rules.
Soundness
2 Rules of Inference and 1 Rule of Equivalence
Strengthening the
Antecedent
pr

(p  q)  r
Absorption Case 1
Weakening the
Consequent
p  (q  r)

pr
Absorption Case 2
p and q  r

p and (q  p)  r
p and q  r

p and q  (r  p)
Soundness
Recursive Conditional Reading
One can see graphs with multiple cuts inside each other as
expressing recursively conditioned conditionals. For example:
P
Q
R
S
This graph can be read as: ‘if P is true then Q is true, but if P is
true, then it is also true that if R is true then S true’. Hence the
conditional ‘if R then S’ is conditionally true. Thus, as more
and more conditions get added, the truth of more and more
statements can be asserted.
Soundness
Relative Recursive Conditional Reading I
0
1 

2k-1
2k
Relative to any subgraph  existing at an odd level 2k-1,
one can see the graph as a whole in the above manner (note:
if there is no cut next to  , then one has to add an empty
double cut next to  to make it work).
Soundness
Relative Recursive Conditional Reading II
0
1 

2k-1
2k
The Recursive Conditional Reading (RCR) of a graph relative to
a subgraph  existing at odd level 2k – 1 is defined as follows:
0 &
 1  2 &
(1  3)  4

(1    2k-1  )  2k
Soundness
Relative Recursive Conditional Reading III
0
1 
2k-1

2k
Relative to any subgraph  existing at an even level 2k, one
can see the graph as a whole in the above manner.
Soundness
Relative Recursive Conditional Reading IV
0
1 
2k-1

2k
The Recursive Conditional Reading (RCR) of a graph relative to
a subgraph  existing at even level 2k is defined as follows:
0 &
 1  2 &
(1  3)  4

(1    2k-1)  2k  
Soundness
Soundness of Insertion
0
1 
2k-1
2k
0 &
1  2 &

(1    2k-1)  2k

? IN
0
1 

2k-1
2k
pr

(p  q)  r
0 &
1  2 &

(1    2k-1  )  2k
Insertion corresponds to Strengthening the Antecedent
Soundness
Soundness of Erasure
0
1 
2k-1

2k
0 &
1  2 &

(1    2k-1)  (2k  )

? E
0
1 
2k-1
2k
p  (q  r)

pr
0 &
1  2 &

(1    2k-1)  2k
Erasure corresponds to Weakening the Consequent
Soundness
Soundness of Iteration/Deiteration
 

? IT/DE
 


• To demonstrate the
  soundness of iteration
and deiteration, it
suffices to demonstrate
that the subgraph that
has the original at level
0 is equivalent to the
corresponding
  subgraph in the result
of the iteration or
deiteration.
Soundness
Soundness of Iteration/Deiteration Case 1

1 
2k-1
2k
&
1  2 &

(1    2k-1)  2k

? IT/DE

1 

2k-1
2k
p and q  r

p and (q  p)  r
&
1  2 &

(1    2k-1  )  2k
Iteration/Deiteration (Case 1) corresponds to Absorption (Case 1)
Soundness
Soundness of Iteration/Deiteration Case 2

1 
2k-1
2k
&
1  2 &

(1    2k-1)  2k

? IT/DE

1 
2k-1

2k
p and q  r

p and q  (r  p)
&
1  2 &

(1    2k-1)  (2k  )
Iteration/Deiteration (Case 2) corresponds to Absorption (Case 2)
Completeness
Proving Completeness
• On the next slides, we will provide a direct proof
of the completeness of Alpha that very much
follows the strategy used in “Language, Proof, and
Logic” to prove that system F is complete.
Completeness
Alpha Consistency and Alpha Completeness
A graph  is Alpha inconsistent iff
 EG
A graph  is Alpha complete iff for any graph :
 EG  or  EG 
Completeness
Either-Or Lemma
For any graph : if  is Alpha consistent and
Alpha complete, then for any graph :
 EG  or  EG 
but not both  EG  and  EG 
Proof: Suppose  is Alpha consistent and Alpha complete. Then:
By Alpha completeness:  EG  or  EG 
Now suppose  EG  and  EG  . Then:
    EG    

i.e.  is Alpha inconsistent.
Contradiction, so not both  EG  and  EG 
Completeness
Deduction Theorem
For any graphs  and :
 EG 
iff
EG


Proof:
‘if’:
 EG 


 



‘only if’:






EG 

Completeness
Transposition Lemma
For any graphs  and :
 EG 

iff
EG 
Proof:
‘only if’:
So:
‘if’:
Suppose  EG . Then (Ded. Thm.): EG

Suppose
So:  
EG 


 


EG  . Then (‘only if’):

EG 
 





EG 
Completeness
Expansion Theorem
For any graph : if  is Alpha consistent, then there exists a
’ =   for some  such that ’ is Alpha consistent and
Alpha complete.
Proof: Obtain ’ from the following routine:
As = Set of all atomic statements
While As  :
Select and remove some A from As

if  EG A or  EG A
’ =
 A otherwise
{
 = ’
Next two slides: ’ is Alpha consistent and Alpha complete.
Completeness
Expansion Theorem (Alpha Consistency of ’)
To prove: ’ as obtained by the routine is Alpha consistent.
Proof: By induction we’ll show that at any point ’ is Alpha consistent
Base:  is Alpha consistent
Step: Suppose  is Alpha consistent, and suppose that adding A  As
to  makes ’ =  A Alpha inconsistent, i.e:  A EG
Then:
A
  A EG
So (Transposition Theorem): EG  A 
Hence (Ded. Thm):  EG A

A
So, A would not be added to .
Contradiction, so adding A keeps  Alpha consistent.
Completeness
Expansion Theorem (Alpha Completeness of ’)
To prove: ’ as obtained by the routine is Alpha complete.
Proof: By induction on the composition of any statement .
Base: For every atomic statement A, ’ EG A or ’ EG A
Step: Case 1:  = 1 2
By inductive assumption: ’ EG i or ’ EG i
If ’ EG 1 and ’ EG 2 then ’  ’ ’ EG 1 2
If ’ EG 1 or ’ EG 2 then ’  EG 1 2 by IN
Case 2:  = ’
By inductive assumption: ’ EG ’ or ’ EG ’
Hence, ’ EG ’  ’   or ’ EG 
Completeness
Consistency Lemma
For any graph : if  is Alpha consistent and Alpha complete,
then  is consistent.
Proof: Suppose  is Alpha consistent and Alpha complete.
Define truth-value assignment h as follows:
For any atomic statement A: h(A) = True iff  EG A
(the Either-Or Lemma guarantees that h is well-defined).
On the next slide we’ll show that for any graph :
h() = True iff  EG 
Finally, because  EG , h() = True. Hence,  is
consistent.
Completeness
Consistency Lemma (Continued)
To prove: for any graph : h() = True iff  EG 
Proof: By induction on the composition of any statement .
Base: For every atomic statement A, h(A) = True iff  EG A (def. h)
Step: Case 1:  = 1 2
By inductive assumption: h(i) = True iff  EG i
So, h(1 2) = True iff h(1) = True and h(1) = True iff
 EG 1 and  EG 2 iff (trivial)  EG 1 2 iff  EG 
Case 2:  = ’ By ind. assumption: h(’) = true iff  EG ’
Hence, h() = True iff h(’) = false iff not  EG ’ iff
(Either-Or Lemma)  EG ’ iff  EG 
Completeness
The Central Theorem
For any graph :
if  is Alpha consistent, then  is consistent.
Proof:
Suppose  is Alpha consistent.
By the Expansion Theorem there exists a ’ =   for
some  such that ’ is Alpha consistent and Alpha complete.
By the Consistency Lemma, this ’ is consistent.
So,   is consistent.
Therefore,  is consistent.
Completeness
Basic Completeness Theorem
For any : if TF  then EG 
Proof:
Suppose TF 
Then 
is inconsistent.
Hence (Central Theorem): 
Therefore

is Alpha inconsistent.
EG
So (Transposition Theorem): EG 
Completeness
Completeness Theorem
For any  and  : if  TF  then  EG 
Proof:
Suppose  TF 
Then TF 

Hence (Basic Completeness Theorem): EG 
Therefore (Deduction Theorem):  EG 
