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 ![](https://www.scirp.org/html/5-1680081\7f0f8144-c4aa-4107-8fb3-e690f78aab90.jpg)
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 ![](https://www.scirp.org/html/5-1680081\21184d93-eec5-4551-9506-0352a03e828a.jpg)
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 ![](https://www.scirp.org/html/5-1680081\d7ef63a5-67af-44a5-8b2d-88097d96df0b.jpg)
● 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
![](https://www.scirp.org/html/5-1680081\b6ad3a64-6701-4eba-8af9-7ea82cf80e97.jpg)
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 ![](https://www.scirp.org/html/5-1680081\2949518c-672a-4f1d-ad66-85e9a8f0d8bc.jpg)
◦
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
![](https://www.scirp.org/html/5-1680081\b7351f4a-17f3-4827-904b-00ae28bb484e.jpg)
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
![](https://www.scirp.org/html/5-1680081\dfb12a12-c984-4df6-bfbd-c300b4047318.jpg)
in
and
instead of
![](https://www.scirp.org/html/5-1680081\5a50461e-203d-406b-a3d4-f2441afcdd15.jpg)
in the
-calculus.
In
we use a rule
![](https://www.scirp.org/html/5-1680081\82ec9ca2-40c0-4f94-bf12-057d0966584e.jpg)
to deduce
to
if
are consistent. In
, we shall give a deduction rule to reduce
to the atomic cases where
![](https://www.scirp.org/html/5-1680081\a15fa0b7-e9e6-4f18-be28-cd759e6f59d7.jpg)
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 ![](https://www.scirp.org/html/5-1680081\d82302fc-93a5-42bb-bfb3-0b70c03d98c8.jpg)
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:
![](https://www.scirp.org/html/5-1680081\e6d827e0-7d8d-437b-9edd-57fb443ea86d.jpg)
![](https://www.scirp.org/html/5-1680081\7bd3f88e-f686-4bfe-b794-2b136fe27b22.jpg)
![](https://www.scirp.org/html/5-1680081\8574be93-9070-4022-98aa-1c94c6d5f733.jpg)
![](https://www.scirp.org/html/5-1680081\2d931703-72f6-43a6-a4f7-d1a5fb35fff9.jpg)
![](https://www.scirp.org/html/5-1680081\48db17f1-f792-446a-9009-03e373b219de.jpg)
![](https://www.scirp.org/html/5-1680081\0904ee9a-f82c-4dc7-9738-4c10438de660.jpg)
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: ![](https://www.scirp.org/html/5-1680081\b17dbf49-a032-4fdc-b060-a54b451c4bc1.jpg)
logical connectives: ![](https://www.scirp.org/html/5-1680081\3a67a403-83a5-4097-b00c-0f157b30aba2.jpg)
Formulas are defined as follows:
![](https://www.scirp.org/html/5-1680081\e55f7027-1a18-4b61-9808-53f79ebafaee.jpg)
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) ![](https://www.scirp.org/html/5-1680081\7a90fd71-b08c-4973-8b0a-66f53facdb49.jpg)
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
![](https://www.scirp.org/html/5-1680081\ab4f78fc-fc8c-4ed4-8a26-20ad474781f2.jpg)
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, ![](https://www.scirp.org/html/5-1680081\3180fca9-345e-4a98-ae9f-1ca43c702182.jpg)
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) ![](https://www.scirp.org/html/5-1680081\2d93f639-2e54-44d9-a0e4-ec9a4bdf330a.jpg)
2)
and 3) no subformula
of
is contradictory to ![](https://www.scirp.org/html/5-1680081\2e80c9b8-5ec2-4ec3-92bd-fc7751885c3f.jpg)
Each pre-revision
can be generated by the following procedure: given any consistent set
and finite consistent set
assume that
define
![](https://www.scirp.org/html/5-1680081\47af592b-5a03-464a-bd7d-2fadfc203880.jpg)
where
![](https://www.scirp.org/html/5-1680081\e4e08bab-e70b-4f93-b085-15d006cf89c0.jpg)
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 ![](https://www.scirp.org/html/5-1680081\e6c9c149-4ad5-46bd-b801-cbb9ec624852.jpg)
Lemma 2.5.
is a pre-revision of
by
such that
and no subformula of
is contradictory to ![](https://www.scirp.org/html/5-1680081\7c0e0ff9-f2fc-490d-add3-726e9d90e643.jpg)
Proof. Let
be the least
such that
Then,
![](https://www.scirp.org/html/5-1680081\f408b4ca-b2b4-473c-9713-4ae83eb501f5.jpg)
We prove that for any
with
and
by induction on ![](https://www.scirp.org/html/5-1680081\18523e35-2d58-4cf7-8d6a-5bd4d7136f39.jpg)
Let
and
Then,
We prove by induction on the structure of
that
and ![](https://www.scirp.org/html/5-1680081\3157fd54-71ec-47b5-85c1-78ef0c1fc255.jpg)
If
and
then
is inconsistent, a contradiction to the choice of ![](https://www.scirp.org/html/5-1680081\fcd241f3-2e8a-47c9-9fca-140e330e91d2.jpg)
If
and
then
and ![](https://www.scirp.org/html/5-1680081\296e165e-904e-4968-bd91-7d152a57a21d.jpg)
If
and
is consistent then
and
are consistent, and by the induction assumption,
![](https://www.scirp.org/html/5-1680081\5c3db317-5412-4046-8f12-035c7ebfb6fa.jpg)
![](https://www.scirp.org/html/5-1680081\9ef914fa-70f1-485e-a97e-bfbbf3bb6680.jpg)
and hence,
![](https://www.scirp.org/html/5-1680081\b708f5bd-09cb-416a-a7f2-ecb836f88e24.jpg)
If
and
is consistent then either
or
is consistent.
If
and
are consistent. then by the induction assumption,
![](https://www.scirp.org/html/5-1680081\74d24a96-6eda-41b8-8606-2698f5f3f04c.jpg)
![](https://www.scirp.org/html/5-1680081\556bfa13-d88c-4e17-a288-610b5059db8e.jpg)
and hence, ![](https://www.scirp.org/html/5-1680081\8f9dee31-1208-48f4-a5fd-90efdc80b39c.jpg)
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 ![](https://www.scirp.org/html/5-1680081\9b3722db-b8f5-4c14-89fc-0b4792bbf43c.jpg)
3. The
-Calculus ![](https://www.scirp.org/html/5-1680081\8afe192f-a85a-44f3-8d3f-83790b0ebe61.jpg)
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 ![](https://www.scirp.org/html/5-1680081\9ac90695-6ad8-49f2-862b-def2fdb865f3.jpg)
is a deduction rule, where
are statements.
has the following deduction rules:
![](https://www.scirp.org/html/5-1680081\069d2dea-d506-497e-86c2-38269d21dfc8.jpg)
![](https://www.scirp.org/html/5-1680081\ae2e94dd-aa5b-4b08-9256-59db413f63a9.jpg)
![](https://www.scirp.org/html/5-1680081\6c353b2c-83c8-4ac5-9fb2-a17b6993521d.jpg)
![](https://www.scirp.org/html/5-1680081\7b4e704a-7e21-4465-825f-ef2e428defd1.jpg)
![](https://www.scirp.org/html/5-1680081\1f7f2152-3f15-4d2b-86a2-aa32b3933732.jpg)
![](https://www.scirp.org/html/5-1680081\c70cb51a-d3a1-466d-8a65-09afb46d632d.jpg)
Definition 3.2.
is provable if there is a sequence
![](https://www.scirp.org/html/5-1680081\227f4885-5631-4978-8f00-574f43e654ad.jpg)
of statements such that 1) ![](https://www.scirp.org/html/5-1680081\ae1d57dc-dadd-4ab4-8b4c-f36e44f6563f.jpg)
2)
and 3) for each
is either an axiom or deduced from the previous statements by the deduction rules.
For example, the following
![](https://www.scirp.org/html/5-1680081\4b618296-f318-4f09-8a07-4fa9f91a4d88.jpg)
is a proof and so
is provable.
Also, the following
![](https://www.scirp.org/html/5-1680081\f4e52138-d504-4d9f-a829-b2e996005097.jpg)
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., ![](https://www.scirp.org/html/5-1680081\595ba2b7-2c10-4aba-86b9-a7fa35200e8f.jpg)
If the last rule used is
then
and
i.e., ![](https://www.scirp.org/html/5-1680081\917eca8b-21eb-4601-b1d6-8f056722904a.jpg)
If the last rule used is
then
, and
. By the induction assumption,
, and hence,
i.e., ![](https://www.scirp.org/html/5-1680081\3b011953-9836-407f-acf0-9fd271bc6d87.jpg)
If the last rule used is
then
and
By the induction assumption,
and hence,
i.e., ![](https://www.scirp.org/html/5-1680081\c58e90ca-53b9-4e8c-b336-ba38dd2304dd.jpg)
If the last rule used is
then
and
![](https://www.scirp.org/html/5-1680081\464e6175-3377-4a66-bf2e-9d69ce8d021f.jpg)
![](https://www.scirp.org/html/5-1680081\c8232b87-9c80-490d-ae98-1b9c44d35e0e.jpg)
By the induction assumption,
,
, and hence,
i.e., ![](https://www.scirp.org/html/5-1680081\22bfe02c-aace-48a4-80a2-9e8374c80fa5.jpg)
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
, ![](https://www.scirp.org/html/5-1680081\9ca009a8-6c1a-43c5-80c5-3c9dc67fcf0e.jpg)
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, ![](https://www.scirp.org/html/5-1680081\dd0ca39e-6b64-4cb1-ba4d-f4fd07a9b3f4.jpg)
is provable, and by ![](https://www.scirp.org/html/5-1680081\f52250f4-8279-4b13-b3f5-44efe69de1d8.jpg)
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 ![](https://www.scirp.org/html/5-1680081\94dbff81-bfee-4913-ac24-a6e42231bcb6.jpg)
We prove the theorem by the induction on ![](https://www.scirp.org/html/5-1680081\2459fca7-5c61-46c9-98d6-f8442e0f4bd2.jpg)
If
then by theorem 3.3, let
![](https://www.scirp.org/html/5-1680081\274f126f-01a7-4695-97ae-906c6306855c.jpg)
and
satisfies the theorem.
Assume that the theorem holds for
that is, there is a set
such that
is provable. Let ![](https://www.scirp.org/html/5-1680081\a1a548e5-823c-4326-900e-af9193d1d1cc.jpg)
If
is consistent with
then
is provable, where ![](https://www.scirp.org/html/5-1680081\8bb72476-cc18-44d8-99bf-bb178569d617.jpg)
If
is inconsistent with
then
because the last formula
is inconsistent with ![](https://www.scirp.org/html/5-1680081\8e46b001-91b4-41bc-9383-f038be4a2bea.jpg)
Theorem 3.6 (The soundness theorem for
). If
is provable then
is a pseudo-revision of
by ![](https://www.scirp.org/html/5-1680081\449539cb-d3dd-4495-b2a0-63c61669c532.jpg)
Proof. Firstly we prove that if
is provable then
is a pseudo-revision of
by ![](https://www.scirp.org/html/5-1680081\0075119c-0112-4635-b28a-e20f5cb0732d.jpg)
Assume that
is provable.
If
then
is consistent with
and
is a pseudo-revision of
by ![](https://www.scirp.org/html/5-1680081\fd1685bf-b50b-4f5a-afec-f028b920f88d.jpg)
If
then
is inconsistent with φ,
is provable, and
is a pseudo-revision of
by ![](https://www.scirp.org/html/5-1680081\32527044-f1f4-43b5-8b1e-3af808341d35.jpg)
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 ![](https://www.scirp.org/html/5-1680081\40b9d6f7-1cc6-4736-ba9e-c7c4f4ce0ecd.jpg)
If
is consistent then let
, and
is provable, where ![](https://www.scirp.org/html/5-1680081\be6478e3-fabb-44c0-a04a-e7d29e8a4e5c.jpg)
Assume that
is inconsistent. Then,
and let
by theorem 3.4,
is provable.
Let
Then,
is provable.
4. The
-Calculus ![](https://www.scirp.org/html/5-1680081\05410fab-34c1-49af-8244-75709cbcbe53.jpg)
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
![](https://www.scirp.org/html/5-1680081\3dd5e8d7-a05a-4de1-8c3e-3744f7560c83.jpg)
![](https://www.scirp.org/html/5-1680081\f285c7bd-abff-45cb-b409-dd475520f6e9.jpg)
Then, by
we have the following reduction:
![](https://www.scirp.org/html/5-1680081\8d694c99-72f1-4115-adb6-a7cded432081.jpg)
![](https://www.scirp.org/html/5-1680081\2d99e567-6fc0-4d5b-a18d-e0e74e3bce83.jpg)
and by
we shall have the following one:
![](https://www.scirp.org/html/5-1680081\098e9166-948b-4c51-a121-d06e34aeec3f.jpg)
![](https://www.scirp.org/html/5-1680081\5f8e18c5-ad78-4b13-bee9-34251adf9143.jpg)
For the two reductions, we have
![](https://www.scirp.org/html/5-1680081\fc6e7832-0474-4460-935a-9cb4a417748d.jpg)
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:
![](https://www.scirp.org/html/5-1680081\b113b2b5-ebb8-423a-8c5b-1db8438ba290.jpg)
![](https://www.scirp.org/html/5-1680081\b07f3907-bede-41ad-9911-d319ec32752c.jpg)
![](https://www.scirp.org/html/5-1680081\13e4985d-2a3a-466b-b4f1-127fd164b465.jpg)
![](https://www.scirp.org/html/5-1680081\66c8752a-9608-4bc5-bd98-7ffdf3803009.jpg)
where if
is consistent then
![](https://www.scirp.org/html/5-1680081\03920604-8230-48bb-a6ce-4eaaeccec2bd.jpg)
and if
is inconsistent then
![](https://www.scirp.org/html/5-1680081\0f914670-02e3-4571-a408-93776cdded8d.jpg)
The deductions for the inconsistent
are the same as in
minus ![](https://www.scirp.org/html/5-1680081\481521b1-d556-4cf6-b4cd-fee1025a1f3f.jpg)
Definition 4.1.
is provable if there is a sequence
![](https://www.scirp.org/html/5-1680081\d31fcdd7-38d5-413b-aaf6-4e6b74b9ce35.jpg)
of statements such that 1) ![](https://www.scirp.org/html/5-1680081\bf2efa55-7405-4046-b023-93ba7694d939.jpg)
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
![](https://www.scirp.org/html/5-1680081\26338415-6374-4d44-9cc5-c3088dcbd844.jpg)
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
![](https://www.scirp.org/html/5-1680081\004dda32-f9cf-4d6d-b249-249bae0ebdc2.jpg)
and
![](https://www.scirp.org/html/5-1680081\334be5f0-079e-4c21-98dc-2a56bbef3d33.jpg)
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
![](https://www.scirp.org/html/5-1680081\db551922-5a82-4e10-a0f7-9752e2dbaabb.jpg)
![](https://www.scirp.org/html/5-1680081\eb99623a-bfd8-48df-89fa-991af1d8e285.jpg)
where either
or ![](https://www.scirp.org/html/5-1680081\319739af-7fc4-4663-868d-35e8c5603eaa.jpg)
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption,
and
are consistent, and so is ![](https://www.scirp.org/html/5-1680081\c93bc1d3-6e47-4bc3-9e98-c308dbe9a9e8.jpg)
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption,
is consistent, and so is ![](https://www.scirp.org/html/5-1680081\642a8b1b-4a43-4cb7-88cc-7eb902438e2b.jpg)
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption,
is consistent, and so is ![](https://www.scirp.org/html/5-1680081\cc46b7de-75ac-48b2-8d6d-aa38a6d223ba.jpg)
By the proof of the theorem, we have
![](https://www.scirp.org/html/5-1680081\c1136503-60cf-4392-98f4-5f1824bb7e78.jpg)
Theorem 4.3. For any formula sets
and formula
if
is consistent then ![](https://www.scirp.org/html/5-1680081\63df32a1-2dd3-47d5-a063-89941970a0bf.jpg)
Proof. We prove the theorem by the induction on the structure of
Assume that ![](https://www.scirp.org/html/5-1680081\550d7993-cff4-4fc0-8f02-6ea6d41abdc0.jpg)
If
then
and
Hence,
![](https://www.scirp.org/html/5-1680081\07cc436b-6e21-462e-8529-27f700457c31.jpg)
If
then
and
By the induction assumption,
![](https://www.scirp.org/html/5-1680081\232b589d-3332-44cd-85ea-44b356fbfa51.jpg)
![](https://www.scirp.org/html/5-1680081\f0126746-e5e4-4a53-934c-d31c33afc36d.jpg)
Hence, we have
![](https://www.scirp.org/html/5-1680081\7e573c3c-a659-44f4-b4d4-dd53ce45c23b.jpg)
If
then either
is consistent or
is consistent.
If
and
are consistent then
and
By the induction assumption,
![](https://www.scirp.org/html/5-1680081\18471ff3-dd35-4b8a-939d-8d50aa239be3.jpg)
![](https://www.scirp.org/html/5-1680081\ce10feaa-453a-4a61-802f-0755e628089e.jpg)
Hence, we have
![](https://www.scirp.org/html/5-1680081\35296267-acaa-41b2-8b82-087344ffc267.jpg)
If
is inconsistent and
is consistent then
By the induction assumption,
Hence, by Lemma 2.5, we have
![](https://www.scirp.org/html/5-1680081\5c7bbf08-eae5-4a93-b974-b785376a0252.jpg)
![](https://www.scirp.org/html/5-1680081\2528acd3-e378-47a4-9b35-f37dd93a9bb6.jpg)
![](https://www.scirp.org/html/5-1680081\04784b07-acbe-4406-b078-20ab8c05d6b2.jpg)
![](https://www.scirp.org/html/5-1680081\7fa2af3a-4691-4db6-bb14-036a7d868b4c.jpg)
If
is consistent and
is inconsistent then
By the induction assumption,
Hence, by Lemma 2.5, we have
![](https://www.scirp.org/html/5-1680081\6ff07c65-7d0c-4e60-aecd-5d1f326dab26.jpg)
![](https://www.scirp.org/html/5-1680081\29d0957b-5457-4b7b-8b98-65f41b77316b.jpg)
![](https://www.scirp.org/html/5-1680081\6df61fed-d15a-45a7-bf98-317f56feb82c.jpg)
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 ![](https://www.scirp.org/html/5-1680081\0a99bdfa-d5ca-4c78-991b-f4c692aac2b3.jpg)
If
then
and by
is provable, where ![](https://www.scirp.org/html/5-1680081\4d559694-75b0-4910-8b68-bfffd0767322.jpg)
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
![](https://www.scirp.org/html/5-1680081\c7fbb943-13d5-48c6-97a1-f8894b01f8c9.jpg)
is provable, where ![](https://www.scirp.org/html/5-1680081\66a6b6b6-4fe2-4ad0-b3ef-eb24661a8b08.jpg)
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
![](https://www.scirp.org/html/5-1680081\c58bec78-a867-49d8-915a-94948085d50f.jpg)
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 ![](https://www.scirp.org/html/5-1680081\de02f7eb-40a2-40ae-8d84-ac5526897720.jpg)
If
is inconsistent then
a contradiction.
If
is consistent then by Lemma 3.5,
![](https://www.scirp.org/html/5-1680081\93a99e29-7d6b-4a43-b0fb-dd149f730e33.jpg)
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