arXiv:cs/0303021v2 [cs.LO] 2 Apr 2003

A Development Calculus
for Specifications
Wei

LI

liwei@nslde.buaa.edu.cn
State Key Laboratory of Software Development Environment
Beihang University
100083 Beijing, P.R. China
Abstract
A first order inference system, named R-calculus, is defined to develop the specifications. This system intends to eliminate the laws which is not consistent with user’s
requirements. The R-calculus consists of the structural rules, an axiom, a cut rule, and
the rules for logical connectives. Some examples are given to demonstrate the usage of the
R-calculus. Furthermore, the properties regarding reachability and completeness of the
R-calculus are formally defined and proved.
Keywords: Specification, Revision, Necessary premise, R-calculus, R-condition

1

Motivation

During the development of the specifications, two situations are encountered commonly:
First, the specification is not consistent; as a result, a program to satisfy it does not
exist. Second, the specification is consistent, but users and designers refuse to accept
it since the running results of the generated program does not meet their requirements.
Under both circumstances, the specification should be redesigned. If it was indeed the
case, the elimination of inconsistent laws and the introduction of new laws become very
important; this paper will address this concerns principally. For example, consider the
following specification:
Γ ≡ {A, A ⊃ B, B ⊃ C, E ⊃ F }
where A, B, C, E, and E denote some equations. It is obviously that Γ ⊢ C holds. Users,
however, reject C and prefer ¬C. In this case, we have to redesign the specification.
The purpose of this paper, therefore, concerns principally to build an inference system,
named R-calculus to revise the specifications. The nature of R-calculus differentiates it
from many well known inference systems of specifications. The purpose of the latter aims
to deduce the correct programs to satisfy a given specification[10,11,12,13]. However, Rcalculus emphasizes on revising the specifications, and eliminating the laws which are not
consistent with user’s requirements.
The R-calculus is indeed a transition system which consists of the structural rules,
an axiom, an cut rule, and the rules of logical connectives. Some examples are given to
demonstrate how the R-calculus can be used to develop specifications. Furthermore, the
properties of the R-calculus, such as reachability and completeness, are formally defined
and proved.

2

The Necessary Premise

In order to avoid the syntactical details, in this paper, the first order languages are chosen
to be the specification languages [1]. Briefly, a first order language L has two sets of
symbol strings. They are the set of terms and the set of formulas. The set of terms is
defined on the set of variable symbols V ranged over by x, y, z · · ·, the set of function
symbols F ranged over by f, g, h · · ·, and the set of constants symbols C ranged over by
a, b, c · · ·, and it is defined inductively as below:
t ::= c | x | f (t1 , t2 , · · · , tn )
The set of formulas are defined on the set of predicates P ranged over by P, Q, R, · · ·, and
the set of logical connectives including: ¬, ∧, ∨, ⊃, ∀, ∃, and it is defined inductively as
the following,
A ::= P (t1 , t2 , · · · , tn ) | ¬A | A ∧ B | A ∨ B | A ⊃ B |∀x.A | ∃x.A
In this paper, Γ is used to denote a formal theory, which is a finite set of formulas.
T h(Γ) denotes the set of all logical consequences of Γ. Γ ⊢ A is called a sequent, where A
is a logical consequence of Γ [1,2], ⊢ is the deductive relation. A Gentzen style inference
system, such as G system [1] is employed for the logical analysis of the specifications.
Each inference rule of LK is described by a fraction of number of sequents. A proof tree
T of the sequent Γ ⊢ A is a finite tree structure, where every node of T is a sequent, the
node and its direct sons forms an application of an inference rule of the G system, the
root of T is Γ ⊢ A, and every leaf of T is an axiom.
Definition 2.1 Necessary premise
Let Γ ⊢ A, and T be its proof tree. Let P , Q, and R be formulas in T. P is premise
of Q, if and only if the following items hold:
1. If Γ′ , P ⊢ P is a leaf of T, then the P on the left hand side of ⊢ is the premise of the
P on the right hand.
2. If the node of T is an application of a right rule, Q is one of A∧B, A∨B,A ⊃ B, ¬A,
∀x.A, and ∃x.A, which is a principal formula [1] in the denominator of the inference
rules, and P is one of A,B,A[t/x], and A[y/x], which is a side formula [1] in the
numerator of the corresponding inference rule,then P is the premise of Q.
3. If the node of T is an application of a left rule, and Q′ is one of A ∧ B, A ∨ B,A ⊃ B,
¬A, ∀x.A, and ∃x.A, which is a principal formula in the denominator of the inference
rules, then Q′ is the premise of A,B, A[t/x], and A[y/x], which is a side formula
in the numerator of the corresponding inference rule. Every one of A,B, A[t/x],
and A[y/x] is necessary premise of the formula on the right hand side of ⊢ in the
denominator.
4. If P is Q’s premise, and Q is R’s necessary, then P is R’s necessary premise.
Let PT (Γ, A) be the set of premise of A in the proof tree T. If P ∈ Γ holds and P is
the premise of A in T, precisely, P ∈ Γ ∩ PT (Γ, A), P is the necessary premise of A in T,
¯
which can be written as P 7→T A.
Box

