1. Introduction
The AGM postulates ([1],[4-6]) are for the revision of a theory by a formula and the DP postulates ([2]) are for the iterated revision
The -calculus ([3]) gave a Gentzen-type deduction system to deduce a consistent theory from any theory where should be a maximal consistent subtheory of which includes as a subset, where is an -configuration, is a consistent set of formulas, and is a consistent sets of literals (atomic formulas or the negation of atomic formulas). It was proved that if is deducible and is an -termination, i.e., there is no -rule to reduce to another -configuration then is a pseudo-revision of by
The -calculus has the following features:
● is a finite set of literals (propositional variables or the negation of propositional variables);
● is a set of formulas;
● are not sufficient for pseudo-revision, and is introduced to deduce into a consistent set of formulas including
● the soundness theorem holds, that is, if is provable then is a pseudo-revision of by and
● the completeness theorem holds, that is, if is a pseudo-revision of by then is provable.
Because each rule in the -calculus consists of the statements of form
the -calculus is based on pseudo-revision, i.e., to contract from if is inconsistent, which makes the -calculus not preserve the minimal change principle.
Given two theories and a pseudo-revision of by is a consistent subset of including (if is inconsistent; otherwise,).
We shall give two -calculi such that
● in one -calculus, say for any consistent formula set and finite formula set there is a consistent formula set such that is provable and is a pseudo-revision of by (the soundness theorem); and conversely, given any pseudo-revision of by is provable (the completeness theorem);
● in another -calculus, say for any consistent formula set and finite formula set there are consistent formula sets and such that
◦ is provable
◦ is a pseudo-revision of by
◦ and
◦ there is no subformula of contradictory to (the soundness theorem);
and conversely, given any pseudo-revision of by there is a consistent formula set such that is provable, and is contradictory to no subformula of (the completeness theorem).
The -calculi are different from the -calculus in [3] as follows:
◊ is any set of formulas;
◊ The cut-rule in the -calculus is eliminated in the -calculi;
◊ Because -rule in the -calculus is not sufficient for reducing
to either or the - calculus is not complete with respect to the pseudorevision of by In the new -calculi, we split into two deduction rules and according to whether is consistent with or not. The reason is given as follows.
Given a consistent theory and formulas
is inconsistent if and only if
and are inconsistent; and if either or is inconsistent then is inconsistent; and if is inconsistent then we cannot deduce that either or is inconsistent, and what we have is that is inconsistent if and only if either is inconsistent or is inconsistent. Formally,
(1)
(2)
(3)
where and denote that is consistent and inconsistent, respectively. Therefore, we use
in and instead of
in the -calculus.
In we use a rule
to deduce to if are consistent. In, we shall give a deduction rule to reduce to the atomic cases where
with a cost that we cannot prove that if is provable then is a pseudo-revision of by Instead we shall prove that if is provable then is a pre-revision of by that is, there is a consistent theory such that 1) is a pseudo-revision of by 2) and 3) no subformula of is contradictory to
The paper is organized as follows: the next section gives the -calculus in [3] and basic definitions; the third section defines an -calculus for the pseudorevision and proves that is sound and complete with respect to the pseudo-revision; the fourth section defines another -calculus for the pre-revision and prove that is sound and complete with respect to the pseudo-revision, and the last section concludes the whole paper.
2. The -Calculus
The -calculus is defined on a first-order logical language. Let be a logical language of the first-order logic; formulas and sets of formulas (theories), where is a set of atomic formulas or the negations of atomic formulas, and is called an R-configuration.
The -calculus consists of the following axiom and inference rules:
where in means that occurs in the proof tree of from and and in is a term, and is free in for.
The -calculus is in the first-order logic. In the following we discuss the -calculi in the propositional logic.
Let be a logical language of the propositional logic which contains the following symbols:
propositional variables:
logical connectives:
Formulas are defined as follows:
Definition 2.1. Given a consistent set of formulas and a finite consistent set of formulas, a consistent set of formulas is a pseudo-revision of by if (if is consistent), or (if is inconsistent then) satisfies the following conditions:
1)
2) and 3) there is a such that is inconsistent.
Each pseudo-revision can be generated by the following procedure: given any consistent set and finite consistent set assume that is ordered by a linear ordering (without loss of generality, assume that), define
Let Then, is a subset of such that and is consistent.
Lemma 2.2. is a pseudo-revision of by Moreover, Let be the least such that
Then,
Definition 2.3. Given a consistent set of formulas and a finite consistent set of formulas, a consistent set of formulas is a pre-revision of by if there is a pseudo-revision of by such that 1)
2) and 3) no subformula of is contradictory to
Each pre-revision can be generated by the following procedure: given any consistent set and finite consistent set assume that define
where
where is the empty string.
Let and be the pseudo-revision of by in the same ordering as Then, we have the following Lemma 2.4. Let be the least such that Then, for any and for any is a subformula of
Lemma 2.5. is a pre-revision of by such that and no subformula of is contradictory to
Proof. Let be the least such that Then,
We prove that for any with and by induction on
Let and Then,
We prove by induction on the structure of that and
If and then is inconsistent, a contradiction to the choice of
If and then and
If and is consistent then and are consistent, and by the induction assumption,
and hence,
If and is consistent then either or is consistent.
If and are consistent. then by the induction assumption,
and hence,
If is inconsistent and is consistent. then and by the induction assumption, and hence, because and (is inconsistent, and hence, for any formula).
Similar for the case that is consistent and is inconsistent.
Similarly we can prove that for any with
3. The -Calculus
In this section we give an -calculus which is sound and complete with respect to the pseudo-revision, where the decision of whether is consistent is needed so that if is consistent then is provable; otherwise, is provable.
Let be any consistent sets of formulas.
Definition 3.1. is a term; and is a statement, where and; and
is a deduction rule, where are statements.
has the following deduction rules:
Definition 3.2. is provable if there is a sequence
of statements such that 1)
2) and 3) for each is either an axiom or deduced from the previous statements by the deduction rules.
For example, the following
is a proof and so is provable.
Also, the following
is a proof and so is provable.
Theorem 3.3. For any consistent sets of formulas and formula if is provable then is inconsistent; and if is provable then is consistent.
Proof. If is provable then is used and is consistent.
If is provable then we prove that i.e., is inconsistent, by the induction on the length of a proof of and the cases that the last inference rule is used.
If the last rule used is then and i.e.,
If the last rule used is then and i.e.,
If the last rule used is then, and . By the induction assumption, , and hence, i.e.,
If the last rule used is then and By the induction assumption, and hence, i.e.,
If the last rule used is then and
By the induction assumption, , , and hence, i.e.,
Theorem 3.4. For any consistent sets of formulas and formula φ, if is inconsistent then is provable; and if is consistent then is provable.
Proof. If φ is consistent with then by, is provable;
Assume that φ is inconsistent with Δ. We prove by the induction on the structure of φ that is provable.
If φ = p then and by, is provable.
If then and by is provable.
If then there are two subcases: is inconsistent with or is consistent with In the first subcase, by the induction assumption, is provable, and by is provable; and in the second subcase, is consistent and is inconsistent. By the induction assumption, is provable, and by
If then both and are inconsistent. By the induction assumption, both and are provable, and by is provable.
Theorem 3.5. For any consistent sets of formulas, if is finite then there is a set of formulas such that is provable Proof. Let
We prove the theorem by the induction on
If then by theorem 3.3, let
and satisfies the theorem.
Assume that the theorem holds for that is, there is a set such that is provable. Let
If is consistent with then is provable, where
If is inconsistent with then
because the last formula is inconsistent with
Theorem 3.6 (The soundness theorem for). If is provable then is a pseudo-revision of by
Proof. Firstly we prove that if is provable then is a pseudo-revision of by
Assume that is provable.
If then is consistent with and is a pseudo-revision of by
If then is inconsistent with φ, is provable, and is a pseudo-revision of by
Similarly, by the induction on the number of formulas in we can prove that if then is a pseudo-revision of by.
Theorem 3.7 (The completeness theorem for). If is a pseudo-revision of by then is provable.
Proof. Let be a pseudo-revision of Γ by under the ordering of Γ.
We prove by induction on that there is a formula set such that is provable, where and
If is consistent then let, and is provable, where
Assume that is inconsistent. Then, and let by theorem 3.4,
is provable.
Let Then, is provable.
4. The -Calculus
In this section we give an -calculus which is sound and complete with respect to the pre-revision, where the decision of whether is consistent is deduced by a set of -rules.
R1 is used to reduce to when is inconsistent. When is consistent, there are subformulas in which is inconsistent with we hope to reduce those subformulas into the empty string. For example, let
Then, by we have the following reduction:
and by we shall have the following one:
For the two reductions, we have
Let be a consistent set of formulas and a finite consistent set of formulas.
consists of two parts: which we use to decompose formula in if is inconsistent; and -deduction rules, which we use to decompose if is consistent.
has the following -deduction rules to reduce when is consistent:
where if is consistent then
and if is inconsistent then
The deductions for the inconsistent are the same as in minus
Definition 4.1. is provable if there is a sequence
of statements such that 1)
2) and 3) for each is either an axiom or deduced from the previous statements by the deduction rules.
We call the sequence a proof of statement.
For example, the following
is a proof and is provable.
Theorem 4.2. For any consistent sets of formulas and formula if is provable then is inconsistent; and if there is a formula such that is provable then is consistent.
Proof. If is provable then similar to the proof of theorem 3.3, is inconsistent.
Assume that there is a formula such that is provable. We prove by the induction on the length of a proof of and the cases that the last inference rule is used that is consistent.
If the last rule used is then and is provable, where Hence, is consistent.
If the last rule used is then and is provable, where . Hence, is consistent.
If the last rule used is then and there are formulas such that
and
By the induction assumption, if θ1 ≠ λ and θ2 ≠ λ then is consistent and is consistent, and therefore, is consistent.
If the last rule used is then and
where either or
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, and are consistent, and so is
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, is consistent, and so is
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, is consistent, and so is
By the proof of the theorem, we have
Theorem 4.3. For any formula sets and formula if is consistent then
Proof. We prove the theorem by the induction on the structure of Assume that
If then and Hence,
If then and By the induction assumption,
Hence, we have
If then either is consistent or is consistent.
If and are consistent then and By the induction assumption,
Hence, we have
If is inconsistent and is consistent then By the induction assumption, Hence, by Lemma 2.5, we have
If is consistent and is inconsistent then By the induction assumption, Hence, by Lemma 2.5, we have
Theorem 4.4. For any consistent sets of formulas and formula if is inconsistent then is provable; and if is consistent then there is a formula such that is provable.
Proof. If is inconsistent with then similar to theorem 3.5, is provable.
Assume that φ is consistent with We prove the theorem by the induction on the structure of φ.
If φ = p then and by is provable, where
If then and by is provable, where
If then φ1 is consistent with and φ2 is consistent with By the induction assumption, there are formulas such that and are provable. By we have
is provable, where
If then either or is consistent. By the induction assumption, if is consistent then there is a formula such that and if is consistent then there is a formula such that Then, by is provable, where
Remark. In fact, in theorem 4.3, if is consistent then there is a formula such that is provable.
By Theorem 4.3, we have the following Theorem 4.5. (The soundness theorem for). If is provable then is a pre-revision of by Δ.
Proof. We only prove that no subformula ξ of Ξ is contradictory to Δ.
Assume that there is a subformula ξ of some formula in Ξ such that Let such that
If is inconsistent then a contradiction.
If is consistent then by Lemma 3.5,
and for any subformula ξ of θ, if then, by the definition of θ, ξ is replaced by in θ, a contradiction to the assumption that ξ is a subformula of θ.
Theorem 4.6. (The completeness theorem for Γ). If Ξ is a pre-revision of Γ by Δ then is provable.
Proof. The proof is similar to theorem 3.7 and omitted.
5. Conclusion
This paper gave two -calculi which are sound and complete with respect to the pseudo-revision and prerevision, respectively. The calculi are of Gentzen-type, in which each statement is of form Different orderings of give different results of revision Correspondingly, if is irreducible, that is, no deduction rule can be used to reduce then may be a minimal change of by A further work is to give an -calculus such that if is irreducible then is consistent and is a minimal change of by that is, for any with is inconsistent.
NOTES