Transcript Survey on Widening and Narrowing

Techniques for Proving the Completeness of a
Proof System
Hongseok Yang
Seoul National University
Cristiano Calcagno
Imperial College
Completeness Question


Completeness: Is a proof system powerful enough to verify
all true facts?
Proof system for classical propositional logic:
` P)(Q)R)
` (P)(Q)Q’)))((P)Q))(P)Q’))
` ::P)P
` P ` P)Q
`Q



Truth: P holds (denoted ² P) iff P always evaluates to true
by the “table method.”
Completeness Theorem: if ² P, then ` P.
Exercise: Prove ` ((q)r))q))q.
Reasons for Studying Completeness
1.
2.
3.
4.
Sometimes it is easier to show the truth of a
formula than to derive the formula.
The completeness result shows that nothing is
missing in a proof system.
The completeness result formalizes what a proof
system achieves.
With a completeness result, a paper about a proof
system has more chances to get accepted. 
Goal of My Talk



To present common techniques for showing the
completeness, so that you can apply them to your
own problem.
In particular, to explain the following concepts:

maximally consistent set

truth lemma

Lindenbaum lemma
If time permits, I will briefly explain what I’m
working on with Calcagno in Imperial college.
Simple Modal Logic


P := q | :P | P)P | P
Proof system: usual rules in classical logic with the
following additional ones for the modality:
`P
` P
` (P)Q))(P)Q)
Example:
 student, phd, professor
 deadlock, deadlock, ::deadlock
Semantics
A model M is a triple (M, R:M$M, I:Symb!P(M)).


Interpretation of Simple Modal Logic
M,m ² q
iff m 2 I(q)
M,m ² :P
iff M,m 2 P
M,m ² P)Q iff if M,m ² P, then M,m ² Q
M,m ² P
iff for all n, if R(m,n), then M,n ² P
Example:

M=years,

R(n,m) iff m=n+1,

I(phd)={2001,…}, I(student)={1982,…,2001}
Completeness Question



P is valid (denoted ² P) iff for all models (M,R,I)
and all m in M, (M,R,I),m ² P.
Completeness: If ² P, then ` P.
General guide: consider the contrapositive!

Contrapositive: if 0 P, then 2 P.

Guide: for each P such that 0 P, construct a
model (M,R,I) with m in M such that
(M,R,I),m ² :P.
Strategy for Constructing a Required
Model



Build a model M = (M,R,I) such that
1.
[term model] each m in M is a set of formulas;
2.
[truth lemma] for all m and Q,
m ² Q iff Q is in m;
3.
there exists n in M containing :P.
This model is what we are looking for. (Why?)
How to build such a model?
Inferring Requirements from the Truth
Lemma



Let M=(M,R,I) be a model such that each m in M
is a set of formulas.
Try to use induction to show the truth lemma for
M: for all m in M and Q, m²Q iff Q is in m.
What conditions do R and I satisfy?
Inferring Requirements from the Truth
Lemma



Let M=(M,R,I) be a model such that each m in M
is a set of formulas.
Try to use induction to show the truth lemma for
M: for all m in M and Q, m²Q iff Q is in m.
What conditions do R and I need to satisfy?
1.
Q is not in m iff :Q is in m.
2.
If both Q and Q)Q’ are in m, then Q’ is in m.
3.
If R(m,n) and Q is in m, then Q is in n.
4.
m is in I(q) iff q is in m.
Maximally Consistent Set



A set m of formulas is maximally consistent iff
1.
for all Q, only one of Q and :Q is in m; and
2.
if Q0,Q1,...,Qn2m and `Q0)Q1)…)Qn)Q’, then Q’ in m.
By turning the conditions into the definition (almost
directly), we can construct the required model:

M consists of maximally consistent sets of formulas;

R(m,n) iff for all Q in m, Q in n;

m2I(p) iff p2m.
The proof for the truth lemma “almost” works.
Lindenbaum Lemma



Still need to show two facts:

If m ² Q, then Q is in m.

There exists m in M such that m ² :P.
Lindenbaum Lemma:
Let {Q0,Q1,…,Qn} be a set of formulas. If
0 Q0)Q1) …)Qn)false,
then there is a maximally consistent set m s.t.
Q0, Q1, …, Qn 2 m.
Try to show the two properties with Lindenbaum
Lemma.
Summary
We constructed “canonical” model (M,R,I):

M consists of maximally cons. sets of formulas.

R(m,n) iff for all P in m, P is in n.

m 2 I(p) iff p in m.
The model satisfies the following properties:

truth lemma: m ² P iff P is in m.

If 0:P, then there is m such that P 2 m.
These two properties lead to the completeness.
My Work with Calcagno
Interested in the completeness of Boolean BI wrt PCM models.

Conceptual implication: supports that BBI is a logic for
computational resources.

“Practical” implication: shows that the proof rules in
separation logic are powerful enough.
Roughly, the question is similar to asking whether our model
logic are complete wrt injective models.

(M,R,I) is injective iff R(m,n)ÆR(m,n’) ) n=n’
We found a method to transform the “canonical” model to an
injective one, while preserving the satisfiability of formulas.