According to definition 2.1, for any given Γ ⊢ A, the necessary premise of A depends
on the proof tree T. However, whenever Γ ⊢ A holds, its proof tree exists. Thus, for the
reason to simplify the writings, sometimes the tree T is omitted from 7→ and the related
notation will be written as P 7→ A when there does not exist confusion in the context.
Example 2.1 ∧- right rule:

Γ⊢A Γ⊢B
Γ⊢ A∧B
A and B are the necessary premise of A ∧ B.
Example 2.2
Consider the sequent: C, A, ∀x(A ⊃ B(x)) ⊢ ∃xB(x). Its proof tree is the following:
C, A∗4 , (∀x(A ⊃ B(x)))∗2 , (A ⊃ B[t/x])∗2 ⊢ A∗3
C, A, (∀x(A ⊃ B(x)))∗2 , (B[t/x])∗3 ⊢ B[t/x]∗1
C, A, (∀x(A ⊃ B(x)))∗2 , (A ⊃ B[t/x])∗2 ⊢ B[t/x]∗1
C, A, (∀x(A ⊃ B(x)))∗2 ⊢ B[t/x]∗1
C, A, ∀x(A ⊃ B(x)) ⊢ ∃xB(x)

The first node is an application of the ∃-right rule. B[t/x] is premise of ∃xB(x). We use
superscript ∗ to denote the premise, and use number 1 to denote the first node. The second
node is an application of the ∀-left rule. According to definition 2.1, (∀x(A ⊃ B(x)))∗2 on
the left hand of ⊢ in the denominator of the node 2 is the premise of (A ⊃ B[t/x])∗2 on
the left hand of ⊢ in the numerator, and (A ⊃ B[t/x])∗2 is also the premise of B[t/x]∗1 .
The third node of the proof three is an application of ⊃-left rule. According to definition
2.1, (A ⊃ B[t/x])∗2 is the premise of A∗3 on the right hand of ⊢ of the first sequent in the
numerator, and is also the premise of B[t/x]∗3 on the left hand of ⊢ of the second t in the
numerator. A∗3 and B[t/x]∗3 are the premise of B[t/x]∗1 on the right hand of ⊢ in the
denominator of the node 3. The forth node is an application of the axiom. A∗4 on the left
hand of ⊢ is the premise of A∗3 on the right hand. The fifth node is also an application of
the axiom. B[t/x]∗3 on the left hand of ⊢ is the premise of B[t/x]∗1 on the right. Thus,
the set of numbers of the premise of the proof three is
{B[t/x], ∀x(A ⊃ B(x)), A ⊃ B[t/x], A}
According to the definition 2.1, the necessary premise of ∃x.B(x) of the sequent C, A, ∀x(A ⊃
B(x)) ⊢ ∃x.B(x) is:
{A, ∀x(A ⊃ B(x))}
✷
Lemma 2.1 Let Γ ⊢ A and T be its proof tree. The set P(Γ, A) is decidable.
Proof. According the definition of the necessary premise, an algorithm can be designed
in the following way: Its input is the proof tree, and its output is the set P(Γ, A). The
algorithm computes the premise from the root of T to the leaves of T as shown in the
above example2.2. Since the proof tree T is finite, the algorithm will be halt.
✷
In this paper, the finite formal theories of L are used to describe the specifications.

