1 Gentzen Style Proof Systems
for Classical Propositional Logic
Hilbert style systems are easy to define
and admit a simple proof of the Completeness
Theorem but they are difficult to use. By
humans, not mentioning computers. Their emphasis is on
logical axioms, keeping the rules of inference at a minimum.
Gentzen systems reverse this situation by emphasizing the importance of
inference rules, reducing the role of logical axioms to an absolute
minimum. They may be less intuitive then
the Hilbert-style systems, but
they will allow us to give an effective automatic
procedure for proof search, what was impossible in a case of
the Hilbert-style systems.
The
first idea of this type was presented by
G. Gentzen in 1934. He dealt with a complicated structure,
called sequent. His exact formalization will be presented in
the case if the intuitionistic logic.
The proof system presented here is due to
H. Rasiowa and R. Sikorski and appeared for the first time in 1961.
It is inspired by Gentzen original system and is equivalent to it (like may
others), so all of them are called Gentzen style proof systems.
1.1 The Gentzen Style System RS
Language
Let F denote a set of formulas of L = L {
¬ , Þ , È , Ç }.
The rules of inference of our system RS will operate on
finite sequences of formulas, i.e. elements of F* ,
instead of just plain formulas F, as in Hilbert
style formalizations. We will denote the finite sequences
of formulas by G , D , S , with indices if
necessary.
Meaning of Sequences
The intuitive meaning of a sequence G Î F* is
that the truth assignment v makes it true if and only if it makes
the formula of the form of
the disjunction of all formulas of G true.
As we know, the disjunction in classical logic is associative and
commutative, i.e.,
for any formulas A, B, C Î F, the formulas
AÈ (BÈ C) , ( AÈ B )È C, A È (C È B) ,
( B È A )È C, C È (BÈ A) , C È (A È B) ,
( C È A )È B, etc...
are logically equivalent.
We adopt hence a notation
to denote any disjunction of formulas A, B, C.
In a general case, for any sequence
G Î F* ,
if G is of a form
A1 , A2 , ... , An
(1)
then by dG we will understand any disjunction
of all formulas of G , i.e.
Formal Semantics for RS
Let v: VAR ¾® {T, F } be a truth assignment,
v* its extension to the set of formulas F,
we formally extend v to the set F* of all finite
sequences of F as follows. For any sequence
G Î F* , if G is of the form X,
then we define:
| v |
|
(G )= v |
|
(d |
|
)=
v |
|
(A1)È v |
|
( A2) È ... È v |
|
( An ). |
Model
The sequence G is said to be satisfiable
if there is a truth assignment v: VAR ¾® {T, F }
such that v* (G )= T. Such a truth assignment
will be also called a model
for G.
Counter- Model
The sequence G is said to be falsifiable
if there is a truth assignment v,
such that v* (G )= F. Such a truth assignment
will be also called a counter-model
for G.
Tautology
The sequence G is said to be a tautology
if v* (G )= T for all
truth assignments v: VAR ¾® {T, F }.
Example
Let G be a sequence
a, (b Ç a) , ¬ b, (b Þ a) .
The truth assignment v for which
v(a) = F and v(b) = T falsifies G,
as shows the following computation.
v* (G )= v* (dG)=
v* (a) È v* ( b Ç a) È
v* (¬ b ) È v* (b Þ a ) =
F È (F Ç T) È F È (T Þ F )=
FÈ F È F È F = F.
Example
Let G be a sequence
a, (¬ b Ç a) , ¬ b, (a È b)
and let v be a truth assignment for which
v(a) = T. Directly from the the definition, we get that
v* (G )= v* (dG)=
v* (a) È v* (¬ b Ç a) È
v* (¬ b ) È v* (a È b) =
T È v* (¬ b Ç a) È
v* (¬ b ) È v* (a È b) = T.
This proves that v is a model
for G and G is satisfiable.
Assume now that G is falsifiable
i.e. that we have a truth assignment v for which
v* (G )= v* (dG)=
v* (a) È v* (¬ b Ç a) È
v* (¬ b ) È v* (a È b) = F
This is possible only when v* (a) =F
and for example v* (a È b) = F. But
v* (a È b) = v* (a) È v* (b) =
F È v* (b) =
F if and only if v* (b) =
F. In this case v* (¬ b ) = ¬ v* ( b )=
¬ F = T and hence
v* (a) È v* (¬ b Ç a) È
v* (¬ b ) È v* (a È b) =
v* (dG)= v* (G )=
T.
This contradiction proves that G is a tautology.
Axioms and Rules of Inference
The rules of inference of RS are of the form:
where G 1, G 2 and G
are sequences G 1, G 2 are called
premises and G is called the conclusion of the rule of inference.
Each rule of inference introduces a new logical connective, or a negation
of a logical connective
to the antecedent or to the succedent of the conclusion sequent.
We denote the rule that introduces the logical
connective ° the conclusion sequent G by
( ° ). The notation
( ¬ ° ) means that
the negation of the logical
connective ° is introduced
the conclusion sequence G .
As our language contains the connectives: Ç , È,
Þ and ¬ , so we
we are going to define seven inference rules:
(È ), (¬ È ), (Ç ), (¬ Ç ),
(Þ ), (¬ Þ ), and (¬ ¬ ).
Axioms
As the axiom we adopt
any sequence which contains any formula
and its negation, i.e any sequence of the form
G1, A, G2, ¬ A , G3,
(2)
or of the form
G1, ¬ A, G2, A , G3
(3)
for any formula
A Î F and any sequences G1,G2,
G3 Î F* .
We
denote, as usual, the set of all axioms by
AX.
In order to define the rules of inference of RS
we need to introduce some definitions.
Literals
We form a special subset
LT Ì
F of formulas,
called a set of all literals, which is defined as follows.
LT = VAR È
{ ¬ a : a Î VAR }.
The variables are called
positive literals and the elements of the second
set of the above union are called
negative literals. I.e. Propositional variables
are called positive literals and the negation
of a variable is called a negative literal, a variable or
a negation of Propositional variable is called a literal.
Now we
form finite sequences out of formulas
(and, as a special case, out of literals). We need to distinguish
the sequences formed out of literals from the sequences formed out of other
formulas, so we adopt the following notation.
We denote by
G ', D ', S '
finite sequences (empty included) formed out of literals i.e.
out of the elements of LT i.e. we
assume that G ', D ',
S ' Î LT* .
We will denote by G , D , S the elements of
F* i.e. the finite sequences (empty included)
formed out of elements of F.
Inference rules of RS
We define formally the inference rules of RS as follows.
Disjunction rules
| (È ) |
| G ', A, B, D |
|
| G ', ( A È B), D |
|
,
(¬ È ) |
| G ', ¬ A ,
D : G ',¬ B, D |
|
| G ', ¬ (A È B), D |
|
Conjunction rules
| (Ç ) |
| G ', A, D ;
G ', B, D |
|
| G ', (A Ç B ), D |
|
,
( ¬ Ç ) |
| G ',¬ A, ¬ B, D |
|
| G ', ¬ (A Ç B), D |
|
Implication rules
| ( Þ ) |
| G ', ¬ A, B, D |
|
| G ', ( A Þ B), D |
|
,
(¬ Þ ) |
| G ', A ,
D :
G ',¬ B, D |
|
| G ', ¬ (A Þ B),
D |
|
Negation rule
where G ' Î LT* , D Î
F* , A,B Î F.
The Proof System RS
Formally we define:
| RS = ( L |
|
, AX |
|
,
(È ), (¬ È ), (Ç ), (¬ Ç ),
(Þ ), (¬ Þ ),(¬ ¬ )) |
where (È ), (¬ È ), (Ç ), (¬ Ç ),
(Þ ), (¬ Þ ),(¬ ¬ ) are the inference
rules defined above and AX
is the axiom of the system defined by the
schemas X and X.
We define the notion of a formal proof in RS
as in any proof system, i.e., by a formal proof of a sequence
G in the proof system RS = ( F* ,
AX ,
(È ), (¬ È ), (Ç ), (¬ Ç ),
(Þ ), (¬ Þ ),(¬ ¬ ))
we understand any sequence
G1 G2 .... Gn
of sequences of formulas
(elements of F* , such that
G1 Î AX, Gn = G ,
and for all i (1 <i £ n) Gi Î AX,
or Gi is a conclusion of one of the inference rules of RS
with all its premises placed in the sequence
G1 G2 .... Gi-1.
As the proof system under consideration is fixed, we will write, as usual,
|- G
instead of |- RS G
to denote that G has a formal proof in RS.
As the proofs in RS are sequences (definition of the formal
proof) of sequences of formulas (definition of RS ) we
will not use "," to separate the steps of the proof, or will write
sometimes the formal proof
(i. e. the sequence G1 G2 .... Gn)
in a vertical form
G1
G2
...
Gn.
We write, however, the formal proofs in RS
in a form of trees rather then in a form of sequences, ie. in a form
theorem
/\
where leafs of
the tree are axioms,
nodes are
sequences such that each sequence on the tree
follows from the ones immediately preceding it by one of the
rules. The root is a theorem. We picture, and write our tree-proofs
with the node on the top, and leafs on the very bottom, instead of more
common way, where the leafs are on the top and root is
on the bottom of the tree. We adopt hence the following definition.
Proof Tree
By a proof tree, or RS-proof of G we understand
a tree T G
of sequences satisfying the following conditions:
1. The topmost sequence, i.e. the root of
T G is
G ,
2. all leafs are axioms,
3. the nodes are
sequences such that each sequence on the tree
follows from the ones immediately preceding it by one of the
rules.
We picture, and write our proof trees
with the node on the top, and leafs on the very bottom, instead of more
common way, where the leafs are on the top and root is
on the bottom of the tree.
In particular cases we write our proof trees indicating additionally
the name of the inference rule used at each step of the proof.
For example, if the proof of a theorem
from 3 axioms
was obtained by the subsequent use of the
rules (Ç ) ,(È ), (È ), (Ç ), (È ),
(¬ ¬), and (Þ ),
we represent it as the following tree:
theorem
| (Þ)
conclusion of (¬ ¬)
| (¬ ¬)
conclusion of (È )
| (È )
conclusion of (Ç )
Ù (Ç)
conclusion of (Ç )
conclusion of (È )
| (È )
| (È )
axiom
conclusion of (Ç )
Ù (Ç)
The proof trees are often called derivation trees and we will
use this notion as well.
Remark that the derivation trees don't
represent a different definition of
a formal proof. Trees represent a certain visualization
for the proofs and any formal proof in any system
can be represented in a tree form.
Example
The proof tree in RS
of the de Morgan law
( ¬ ( a Ç b) Þ (¬ a È ¬ b ))
is the following.
(¬ (a Ç b ) Þ (¬ a È ¬ b ))
| (Þ )
¬ ¬ (a Ç b), (¬ a È ¬ b )
| (¬ ¬ )
(a Ç b), (¬ a È ¬ b )
Ù (Ç )
a, (¬ a È ¬ b )
b, (¬ a È ¬ b )
| (È)
| (È)
a, ¬ a, ¬ b
b, ¬ a, ¬ b
To obtain a "linear " formal proof (written in a vertical form) of it
we just write down the tree as a sequence,
starting from the leafs and going up (from left to right)
to the root.
The formal proof thus obtained will be the following
sequence of elements of F* :
a, ¬ a, ¬ b
b, ¬ a, ¬ b
a, (¬ a È ¬ b )
b, (¬ a È ¬ b
(a Ç b), (¬ a È ¬ b )
¬ ¬ (a Ç b), (¬ a È ¬ b )
(¬ (a Ç b ) Þ (¬ a È ¬ b )).
2 Search for Proofs and Decomposition trees
The main advantage of our system and the
the Gentzen style systems in general lies not
in a way we generate proofs in them, but
in the way we can search for proofs in them.
That happens to be deterministic and
automatic.
Before we describe the general proof
search procedure,
let us
consider few examples.
Example
Consider now a formula A of the form of
another de Morgan law
( ¬ ( a È b) Þ (¬ a Ç ¬ b )).
Obviously it should have a proof in RS.
The search for it consists of building a
certain tree and proceeds as follows.
Observe that the main connective of A is Þ. So,
if it had a proof in RS it would have come from
the only possible rule used in its last step, namely the rule
( Þ ) applied to a sequence
¬ ¬ (a È b), (¬ a Ç ¬ b ). So the
last step in the proof of A would look as follows.
( ¬ ( a È b) Þ (¬ a Ç ¬ b ))
| (Þ)
¬ ¬ (a È b), (¬ a Ç ¬ b )
Now, if the sequence
¬ ¬ (a È b), (¬ a Ç ¬ b )
(and hence also had our formula )
had a proof in RS
its only step at this stage would
have been the application of the rule (¬ ¬ )
to a sequence (a È b), (¬ a Ç ¬ b ) .
So, if A had a proof,
its last two steps
would have been:
( ¬ ( a È b) Þ (¬ a Ç ¬ b ))
| (Þ)
¬ ¬ (a È b), (¬ a Ç ¬ b )
| (¬ ¬)
(a È b), (¬ a Ç ¬ b )
Again, if the sequence (a È b), (¬ a Ç ¬ b )
had a proof in RS
its only step at this stage would
have been the application of the rule (È )
to a sequence a, b, (¬ a Ç ¬ b ) .
So, if A had a proof,
its last three steps
would have been as follows.
( ¬ ( a È b) Þ (¬ a Ç ¬ b ))
| (Þ)
¬ ¬ (a È b), (¬ a Ç ¬ b )
| (¬ ¬)
(a È b), (¬ a Ç ¬ b )
| (È )
a, b, (¬ a Ç ¬ b )
Now, if the sequence a, b, (¬ a Ç ¬ b )
had a proof in RS
its only step at this stage would
have been the application of the rule (Ç )
to the sequences a, b, ¬ a and
a, b, ¬ b as its left and right premises, respectively.
Both sequences are axioms and the following tree is a proof of
A in RS.
( ¬ ( a È b) Þ (¬ a Ç ¬ b ))
| (Þ)
¬ ¬ (a È b), (¬ a Ç ¬ b )
| (¬ ¬)
(a È b), (¬ a Ç ¬ b )
| (È )
a, b, (¬ a Ç ¬ b )
Ù (Ç)
a, b, ¬ a
a, b, ¬ b
From the above proof tree of A we construct
its
formal proof, written in a vertical manner,
by writing the two axioms, which form the
two premises of the rule (Ç) one above the other. All
other sequences remain the same. I.e. the following
sequence of elements of F* is a formal proof of
( ¬ ( a È b) Þ (¬ a Ç ¬ b )) in RS.
a, b, ¬ b
a, b, ¬ a
a, b, (¬ a Ç ¬ b )
(a È b), (¬ a Ç ¬ b )
¬ ¬ (a È b), (¬ a Ç ¬ b )
( ¬ ( a È b) Þ (¬ a Ç ¬ b ))
Example
Given a formula A of the form
(((a Þ b ) Ç ¬ c ) È
(a Þ c))
Observe that the main connective of A is È. So,
if it had a proof in RS it would have come from
the only possible rule used in its last step, namely the rule
(È) applied to a sequence
((a Þ b ) Ç ¬ c ),
(a Þ c).
So the last step in the proof of A would have been:
(((a Þ b ) Ç ¬ c ) È
(a Þ c))
| (È)
((a Þ b ) Ç ¬ c ),
(a Þ c)
Now, if the sequence
((a Þ b ) Ç ¬ c ),
(a Þ c) (and hence also had our formula )
had a proof in RS its only step at this stage would
have been the application of the rule
(Ç )
to the sequences (a Þ b), (a Þ c) and
¬ c, (a Þ c) as its left
and right premises, respectively. So, if A had a proof,
its last two steps
would have been:
(((a Þ b ) Ç ¬ c ) È
(a Þ c))
| (È)
((a Þ b ) Ç ¬ c ),
(a Þ c)
Ù (Ç)
(a Þ b), (a Þ c)
¬ c, (a Þ c)
Now, if the sequences (a Þ b), (a Þ c) and
¬ c, (a Þ c) had proofs in RS, then
their last, and the only steps would have been the the separate
application of the rule (Þ )
to the sequences ¬ a, b, (a Þ c) and ¬ c, ¬ a, c ,
respectively. The sequence
¬ c, ¬ a, c is an axiom, so we stop the search on this branch.
The sequence ¬ a, b, (a Þ c) is not an axiom,
so the search continues. In this case we can go one step further:
if ¬ a, b, (a Þ c) had a proof it would have been
only by
the application of the rule (Þ )
to a sequence ¬ a, b, ¬ a , c
which is not an axiom and the search ends.
The tree generated by this search is called a decomposition tree
and is the following.
(((a Þ b ) Ç ¬ c ) È
(a Þ c))
| (È)
((a Þ b ) Ç ¬ c ),
(a Þ c)
Ù (Ç)
(a Þ b), (a Þ c)
¬ c, (a Þ c)
| (Þ)
| (Þ)
¬ a , b , (a Þ c)
¬ c, ¬ a , c
| (Þ)
¬ a , b , ¬ a ,c
As the tree generated by this search contains an non-axiom leaf
and hence is not a proof.
As we can see from the above example,
the process of searching for the proof of
a formula A in RS consists of building a certain tree, whose root is
the formula A, nodes correspond to sequences which are
conclusions of
certain rules (and those rules are well defined at each step
by the way the node is built), and leafs are axioms or, as we will
see in the next example, are sequences of literals.
The trees build in this way will be called decomposition trees and we will see that each formula
A generates its unique, finite decomposition tree,
T A.
If all the leafs of the tree T A are axioms,
it means that the proof of A in RS is found.
If there is a leaf of T A which is not an axiom, it
would mean that the proof of A does not exist.
Before we give a proper mathematical definition
of the proof search procedure by building the decomposition trees we
list few important observations about
the structure of the rules of the system
RS.
-
Introduction of Connectives
-
The rules of RS
are defined in such a way that each of them introduces
a new logical connective to a sequence in its domain
(rules (È ), (Þ ), (Ç )) or a negation
of a new logical connective (rules (¬ È ), (¬ Ç ),
(¬ Þ ), (¬ ¬ )).
I.e. the rule
(È ) introduces a new connective È to a sequence
G ', A, B, D and it becomes, after the application
of the rule, a sequence
G ', ( A È B), D . Hence a name for this rule is
(È ). The same applies to all remaining rules of RS,
hence their names say which connective, or the negation
of which connective
has been introduced by the particular rule.
- Indecomposable
-
If a sequence G is built only out of literals, i.e.,
G Î LI* none of the rules has been
applied. Such sequences will be called
indecomposable.
- Decomposable formula
-
If G ÏLI* , i.e.
G is a decomposable sequence, there is a
first formula in G
which is not a literal. Let call it
decomposable formula.
- Unique rule
-
For any decomposable
sequence, i.e. for any G ÏLI*
there is exactly one inference rule, such that
G has a form of its conclusion.
This rule is determined by
the first decomposable formula in G, and by
the main connective of that formula.
In particular, we have the following cases.
-
- Connective
-
The main connective of the first decomposable
formula is È , Ç , or Þ , then
the rule determined by it is (È ), (Ç ), or
(Þ ), respectively.
- Negation of a connective
-
The main connective of the first decomposable
formula is ¬. The rule determined by it is
hence determined by the second connective
of the formula. If the second connective is
È , Ç ,¬ , or Þ , then
corresponding
rule is (¬ È ), (¬ Ç ), (¬ ¬ ) and
(¬ Þ ).
Because of the
importance of the above observations we
write them in a form of the following
Lemma 2.1 [Unique rule principle] For any sequence G Î F* ,
G Î LI* or G is
a conclusion of exactly one rule of RS.
Let's now use the above observations to
define for any sequence G of formulas
its a a decomposition tree TG.
Definition of the Decomposition Tree
Theorem 2.1 For any sequence G Î F* the following
conditions hold.
1. TG is finite and unique.
2. TG is a proof of G in
RS if and only if all its leafs are axioms.
3. ¬ |- bf RS
if and only if TG has a non- axiom leaf.
Example
Let construct, as an
example a decomposition tree of the following formula A.
((a È b ) Þ ¬ a )
È (¬ a Þ ¬ c))
The formula A forms a one element decomposable sequence. The first decomposition rule used
is determined by its main connective. We put a box around it,
to make it more visible. The first and only rule applied is
(È ) and we can write the first segment of our
decomposition tree:
| ((a È b ) Þ ¬ a )
|
|
(¬ a Þ ¬ c)) |
| (È )
((a È b ) Þ ¬ a )
,(¬ a Þ ¬ c))
Now we decompose the sequence ((a È b ) Þ ¬ a ),
(¬ a Þ ¬ c)). It is a decomposable
sequence with the first, decomposable formula
((a È b ) Þ ¬ a ). The next step of the construction
of our decomposition tree is determined by its main connective
Þ (we put the box around it), hence the only rule
determined by the sequence is (Þ ).
The
decomposition tree now has a form:
| ((a È b ) Þ ¬ a )
|
|
(¬ a Þ ¬ c)) |
| (È )
| ((a È b ) |
|
¬ a ),
(¬ a Þ ¬ c)) |
| (Þ)
¬ (a È b ), ¬ a,
(¬ a Þ ¬ c))
The next sequence to decompose is the sequence
¬ (a È b ), ¬ a,
(¬ a Þ ¬ c)) with the first decomposable formula
¬ (a È b ). Its main connective is ¬, so to find
the appropriate rule we have to examine next connective, which is È.
The rule determine by this stage of decomposition is (¬ È) and
now the decomposition tree becomes:
| ((a È b ) Þ ¬ a )
|
|
(¬ a Þ ¬ c)) |
| (È )
| ((a È b ) |
|
¬ a ),
(¬ a Þ ¬ c)) |
| (Þ)
| |
|
(a |
|
b ), ¬ a,
(¬ a Þ ¬ c)) |
Ù (¬ È)
¬ a, ¬ a,
(¬ a Þ ¬ c))
¬ b, ¬ a,
(¬ a Þ ¬ c))
Now we have two decomposable sequences: ¬ a, ¬ a,
(¬ a Þ ¬ c)) and ¬ b, ¬ a,
(¬ a Þ ¬ c)). They both happen to have the same
first decomposable formula (¬ a Þ ¬ c)). We decompose it
and obtain the following:
| ((a È b ) Þ ¬ a )
|
|
(¬ a Þ ¬ c)) |
| (È )
| ((a È b ) |
|
¬ a ),
(¬ a Þ ¬ c)) |
| (Þ)
| |
|
(a |
|
b ), ¬ a,
(¬ a Þ ¬ c)) |
Ù (¬ È)
| ¬ a, ¬ a,
(¬ a |
|
¬ c)) |
|
¬ b, ¬ a, (¬ a |
|
¬ c)) |
| (Þ)
| (Þ)
¬ a, ¬ a,
¬ ¬ a, ¬ c
¬ b, ¬ a, ¬ ¬ a, ¬ c
It is easy to see that we need only one more step to
complete the process of constructing the unique decomposition tree of A,
namely, by decomposing the sequences: ¬ a, ¬ a,
¬ ¬ a, ¬ c and ¬ b, ¬ a,
¬ ¬ a, ¬ c
The complete decomposition tree TA is:
| ((a È b ) Þ ¬ a )
|
|
(¬ a Þ ¬ c)) |
| (È )
| ((a È b ) |
|
¬ a ),
(¬ a Þ ¬ c)) |
| (Þ)
| |
|
(a |
|
b ), ¬ a,
(¬ a Þ ¬ c)) |
Ù (¬ È)
| ¬ a, ¬ a,
(¬ a |
|
¬ c)) |
|
¬ b, ¬ a,
(¬ a |
|
¬ c)) |
| (Þ)
| (Þ)
| ¬ a, ¬ a,
|
|
a, ¬ c |
|
¬ b, ¬ a, |
|
a, ¬ c |
| (¬ ¬)
| (¬ ¬)
¬ a, ¬ a, a, ¬ c
¬ b, ¬ a,
a, ¬ c
All leafs are axioms, the tree represents a proof of A in RS
Consider now again a formula (((a Þ b ) Ç ¬ c ) È
(a Þ c)) and its decomposition tree:
(((a Þ b ) Ç ¬ c ) È
(a Þ c))
| (È)
((a Þ b ) Ç ¬ c ),
(a Þ c)
Ù (Ç)
(a Þ b), (a Þ c)
¬ c, (a Þ c)
| (Þ)
| (Þ)
¬ a , b , (a Þ c)
¬ c, ¬ a , c
| (Þ)
¬ a , b , ¬ a ,c
The above tree is unique by the theorem X and represents
the only possible
search for proof of the formula A of the form
((a Þ b ) Ç ¬ c ) È
(a Þ c))
in RS. It ended with a non-axiom leaf hence
the proof of
A
in RS does not exists.
We use this information to construct a variable assignment that would falsify
a given formula. Such a variable assignment is called
a counter-model generated by the decomposition tree.
Counter-model generated by the decomposition tree
Given a formula A: ((a Þ b ) Ç ¬ c ) È
(a Þ c)) and its decomposition tree TA.
Consider a non-axiom leaf
¬ a , b , ¬ a ,c of TA . Let v be any
variable assignment
v: VAR ¾® {T, F}
such that
v(a) = T, v(b) = F, v(c) = F.
Obviously,
| v |
|
(¬ a , b , ¬ a , c) = F. |
Moreover, all our rules of inference are sound
(to be proven formally in the next section). It means that
if one of premises of a rule is FALSE, so is the conclusion.
This proves that v, as defined above falsifies all
sequences on the branch of TA that ends
with the non-axiom leaf ¬ a , b , ¬ a ,c.
In particular, the formula A is on this branch, hence
| v |
|
(((a Þ b ) Ç ¬ c ) È
(a Þ c)) = F |
and v is a counter-model for A.
The variable assignments constructed in this way are called
the counter-model generated by the decomposition tree.
We generalize the method presented in the above example to prove
the following.
Theorem 2.2 For any G Î F*,
if ¬ |- RS G then
¬ |= G .
3 Soundness and Completeness of RS
Lemma 3.1 [Soundness Lemma 1]
For any G Î F*,
if |-RS G , then |= G.
We prove here as an example the soundness of two of inference rules.
PROVE AS THE HOMEWORK ALL OTHERS.
We show that rules (Þ ) and
( ¬ È ) of G are sound.
We will show even more, that the premises and conclusion of both rules are logically equivalent.
I.e.
instead of showing that for all v,
v*(Premise (s))=T,
then v* (Conclusion) =T, we will show the following.
If P1 , (P2 ) are
premise (s) of a rule, C is its conclusion, then
v* (P1) = v* (C) in case of one
premise rule and
v* (P1) Ç v* (P2) = v* (C), in case
of the two premises rule.
Consider the rule (È).
| (È) |
| G ', A, B, D |
|
| G ', ( A È B), D |
|
. |
By the definition:
v* (G ', A, B, D)
= v* (d{G ', A, B, D }) =
v* (G ') È v* (A) È v* (B) È
v* (D ) =
v* (G ') È v* (A È B) È
v* (D ) =
v* (d {G ', (AÈ B), D }) =
v*(G ', ( A È B), D ).
Consider the rule (¬ È).
| (¬ È ) |
| G ', ¬ A ,
D : G ',¬ B, D |
|
| G ', ¬ (A È B), D |
|
. |
By the definition:
v* (G ', ¬ A ,
D ) Ç v* (G ', ¬ B, D) =
(v* (G ') È v*(¬ A ) È v*(D )
)
Ç (v* (G ') È v*(¬ B ) È v*(D )
)=
(v* (G ',D) È v*(¬ A )
) Ç (v* (G ', D ) È v*(¬ B )) =
by distributivity = (v* (G ',D) È (v*(¬ A)
Ç v*(¬ B )) =
v* (G ' )È v* (D) È (v*(¬ A
Ç ¬ B )) = by the logical equivalence
of (¬ A Ç ¬ B ) and ¬ (A È B ) =
v*(d{ G ', ¬ (A È B), D }
=v*(G ', ¬ (A È B), D )).
From the above Soundness Lemma 1 X
we get, in a case when G is a one formula
sequence, as a corollary the following soundness lemma for formulas.
Lemma 3.2 [Soundness Lemma 2]
For any A Î F,
if |-RS A , then |= A.
Theorem 3.1 [Completeness Theorem 1]
For any formula A F,
|-RS A if and only if |= A.
Theorem 3.2 [Completeness Theorem 2]
For any G Î F*,
|-RS G if and only if |= G .
As an example, we list the main steps in the proof of
a contraposition:
If ¬ |-RS A , then ¬ |=A .
To prove this we proceed as follows.
-
Define, for each A Î F its decomposition tree.
- Prove that the decomposition tree is unique and has the following property:
|-G A iff all leafs of the decomposition tree of A are axioms.
What means that
If ¬ |-RS A , then there is a leaf of the decomposition tree
of A, which is not an axiom.
- Observe, that if one premise of a rule of RS
is FALSE, so is the conclusion. So, by the definition of the
decomposition tree, if we have
a truth assignment v, such that v*(leaf) =F , it means
that we have a truth assignment which falsifies A, namely v*(A) =F.
- Given a formula A such that
¬ |-G A
and
the decomposition tree of A. The non-axiom leaf LA
defines a truth assignment v which falsifies A, as follows:
| v(a) = |
ì
í
î |
| F |
if a appears in LA |
| T |
if ¬ a appears in LA |
| any value |
if a does not appear in LA |
|
|
This proves that ¬ |=A .
This document was translated from LATEX by HEVEA.