Definition 2.2 Specification
A finite consistent set Γ of the sentences is called a specification. The sentences contained in Γ are called the laws of the specification.
We assume that two sentences P and Q are the same sentence if and only if P ≡ Q
(that is (P ⊃ Q) ∧ (Q ⊃ P ) is a tautology).
A model M is a pair < M, I >, where M is a non empty set and it is called domain,
I is a map and it is called interpretation. The form M |= A means that for the given
domain M and the interpretation I, A is true in M . M |= Γ mean that for every A ∈ Γ,
M |= A.
Definition 2.3 A is called a logical consequence of Γ and is written as Γ |= A, if and
only if for every M, if M |= Γ, then M |= A holds.

3

The User’s rejections

As we mentioned before, the users reject a specification when they have found its counter
example. In the first order logic, the user’s rejection can be defined by the models.
Definition 3.1 User’s rejection
Let Γ |= A. A model M is called a user’s rejection of A if and only if M |= ¬A. Let
ΓM (A) ≡ {Ai | Ai ∈ Γ, M |= Ai , M |= ¬A}
M is called an ideal user’s rejection of A if and only if ΓM (A) is maximal in the sense
that there does not exist another user’s rejection M′ of A, such that ΓM (A) ⊂ ΓM ′ (A) .
The above definition describe the following situation that Γ ⊢ A, but the users or
designers have found a counter example M that makes ¬A true. ΓM (A) is a subset of Γ
which does not contradict to ¬A. The user’s rejection meets the intuition that whether a
specification is accepted, depends only on whether its logical consequences agree with user’s
requirements. The ideal user’s rejection meets the Occam’s razor, which says: Entities
are not to be multiplied beyond necessity[3]. Here, it means that if a logical consequence
deduced from a specification is rejected by the users, then the maximal subsets of the
specification which is consistent with the user’s rejection must be retained and are assumed
to be true in the current stage of the development of the specification, but the rest of laws
contained in the specification must be removed because they lead to the user’s rejection.
In the rest of the paper, we consider ideal user’s rejections only, and simply call them
user’s rejections. Sometimes, we even say that ¬A is a user’s rejection of Γ, it means that
Γ ⊢ A and there is an ideal user’s rejection M and M |= ¬A.
Definition 3.2 (Maximal contraction).
Let Γ ⊢ A and Λ ⊂ Γ. Λ is called a maximal contraction of Γ by ¬A if it is a maximal
subset of Γ and is consistent with ¬A.
Example 3.1
Let Γ ≡ {A, A ⊃ B, B ⊃ C, E ⊃ F }. It can be proved that Γ ⊢ C holds. Let ¬C be a
user’s rejection. It cab be verified that there are three maximal contractions:
{A, A ⊃ B, E ⊃ F }, {A, B ⊃ C, E ⊃ F }, {A ⊃ B, B ⊃ C, E ⊃ F }.

Lemma 3.1
If Γ ⊢ A and Λ is a maximal contraction of Γ by ¬A, then there exists a user’s rejection
M of Γ by A and M |= ¬A holds.
Proof: The proof is directly from the definition.

4

The R-calculus

The purpose of this section is to build an inference system about logical connectives to
remove the laws which is not consistent with a given user’s rejection. It is called R-calculus.
For a given Γ ⊢ A, the R-calculus is used to derive all maximal contractions of Γ by ¬A.
In fact, if Γ is not consistent,
the R-calculus is still employed to derive all maximal subsets of Γ that is consistent
with ¬A.
In order to define the calculus, for a formal theory Γ, a concept called R-condition of
Γ is to be introduced. The R-condition is a kind of mirror reflection of the concept of
T-condition used in the forcing theory [8].
Definition 4.1 R-condition of Γ
Let Γ be a specification and ∆ be a finite consistent set of atomic formulas and the
negations of atomic formulas. ∆ is called an R-condition of Γ, if and only if for every
A ∈ ∆, Γ ⊢ ¬A holds.
Lemma 4.1
Let Γ be a specification and ∆ be a R-condition of Γ. If A ∈ ∆, then A is a user’s
rejection of Γ.
Proof. The proof is directly from the definition.
Definition 4.2 R-configuration
∆|Γ
is called a R-configuration, if and only if Γ is a specification and ∆ is a R-condition of Γ.
The R-configuration ∆|Γ is read as ∆ overrides Γ.
∆ and Γ can be written as sequences, such as A, B, ∆1 and A, B, Γ′ , etc. Let Delta be
A1 , A2 , · · · , An . According to the above definitions, the R-configuration ∆|Γ implies that
Γ ⊢ ¬A1 ∧ ¬A2 , · · · , ∧An holds. Let its proof tree be denoted by T.
Definition 4.3 R-transition
∆ | Γ =⇒ ∆′ | Γ′
is called a R-transition. It means that the configuration ∆ | Γ is transformed to ∆′ | Γ′ .
=⇒∗ denotes a sequence of the transitions. ∗ denotes finite times of transitions but
also infinite times and 0 times of transitions. The following R-transition
∆ | A, Γ =⇒ ∆ | Γ
means that ∆ | Γ, A is transformed to ∆ | Γ, and A is deleted during the transition.

R-calculus contains four kinds of transformation rules. They are structural rules, the
R-axiom, the R-cut rule and the rules of logical connectives. As mentioned before, for the
writing simplicity, the proof tree is omitted from 7→ and =⇒.
Structural rules
Definition 4.4
Contraction
∆ | A, A, Γ =⇒ ∆ | A, Γ

A, A, ∆ | Γ =⇒ A, ∆ | Γ

Exchange
∆ | A, B, Γ =⇒ ∆ | B, A, Γ

A, B, ∆ | Γ =⇒ B, A, ∆ | Γ

The contraction rules mean that the same formulas occurring on one side can be
contracted to one. The exchange rules say that a formula can be moved from one position
to another within one side of a configuration.
Definition 4.5 R-axiom
A, ∆ | ¬A, Γ =⇒ A, ∆ | Γ
The R-axiom means that if A (the atomic formula or the negation of atomic formula)
occurs on the left hand side and its negation ¬A occurs on the right hand side, then ¬A
must be deleted.
Definition 4.6 R-cut rule
Γ1 , A ⊢ B

A 7→ B B, Γ2 ⊢ C ∆ | C, Γ2 =⇒ ∆ | Γ2
∆ | Γ1 , A, Γ2 =⇒ ∆ | Γ1 , Γ2

Where Γ = Γ1 , A, Γ2 and ∆ = ¬C, ∆′ . The R-cut means that C is an atomic formula
or the negation of an atomic formula, and C is not consistent with ∆. Furthermore, B is
a lemma used in the proof of C, A is contained in Γ and is the necessary premise of B. In
this circumstance, A must be eliminated.
Logical rules
Definition 4.7 R-∧ rule
∆ | A, Γ =⇒ ∆ | Γ
∆ | A ∧ B, Γ =⇒ ∆ | Γ

∆ | B, Γ =⇒ ∆ | Γ
∆ | A ∧ B, Γ =⇒ ∆ | Γ

A occurring in the numerator of the R-∧ rule means that ∆ ⊢ ¬A holds. According
to the ∧ rule of G system, ∆ ⊢ ¬A ∨ ¬B holds. That is ∆ ⊢ ¬(A ∧ B) holds. Therefore,
if A is deleted, then A ∧ B must be deleted. Similarly, for the rule on the right, if B is
deleted, then A ∧ B must be deleted.

Definition 4.8 R-∨ rule
∆ | A, Γ =⇒ ∆ | Γ
∆ | B, Γ =⇒ ∆ | Γ
∆ | A ∨ B, Γ =⇒ ∆ | Γ
Since A and B occurring in the numerator of R-∨ rule are going to be deleted, ∆ ⊢ ¬A
and ∆ ⊢ ¬B hold. According to the ∨ rule of the G system, ∆ ⊢ ¬A ∧ ¬B holds. The
later implies ∆ ⊢ ¬(A ∨ B). Therefore, A ∨ B must be deleted.
Definition 4.9 R-⊃ rule
∆ | ¬A, Γ =⇒ ∆ | Γ
∆ | B, Γ =⇒ Γ
∆ | A ⊃ B, Γ =⇒ ∆ | Γ
The R-⊃ rule holds since (A ⊃ B) ≡ (¬A ∨ B).
Definition 4.10 R-∀ rule
∆ | A[t/x], Γ =⇒ ∆ | Γ
∆ | ∀xA, Γ =⇒ ∆ | Γ
where t is a term and is free in A for x.
Since A[t/x] occurring in the numerator of the R-∀ rule is to be deleted, ∆ ⊢ ¬A[t/x]
holds. It implies ∆ ⊢ ¬∀xA[x]. Thus, ∀xA[x] must be deleted. R-∀ means that if A[t/x]
is not consistent with ∆, then ∀xA(x) can not be consistent with ∆.
Definition 4.11 R-∃ rule
∆ | A[y/x], Γ =⇒ ∆ | Γ
∆ | ∃xA, Γ =⇒ ∆ | Γ
y is an eigenvariable and it does not occur in the denominator of the rule.
If A[y/x] is to be deleted in the numerator of the R-∃ rule, then ∆ ⊢ ¬A[y/x]. According to the ∃ rule of the G system, ∆ ⊢ ¬∃xA(x) holds. Therefore, ∃xA(x) must be
deleted. This rule means that for any eigenvariable y, if A[y/x] is not consistent with ∆,
then ∃xA(x) is not consistent with ∆.
Definition 4.12 R-¬ rule
∆ | A, Γ =⇒ ∆ | A′ , Γ
A and A′ are defined as below:
A
A′

¬(B ∧ C)
¬B ∨ ¬C

¬(B ∨ C)
¬B ∧ ¬C

¬¬B
B

¬(B ⊃ C)
B ∧ ¬C

¬∀x.B
∃x.¬B

¬∃x.B
∀x.¬B

R-¬ rule is an expansion rule. ¬A occurring on the left of the long right arrow is
substituted by its equivalent A′ , and the ”¬” goes to the next level.

Definition 4.13 R-calculus
R-calculus is the set which consists of the structural rules, the R-axioms, the R-cut
rule, the R-∧ rule, the R-∨ rule, the R-⊃ rule, the R-∀ rule, the R-∃ rule, and the R-¬
rule.
An R-configuration ∆ | Γ is called an R-termination if there does not exist an R-rule
that can be applied to ∆ | Γ with the exception of the structural rules.
In summary, every R-configuration ∆|Γ consists two parts: the left part ∆ is a finite
consistent set of atomic formulas and the negations of atomic formulas, the right part Γ
is a finite set of sentences which may not be consistent. For every A ∈ ∆, A is a user’s
rejection of Γ. The R-calculus is an inference system. It can be used to eliminate those
laws which are not consistent with
∆. The principles of eliminating are as below: The law A of Γ (on the right hand side
of |) is to be eliminate if its negation ¬A occurs in ∆ (on the left hand side of |). If A of Γ
is a compound sentence, then whether A is to be eliminated depends on the eliminations
of the components of A and the meaning of the logical connective occurring in A. The
rule for a logical connective of R-calculus is a mirror reflection of the rule for the same
logical connective of the first order inference system.

5

Some Examples

The following three examples are given to show how the R-calculus can be used to delete
the laws of Γ which is not consistent with its user’s rejection.
Example 5.1
Let Γ ≡ {∀x.A(x), Γ′ } and ∆ ≡ {¬A[c]} holds. The latter means that we must accept
¬A[c], where c is a constant. According to the R-axiom,
¬A[c] | A[c], Γ′ =⇒ ¬A[c] | Γ′
holds. By the R-∀ rule,
¬A[c] | A[c], Γ′ =⇒ ¬A[c] | Γ′
¬A[c] | ∀xA(x), Γ′ =⇒ ¬A[c] | Γ′
holds. Thus, it is proved by the R-calculus that ∀xA(x) is not consistent with ¬A[c]. and
it should be eliminated from Γ.
✷
The following example demonstrates how to use the R-cut rule.
Example 5.2 Consider the example given in the beginning of the paper. Let
Γ ≡ {A, A ⊃ B, B ⊃ C, E ⊃ F }
Γ ⊢ C holds. Suppose ¬C is a user’s rejection. According to the definition, there exists
three maximal contraction of Γ by ¬C:
{A, A ⊃ B, E ⊃ F },

{A, B ⊃ C, E ⊃ F }

{A ⊃ B, B ⊃ C, E ⊃ F }.

In fact, each one of the above three can be derived by the R-calculus. Consider
{A, A ⊃ B, E ⊃ F } first. Let
Γ1 ≡ {A, A ⊃ B} Γ2 ≡ {E ⊃ F }.
By the G system, both
Γ1 , B ⊃ C ⊢ C and C, Γ2 ⊢ C
hold. According to the definition 2.1, B ⊃ C is the necessary premise of C and B ⊃ C 7→ C
holds.
¬C | C, Γ2 =⇒ ¬C | Γ2
holds by the R-axiom. the R-cut rule is then applied and
¬C | Γ1 , B ⊃ C, Γ2 =⇒ ¬C | Γ1 , Γ2
hold. Here Γ1 , Γ2 is just {A, A ⊃ B, E ⊃ F }.
Consider the second maximal contraction {A, B ⊃ C, E ⊃ F }. Let
Γ1 ≡ {A}

Γ2 ≡ {B ⊃ C, E ⊃ F }.

By the G system,
Γ1 , A ⊃ B ⊢ B and B, Γ2 ⊢ C hold.
Notice that A ⊃ B is the premise of B and is in Γ. Thus, A ⊃ B 7→ B holds. According
to the R-axiom,
¬C | C, Γ2 =⇒ ¬C | Γ2
holds. Thus, the R-cut rule is applied and
¬C | Γ1 , A ⊃ B, Γ2 =⇒ ¬C | Γ1 , Γ2
holds. Here Γ1 , Γ2 is {A, B ⊃ C, E ⊃ F }. Finally, Let
Γ1 ≡ ∅ Γ2 ≡ {A ⊃ B, B ⊃ C, E ⊃ F }.
Using the similar proof strategy, the third maximal contraction {A ⊃ B, B ⊃ C, E ⊃
F } can derived by the R-calculus.
✷
In the above two examples, Γ is a finite consistent set of laws. The following example
shows that if Γ is not consistent, the R-calculus still works to deduce all of maximal subset
of Γ which is consistent with ∆. :
Example 5.3
Let ∆ = {x = x} and Γ = {f (x) = y, f (y) = z, ¬(f (f (x)) = z)}. Obviously, Γ is
not consistent. But the R-cut rule can be applied to deduce the maximal subsets which is
consistent with ∆. For example, let Γ1 = {f (x) = y}, Γ2 = {¬(f (f (x)) = z)}. First,
Γ1 , (f (y) = z) ⊢ f (f (x)) = z and (f (f (x)) = z), Γ2 ⊢ ¬(x = x)

holds. It is proved that (f (y) = z) is the necessary premise of f (f (x)) = z. According to
the R-axiom,
(x = x) |¬(x = x) =⇒ (x = x)|∅
holds. Therefore, by the R-cut rule,
(x = x)| {f (x) = y, f (y) = z, ¬(f (f (x)) = z)} =⇒ (x = x)| {f (x) = y, ¬(f (f (x)) = z)}
holds. It can be verified that {f (x) = y, ¬(f (f (x)) = z)} is a maximal subset of Γ and is
consistent with x = x.
✷

6

The Reachability and Completeness

¿From the examples given in the last section, we have found that for the given Γ and ∆,
every maximal contraction of Γ by ∆ can be deduced by the R-calculus. This fact is called
the reachability of the R-calculus.
Definition 6.1 R-reachabilty
Let ∆ | Γ be any given R-configuration, Γ be a specification, and ∆ be an R-condition
of Γ. The R-calculus is reachable, if and only if for any given maximal contraction Γ′ of
Γ by ∆, there exists an R-transition sequence such that
∆ | Γ =⇒∗ ∆ | Γ′
holds, where ∆ | Γ′ is an R-termination.
Lemma 6.1
Let ∆ | Γ be a given R-configuration, Γ be a specification, and ∆ be an R-condition of
Γ. If Γ1 is a maximal contraction of Γ by ∆, then there exists a sequence of R-transitions,
such that
∆ | Γ =⇒∗ ∆ | Γ1
holds.
Proof. Consider the simple case that ∆ contains only one element, ∆ ≡ {¬A}, and A is
an atomic formula or the negation of atomic formula. Γ ⊢ A holds. Let Γ1 be a maximal
contraction of Γ by ¬A, and let Γ2 ≡ Γ − Γ1 .
The aim is to prove that for any B ∈ Γ2 , B will be eliminated by the R-calculus. To
do so, let Γ3 ≡ Γ2 − {B}. Thus, Γ = Γ3 , B, Γ1 . First, Γ3 , B ⊢ B holds. Second, B on the
left of ⊢ is the necessary premise of B on the right of ⊢. Since Γ1 is a maximal contraction
of Γ by ¬A, Γ1 , B ⊢ A holds.
¬A | A, Γ1 =⇒ ¬A | Γ1
is an application of the R-axiom. By the R-cut rule,
Γ3 , B ⊢ B

B 7→ B Γ1 , B ⊢ A ¬A | A, Γ1 =⇒ ¬A | Γ1
¬A | Γ3 , B, Γ1 =⇒ ¬A | Γ3 , Γ1

Thus, B is eliminated. Therefore, every law of Γ2 should be eliminated by the Rcalculus.
✷
The converse of the lemma is not true. For every sequence of R-transitions:
∆ | Γ =⇒∗ ∆′ | Γ′
where ∆′ | Γ′ is an R-termination, Γ′ may not be a maximal contraction of Γ by ∆.
Consider the following example:
Example 6.1 Let
Γ ≡ {A, A ⊃ B, B ⊃ C, A ⊃ E, E ⊃ C}
Γ ⊢ C holds. Suppose that C is rejected by the users. Using the R-cut rule, We can
eliminate A ⊃ B. And then, since
A, A ⊃ E, E ⊃ C ⊢ C
we apply the R-cut rule again and eliminate A. Thus, we have:
{B ⊃ C, A ⊃ E, E ⊃ C}.
The above set is not a maximal contraction of Γ by ¬C. The maximal contraction is
{A ⊃ B, B ⊃ C, A ⊃ E, E ⊃ C}.
✷
Lemma 6.2
Let A | Γ be an R-configuration, A be an atomic formula or the negation of an atomic
formula. If Γ is consistent with A, then A|Γ is an R-terminated configuration.
Proof: Since Γ is finite, Γ can be written as A1 ∧ · · · ∧ An . Let r(Γ) be the rank of Γ [1].
The proof is given by induction on r(A1 ∧ · · · ∧ An ) as below:
If r(Γ) = 1, Γ is an atomic formula. It can not be eliminated since it is consistent with
A. By the definition, A|Γ is R-termination.
Suppose that the lemma holds for r(Γ) < k. Consider the case of r(Γ) = k. Let Γ be
B, Γ′ , where r(Γ′ ) < k, and Γ′ is consistent with A. B can be one of the following cases:
1. B is an atomic formula. B can not be ¬A since Γ is consistent with A. Therefore,
A|Γ is an R-termination.
2. B is B1 ∨B2 . According to the R−∨ rule, B is eliminated if and only if B1 in A|B1 , Γ′
is to be eliminated, and B2 in A|B2 , Γ′ is also to be eliminated. Since B1 , Γ′ with A,
and r(B1 , Γ′ ) < k holds. According to the inductive hypothesis, B1 in A|B1 , Γ′ can
not be eliminated. Similarly, B2 in A|B2 , Γ′ is also not eliminated. Therefore, A|Γ
is an R-termination.
3. Similarly, we can prove the cases that B is B1 ∧ B2 and B is B1 ⊃ B2 .

4. B is ∀xB1 . According to the R − ∀ rule, B1 is eliminated if and only if B1 [t/x]
in A|B1 [t/x], Γ′ is to be eliminated. Since {B1 [t/x], Γ′ } is consistent with A, And
r(B1 [t/x], Γ′ ) < k holds. According to the inductive premise, B1 [t/x] in B1 [t/x], Γ′
can not be eliminated. Thus, A|Γ is an R-termination.
5. Similarly, we can prove the case of that B is ∃x.B1 .
6. Finally, we prove that every one of A1 , · · · , An in Γ can not be eliminated by the Rcut rule. For each Ak , k = 1, · · · , n, the R-cut rule is applied only in the circumstance
that there exists B, such that A1 , · · · , Ak−1 , Ak ⊢ B, Ak 7→ B, and B, Ak+1 , · · · , An ⊢
P holds, and P in A|P , and Ak+1 , · · · , An is to be eliminated. Since Γ is consistent
with A, {P, Ak+1 , · · · , An } is also consistent with A, Furthermore, P is an atomic
formula or the negation of an atomic formula. We know that r(P, Ak+1 , · · · , An ) ≤ k
holds. According to the item 1, we know that A|P, Ak+1 , · · · , An is an R-termination.
So P can not be eliminated. Therefore, the R-cut rule can not be applied.
✷
Theorem 6.1
The R-calculus is reachable.
Proof: Let ∆ | Γ be a given R-configuration, where Γ is a finite set of sentences, and ∆
is an R-condition of Γ. Consider the simple case that ∆ contains only one element A. Let
Γ′ be a maximal contraction of Γ by A. For every B in Γ − Γ′ , by the lemma 6.1, there
exists a sequence of R-transitions at the end of which B is eliminated. Since Γ − Γ′ is a
finite set of sentences, the above the sequences can be concatenated to form a sequence of
R-transitions:
A | Γ =⇒∗ A | Γ
where A | Γ′ is an R-termination by the lemma 6.2.

✷

Definition 6.2 R-completeness
Let ∆ | Γ be any R-configuration, where Γ is a specification and ∆ is R-condition of
Γ.
The R-calculus is R-complete, if and only if for a given R-configuration ∆ | Γ and
every ideal user’s rejection M, if M |= ∆, then there exists a transition sequence:
∆ | Γ =⇒∗ ∆ | Γ′ ,
where ∆ | Γ′ is a termination and
Γ′ = {A |M |= A and A ∈ Γ}
holds.

✷

Theorem 6.2
The R-calculus is R-complete.
Proof: This theorem is a corollary of the lemma 3.1 and the theorem of R-reachability.
✷

7

Related works

In 1985, Gärdenfors and his colleagues introduced their theory of changes [4]. The theory
addresses the proof-theoretic concepts of the expansion, the contraction, and the revision
in the scope of propositional logic. The maximal contraction given here can be viewed a
special kind of AGM’s contraction, but in the scope of the first order logic. The user’s
rejection is a corresponding model-theoretic concept of the maximal contractions [6,9].
The AGM’s theory focuses on building the systems of the propositions of the expansion,
the contraction and the revision, and on studying the properties of these systems [4,5]. The
principal difference between the AGM’s theory and The R-calculus is as the following: the
aim of designing the R-calculus is to build a transition system that can deduce all maximal
contractions from a given formal theory Γ and its user’s rejection A.
Finally, it is believed that using the methods given in [2], certain proper type theories
based on the R-calculus can be constructed and the corresponding interactive tools can
be implemented to develop the specifications .
Acknowledgement: The author would like to take this chance to thank Dr. Zhang
Yuping. His counter examples helped the author to find the current version of the definition
of the necessary premise.
References
[1] Gallier, J.H., Logic for Computer Science, foundations of automatic theorem proving.
John Wiley & Sons, 1987, 147-158, 162-163, 197-217.
[2] Paulson, L., Logic and Computations, Cambridge University Press, 1987, 38-50.
[3] Flew, A., A Dictionary of Philosophy, Pan Books Ltd, 1979.
[4] Alchourrón, C.E., Gärdenfors, R. and Makinson, D., On the logic of theory change:
partial meet contraction and revision functions, The Journal of Symbolic Logic,
Vol.50, No.2, June, 1985.
[5] Gärdenfors, P., Knowledge in Flux, The MIT Press, 1988.
[6] Li, W., An Open Logic System, Science in China, Series A, March, 1993.
[7] Shoenfield, J.R., Mathematical Logic, Addison-Wesley, Reading, Mass, 1967, 74-75.
[8] Forcing, Burgess, Handbook of mathematical logic, edited by J., Barwise, NorthHolland Publishing Company, 1977.
[9] Li W., A Logical Framework for the evolution of Specifications. ESOP’94, LNCS 788,
1994, Springer-Verlag.
[10] Burstall, R. and Goguen J.A., Putting theories together to make specifications, Proc.
5th. IJCAI Cambridge, Mass, 1045-1058 (1977).
[11] Bjørner, D., and Jones, C., Formal specification and Software Development, Prentice
Hall International, 1983.

[12] Nordström, B., and Smith, J., Propositions and specifications of programs in MartinLöf’s type theory, BIT 24 (1984), pp 288-301.
[13] D. Sannella and A. Tarlecki, Toward formal development of programs from algebraic
specifications: implementations revisited. Acta Informatica 25,233-281(1988).

