=Paper= {{Paper |id=Vol-2546/paper01 |storemode=property |title=Dynamic doxastic action in Doxastic Modal Logic |pdfUrl=https://ceur-ws.org/Vol-2546/paper01.pdf |volume=Vol-2546 |authors=Nadiia Kozachenko }} ==Dynamic doxastic action in Doxastic Modal Logic== https://ceur-ws.org/Vol-2546/paper01.pdf
                  Dynamic doxastic action in
                    Doxastic Modal Logic

                     Nadiia Kozachenko[0000−0003−2358−9076]

                     Kryvyi Rih State Pedagogical University,
                   54, Gagarin Ave., Kryvyi Rih, Ukraine, 50086
                            n.p.kozachenk@gmail.com



      Abstract. This article is a trying to combine two main traditions of
      belief revision: the so-called AGM-approach and Dynamic Doxatic Logic
      approach. We consider doxastic actions as modal operators partly like
      DDL-style and compare their features with AGM postulates. We con-
      struct axiomatical systems for the operator of the expansion and the
      operator of the contraction. Within the system based on this interpreta-
      tion, we can express and prove the corresponding postulates of expansion
      and contraction AGM. It demonstrates that these modal operators corre-
      spond to the functions of expansion and contraction described in AGM,
      about that the representational theorem has been formulated.

      Keywords: Belief revision, AGM, DDL, Modal logic, Dynamic modal
      logic, Doxastic action, Epistemic logic, Doxastic logic, Belief change.


1   Dynamic interpretation of doxastic actions
Belief revision is promising trend in modern epistemic logic deals with changes
of our knowledges and beliefs. It is aimed at formal representation of the pro-
cess of belief change. There are two main traditions of belief revision: the so-
called AGM-approach, named after its initiators Carlos E. Alchourròn, Peter
Gärdenfors and David Makinson (see their most seminal paper [1] and inspired
reserches, e.g.: [4]), and DDL-approach — Dynamic Doxatic Logic based on in-
genious ideas of Krister Segerberg (see, e.g.: [12]). Both approaches are very
similar in a general intention and research methodology, furthermore their main
purpose is an adequate representation of doxastic actions perfomed in the pro-
cess of belief change. In both traditions the basic doxastic actions represented
by expansion, contraction and revision, but each approach implements them in
different ways. This ways depend on the format of main epistemic objects such
as epistemic states, admissible epistemic inputs, expected epistemic results etc.
Implemetation of doxastic actions also depends on specific notion of changes in
belief states — it could be taken as a process (see, e.g.: [2]) or as a result of
change (see, e.g.: [3]).

Copyright c 2019 for this paper by its authors. Use permitted under Creative Common
License Attribution 4.0 International (CC BY 4.0).
22

    AGM. The main postulates of belief change were described in AGM, so
this treatment sometimes is called “postulational approach”. Basic properties
of expansion, contraction and revision are presented in AGM as a set of for-
mal axioms. It is commonly accepted that any interpretation of doxastic action
should satisfy the suitable set of the axioms. However, main drawback of this
approach is a static representation of doxastic actions. All doxastic actions in
AGM factually are reduced to operations over theories.

AGM expansion: T + A (T — initial knowledge set (theory), + — the sign
  of expansion and A — new knowledge (or belief) added to the initial set).
AGM contraction: T ÷ A (T — initial knowledge set (theory), ÷ — the sign
  of contraction and A — knowledge (or belief) extracted from the initial set).

    AGM considers the status of the theory before and after change, but it doesn‘t
consider the process of change. Thus an underwater part of iceberg of properties
of doxastic operations are remained unexplored.
    DDL. The idea of constructing an axiomatic system capable to display the
dynamic properties of doxastic actions is partially implemented by the dynamic
direction in belief revision. The basis of this approach is the idea of representing
the dynamic aspect of belief change by specific language of DDL. Doxasic actions
are considered as term-formed operators +, ÷, *.

DDL expansion: +φ (means it is performing an expansion by φ).
DDL contraction: ÷φ (means it is performing a contraction by φ).

    These terms constitute entire formula with additional operators “[ ]”, “<>”.
Thus, notion ψ[+φ] means “ψ regularly holds after the agent performs an ex-
pansion by φ” and ψ < +φ > means “perhaps ψ holds after the agent performs
an expansion by φ”
    This language has much more resources for a detailed analysis of doxastic
actions, but it is too complicated and cumbersome. Whereas the postulational
way allows to define doxastic action and describes the basic principles of belief
change, it has too simple syntax that makes difficult further detailed researching.
Therefore it is reasonable to construct an axiomatic logical system capable to
combine advantages of both approaches and overcome their shortcomings. The
syntax of this logic should be simple like the syntax of the AGM-system and
should be flexible enough to express the process of change.
    To solve this task it need to change the aspect of consideration of doxastic ac-
tions. In this connection Yaroslav Shramko makes an interesting offer, proposed
a more depth consideration of the epistemological grounds of beliefs. He offers
to interpret doxastic actions as pure modal operators to relegating the action
directly into the center of researching [13]. The proposed idea differs from the
modal interpretation of doxastic actions by K. Segerbeg (DDL-approach). If dox-
astic action (expansion, contraction and etc) is considered as regular modal op-
erator, its application to a Boolean formula creates a dynamic formula. Whereas
doxastic operator in DDL forms only term (see: [12], [7]) and thus it is not a
purely modal operator. The representation of doxastic actions as formula-formed
                                                                                   23

modal operators considerably simplify syntax and with that allows to analyze
the dynamic aspect of the belief revision. It is possible to build specific dynamic
modal logic on this notion.
    The basic idea of this paper is to represent expansion and contraction actions
as modal operators and to show the equivalence of received operators to appro-
priate operators AGM. We need to consider the AGM postulates for expansion
and contraction and to prove that they hold doxastic actions interpreted in the
modal way.
    Within the AGM belief state of the subject is reduced to a set of beliefs closed
under the logical consequence. After the AGM under a consequence operation
we mean an operator Cn that takes sets of proposition to sets of proposition,
such that three condition are satisfied, for any sets X and Y of proposition:
X ⊆ Cn(X), Cn(X) = Cn(Cn(X)), and Cn(X) ⊆ Cn(Y ) whenever X ⊆ Y [1,
p. 511]. Thus we will use the equivalent notation y ∈ Cn(X) and X ` y.
    Each set of beliefs can represent the belief state, as well as any belief state
may be presented as a set of beliefs. Each proposition represents a belief and,
accordingly, each belief can be represented in the form of a proposition. That is,
the belief state is a set of propositions – beliefs, in which the subject is convinced
of the truth. We will examine the change of a theory – consistent sets of beliefs,
closed under the logical consequence (Cn).


2    AGM postulates of expansion
Expansion – the simplest doxastic operator in AGM. Its point lies in adding
new information to the initial set of beliefs. Expansions is implemented by using
+, displaying a pair (set of beliefs, statements) on the set of sets of beliefs
(K × L → K). Where K is the initial belief set, the expansion of K by A
is denoted by K + A. Expansion can be characterized by the following set of
postulates [6, p. 48-51].
    Closure          K + A – belief set                   E1
    Success          A ∈ (K + A)                          E2
    Inclusion        K ⊃ (K + A)                          E3
    Vacuity          If A ∈ K then (K + A) = K            E4
    Monotonicity If K ⊃ H then (K + A) ⊃ (H + A) E 5
    These postulates describe a family of expansion operators. Factually, with
the help of the postulates of expansion E1-E5 can be axiomatically defined the
operator of expansion. That is, if the doxastic operator satisfying the postulates
of expansion E1-E5, then it is equivalent to the operator expansion of AGM.


3    AGM postulates of contraction
Contraction is applied in those cases where a proposition must be removed from
the belief set without giving any new information. Contraction is implemented
by using ÷, displaying a pair (set of beliefs, statements) on the set of sets of
beliefs (K × L → K). Where K is the initial belief set, the contraction of K by
24

A is denoted by K ÷ A. Contraction can be characterized by the following set
of postulates [6, p. 60-64].
     Basic postulates of contraction, which factually mean the axiomatic definition
contraction, were developed under the traditional approach of AGM [1]. Building
a contraction operator is considered to be successfull if it exists a proving that
it satisfied the postulates of contraction AGM.
     Closure           K ÷ A – belief set               C1
     Success           If 0 A then K ÷ A 0 A            C2
     Inclusion         K ÷A⊃K                           C3
     Vacuity           If A ∈/ K then K ÷ A = K         C4
     Extensionality If A ⇔ B then K ÷ A = K ÷ B C 5
     Recovery          K ⊆ (K ÷ A) + A                  C6
     The postulate of recovery is not always achieved because it involves the com-
position of operators of contraction and expansion, but it leads to inconsistency
in the AGM. If the contraction operator satisfies five postulates without recovery,
it is named a withdrawal operator. This designation describes irreversible process
and defines contraction as a singular operator, independent on the expansion.


4    Principles of Doxastic Modal Logic (DML)

DML language allows to place doxastic actions in the center of consideration.
Doxastic formula DML formed by hanging doxastic operator on the Boolean
formula. In fact, each doxastic formula DML is the representation of some action
of belief revision at the time of conversion (see [10, p. 18]).
    Let A be an usual formula of propositional calculus, + – doxastic operator
expansion, ÷ – respectively doxastic operator contraction. Consider a fixed the-
ory. Then +A will mean expansion by A. Similarly ÷A will mean contraction
by A. In DML interpretation doxastic operators can be applied to nondoxastic
(Boolean) propositiond. The result of applying these operators will be the dox-
astic formula. Thus, expansion and contraction are interpreted in DML as modal
(single) operators in pure form. And therefore, +A, ÷A and similar doxastic for-
mulas do not express a certain state theory but the transformation theory. As
a result of doxastic actions a static formula can be obtained, which expresses
a certain state theory, or we will need to implement the next steps of doxastic
actions.
    Doxastic actions of expansion and contraction over a fixed belief set will look
this way.
    Expansion by A: +A
    Contraction by A: ÷A
    The general characteristics of dynamic modal logic DML will be common to
all axiomatic systems built according to this approach. Basic properties of the
axiomatic systems will be presented according to the work of Y. Shramko [13].
    As in the language of classical logic the illogical character of a set is an infi-
nite list of propositional variables p, q, r, s. The logical symbols are signs of the
                                                                                          25

truth-functional propositional connectives: &, ∨, ⊃, ¬ and the symbols of doxas-
tic operators + and ÷. The technical characters are left and right parentheses
(, ).

DEFINITION 1 Boolean formula
  A formula is called boolean if and only if it consists of elementary proposi-
  tions and propositional connectives.

    In building of this logic, we assume that doxastic operators are not appli-
cable to doxastic formulas. Iteration of doxastic operators is possible, but with
additional conditions and needs a deeper study. Thus, we have the following
definition of an elementary doxastic formula.

DEFINITION 2 Elementary doxastic formula
  +A and ÷A are elementary doxastic formula iff A is a boolean formula.

DEFINITION 3 Well-formed formula
  Well-formed formula (WFF) is called:
  (1) any Boolean formula
  (2) any elementary doxastic formula
  (3) if A and B are WFF, then A&B, A ∨ B, A → B,¬A are WFF,
  nothing else is WFF.

   All doxastic modal logic which have DML syntax will be formulated as a
system of axioms with the rules of substitution and inference. First of all, note
that all axioms of propositional calculus are axioms of each logic DML. We have
the following rule:
   PC                All axioms of propositional logic are an axiom of DML.
   Typically inference rule is Modus Ponens. If the formula A is inferred and
formula A → B is inferred, then formula B is inferred.
   MP                If ` A and ` A → B then ` B.
   To formulate the rules of substitution we will need the notion of correct
substitution.

DEFINITION 4 Correct substitution Substituting of formula B instead of
  occurrence of some variable p in well-formed formula A is called correct if
  and only if the result of substitution is a WFF.

     Now we can formulate a rule of admissible substitutions.
     US                      Let A be a theorem DML, and p1 , p2 , . . . , pn are some propo-
sitional variables that are included in A. Then formula A, obtained by simulta-
neous substitution of some WFF B1 , B2 , . . . , Bn instead of every occurrence of
p1 , p2 , . . . , pn , is a theorem.
     Factually, the dynamic modal logic DML is a propositional calculus with the
alphabet extended by typing doxastic modal operators:+, ÷. These modal oper-
ators are a formal interpretation of cognitive actions: expansion and contraction,
respectively.
26

5    Minimal logic of expansion
Consider the axiomatic construction of doxastic modal logic of expansion based
on the interpretation of a cognitive action of expansion as a modal operator [10].
For this reason we need a DML language and series of axioms that define the
specific nature of the operator of expansion. Consider the basic properties of the
expansion used in the construction of epistemical theories. AGM define it by
using the apparatus of set theory [8, p. 4]:

    K + A = Cn(K ∪ A), where K is the initial belief set and Cn is the operation
of closure under the logical consequence.

    Thus, if we want to expand the theory by A, we must mechanically add A
to the original belief set using the set-theoretic union operation and close the
obtained set under the logical consequence.
    By completeness of the belief set, each deducible formula of propositional
calculus will be added to the resulting theory. Obviously the next property, if
A is a theorem of propositional calculus, we must add it to our theory, which is
similar to the well-known in modal logic rule of hanging of necessity. In the DML
language this rule will take the following form: if A is a theorem of propositional
calculus, then +A is a theorem of minimal logic of extension.

     N             If ` A, then ` +A.

    In this situation doxastic operator of expansion behaves like a normal modal
operator. Remarkable, such behavior should not follow the properties of the
operator, but from the definition of cognitive operator, which is represented by
this modal operator. It indicates that the chosen method of presentation can
actually be used.
    The following important property is that the operator extension is closed
under Modus Ponens. This characteristic, as the previous one, also follows the
definition of expansion adopted in the AGM. By analogy with the principle of
bringing of modality for normal modal systems, this principle can be expressed
as distributivity operator of expansion with respect to the implication.

     K             +(A → B) → (+A → +B)

    Based on the previous note, the operator of expansion can be interpreted as
a normal modal operator, which owns the properties of positive modality. Rules
as PC, MP, US, N and K are the base of the most weak logic of extension of
beliefs.

6    Dynamic modal logic of extension DM LE
The expressive power of DML language is sufficient to build a stronger logic of
expansion, which will examine in details the properties of AGM expansion. In
building this logic we need a criteria of rationality AGM, taken in the concept:
                                                                                 27

 – Requirement of minimal changes in initial beliefs,
 – Priority of new information,
 – Consistency.
    To the list of criteria of rationality also can be added the principle of cate-
gorical matching, which is usually introduced implicitly, but is one of the most
important when performing any operation. According to the principle of cate-
gorical matching (see [8, p. 5]) the result of the operation must be represented in
the same form as the original data. Thus, the execution of any doxastic operation
on the belief set should guarantee the result as the belief set and nothing else.
    The criterion of priority of the new information requires the presence of
expression in the belief set after expansion of the theory by this statement.
In the AGM postulates for expansion is mentioned a criterion expressed as a
postulate of success. Taking a statement to the belief set, the agent elevates it
to the rank of belief and commits to adopt it.

      T             +A → A

    If we consider konsequent of T as an expression of truth, that “if A is added to
the theory, then A is true“, we get a very strong statement. Given the properties
of the agent of belief (at least, he may be wrong), we can say that this statement
is quite often incorrect. However, if we represent the right side of the formula
as an approval A (according to Frege), not requiring a mandatory truth — no
factual or logical [13]. Then the formula can be considered as an expression of
the sequence of doxastic action which forces an agent to accept all of his beliefs.
Factually, if the agent adds a statement to his belief set, then he is obliged
to assert it. This expression describes agent’s doxastic commitments, that he
imposes on himself by adding a statement to the belief set.
    Logic defines a set of rules PC, MP, US, N, K and T is dynamic modal logic
of expansion DM LE .

7     AGM postulates of expansion within DM LE
Expressive capabilities of DM LE allow to formalize the postulates of expansion
AGM: closure, success, inclusion, vacuity, monotonicity and minimality. Accord-
ing to the theorem AGM [1, p. 513], the operator which satisfies the given pos-
tulates is equivalent to the operator of expansion AGM.

7.1       Closure
The resulting belief set obtained from the expansion of the initial theory by some
proposition A, should be closed under the logical consequence. Formally, if K is
a belief set, then K + A is a belief set. This postulate expresses the principle
of categorical matching whereby the representation of a belief after performing
some operations must be the same as the way of presenting the initial state. In
DM LE the postulate of closure is expressed in rule K.

      K         +(A → B) → (+A → +B)
28

7.2       Success

After the expansion of the theory by some proposition A, it must belong to
the theory. This postulate expresses the criterion of priority a new information,
whereby the input information must be accepted. Formally: A ∈ K + A. In
DM LE the success postulate is expressed by axiom T.

      T         +A → A


7.3       Inclusion

The initial belief set must be always a subset of the expanded belief set. This
is a kind of assertion of ,,purity” of the operator of expansion. According to
the postulate of inclusion, making the expansion, we combine the initial belief
set and the set, which consists of the added proposition, while no proposition
is removed from the initial set. Closure of resulting belief set must include the
original belief set. Formally: K ⊂ K + A. In DM LE postulate of inclusion can
be expressed the following:
      B& + A → B
    The postulate of inclusion can be obtained from the theorem of the proposi-
tional calculus by the substitution rules, so it is deducable in DM LE .


7.4       Vacuity

Expansion of the theory by proposition A which is already presented in it, does
not change the theory. Formally: if A ∈ K, then K + A = K. In DM LE the
postulate of vacuity can be expressed as follows:
      A → (+A → A)
    The above mentioned postulate AGM expansion may be withdrawn within
DM LE using an axiom of propositional calculus and the rules of substitution,
so it is a theorem of logic of expansion.


7.5       Monotonicity

Operation of expansion is monotonous under the set-theoretic operation of in-
clusion. If K ⊆ N , then K + A ⊆ N + A. The same property retains the operator
of expansion with respect to implication in DM LE .
      (B → C) → ((B& + A) → (C& + A))
    The postulate of monotonicity of expansion is also inferred in DM LE by the
rules of substitution.
                                                                                 29

7.6     Minimality
For any belief set K and proposition A, K + A is the lowest set of beliefs which
satisfies the postulates of closure, success and inclusion. This postulate expresses
the criterion of minimality, whereby the modified belief set must be strictly
regulated. Expanding the theory by some proposition A we should add only this
proposition A and nothing more to the belief set. Closure of the received belief set
provides a presence added proposition in the belief set. Thus, if a proposition
B does not follow from A, the expanding of the theory by A should not lead
expansion of a theory by B.

Theorem. Minimality DMLE . ¬(A → B) → ¬(+A → +B)

      Proof.
      1 ¬(A → B) → ¬ + (A → B)   US, T, contraposition
      2 ¬ + (A → B) → ¬(+A → +B) 1,K
      3 ¬(A → B) → ¬(+A → +B)    1, 2, transitivity
    If the implication (A → B) exists in the initial belief set, then when adding
A, proposition B appears in the theory as a result of keeping closure. If B does
not follow from A, but was still present in the initial theory, its adding does not
change the theory, according to the postulate of vacuity.
    Thus, the formalization of operation of expansion allows to express the def-
inition of expansion, which moves in the AGM, the basic properties of this op-
eration and criteria of rationality applicable to the expansion. The postulates
AGM, which define the basic properties of operation of expansion, can be for-
malized and proved in dynamic doxastic logic of expansion. Thus, the logic given
by the PC, US, N, K and T is a dynamic modal logic of extension DM LE and
represents the function of expansion AGM.


8      Dynamic modal logic of contraction DM LC
Let us consider the operator of contraction. Any logical system based only on the
operator of contraction, without expansion, allows us to express the properties
of the withdrawal function [11], a specific type of contraction, which does not
satisfy the postulate of recovery. Notably, while all the other AGM postulates
of contraction are satisfied. It seems inappropriate to build a logical system
based on an operator, which does not satisfy all AGM postulates of contraction,
however, to express the complex operator, can be based even on withdrawal
operator.
    To build a logical system based on the operator of contraction, use the al-
phabet of dynamic modal logic DML with the rules of PC, MP, US. In addition,
we introduce some specific rules in a logical system, that determine the proper-
ties of contraction, defined by the axiomatic definition of the AGM contraction
functions.
    First of all, consider the introduction of the operator of contraction. The
next rule says that when we contract the theory by proposition B, we should
30

remove all propositions A, which inferred B. Factually, if A → B is a theorem,
then ÷B → ÷A is a theorem.

     C        If ` A → B and A → B is a boolean formula, then ` ÷B → ÷A.

    Note, the same principle, expressed by a formula (A → B) → (÷B → ÷A)
can not be accepted as an axiom of DM LC , because if (A → B) is not a tautol-
ogy, an alternative for removal A (due to contraction by B) could be generally
removal formula (A → B).
    The operation of contraction should provide consistency of belief set. If the
belief set contains some proposition A, it should not contain a denial of this
proposition ¬A. Contraposition of these statements is more convenient: if a belief
set contains ¬A, then in order to preserve consistency of the set, we need to delete
A.
    This doxastic commitment can be justified in another way, if we believe in
a false proposition A (this is possible if A is contrary to our initial belief set
and initial set contains ¬A), we must reject the false proposition. Indeed, we are
trying to get rid of false propositions in the change of belief, no matter for what
reason — as a result of obtaining some new information, or, for example, due to
review the existing belief set in search of contradictions.
    This principle of consistency of a belief set reflects the mechanism of contrac-
tion, and therefore should be accepted as an axiom DM LC and can be stated
as follows:

     U        ¬A → ÷A

   The following axiom expresses an important principle of partial meet con-
traction AGM, also called ”conjunctive factorization”.

     DM1              ÷(A&B) → (÷A ∨ ÷B)

   It is natural to adopt this axiom. If we wish to contract the belief set by a
conjunction and there exists some preference between the conjuncts, then this
contraction is equivalent to contraction by the non-preferred conjuncts. If the
both conjuncts are equal, then we will have to remove both [5, p. 12]. There are
three ways to contract initial belief set by conjunction A&B, such us: remove
the sentence A but leave the sentence B, remove the sentence B but leave the
sentence A, and remove both.

9    Doxastic modal logic of contraction DM LC and AGM
     postulates
The most convenient kind of contraction is represented in AGM by so-calling
,,partial meet contraction”. The basic postulates of contraction are developed in
AGM (six basic and two additional postulates)[1]. All the postulates of contrac-
tion can be expressed in the language of DM LC , moreover almost all postulates
of contraction can be proved in the doxastic modal logic of contraction.
                                                                                31

9.1    Closure
According to the principle of categorial matching, the representation of a belief
state after a belief change should have the same form as the representation
of the belief state before the change [8, p. 5]. Hence, if the initial theory K is
logically closed, then theory K ÷ A is closed too. Let us contracting the set K by
proposition A. Thus, before contraction we need to make sure that the original
set K is closed under logical consequense, and after a contraction we must to
implement the closure outcome set K ÷ A.
    On the expansion postulate of closure acquires the form

      +(A → B) → (+A → +B)

    On the contraction this postulate points out that if the contraction the set
K by proposition A was done correctly, then closure of the outcome set K ÷ A
must not contain A. The proposal should be deleted explicitly and implicitly.
To do this we need to remove all statements that lead A otherwise the closure
operation again returns it to the theory. In the language of DM LC it will look
as follows.

Theorem 1. DML1                ` (A → B) ⇒ ` (÷B → ÷A)

Proof. If B follows from A, then, if we remove B, then we must remove A. This
is a inference rule C.

9.2    Inclusion
K ÷A⊆K
    A theory obtained by contraction of some theory must be a subset of the
initial theory. It is impossible that the outcome belief set K ÷ A was intersected
with the initial belief set or K was a proper subset of K ÷ A.

Theorem 2. DML2                ÷B → (÷A → ÷B)

Proof. This principle is a special case of the consequent approval, and therefore,
it is the theorem of our system.

A deletion any proposition should not cause an expansion of a system by means
of proposition which are not exist in it. Factually, any proposition which does
not belong to belief set should not appear in the theory as a result of contraction
by anyone proposition.

9.3    Vacuity
A∈/ K ⇒K ÷A=K
   If the proposotion does not belong to the original belief set, then its removal
should not cause any transformation of the system. In doxastic modal logic of
contraction this postulate can be expressed by the following method:
32

Theorem 3. DML3               (B&¬A) → (÷A → B)

    In other words, if belief set is compatible with ¬A, that it does not contain
statement A, then we obtain the same initial set B, when try to remove the A.
      Proof.
      1 (B&¬A) → B                 PC
      2 B → (B ∨ ¬ ÷ A)            1, PC
      3 (B ∨ ¬ ÷ A) → (÷A → B)     2, PC
      4 (B&¬A) → (÷A ∨ B)          1, 3, transitivity

9.4     Success
A∈ / Cn(∅) ⇒ A ∈ / (K ÷ A)
    Reformulating this postulate by contraposition, we obtain the next note: if
A ∈ (K ÷ A), then A ∈ Cn(∅). That is, if a statement is present in the theory
after it was removed, then the statement is a logical tautology. In the language
of DM LC this postulate can be written as

Theorem 4. DML4               (÷A → A) → ((A → A) → A)

      Proof.
      1 ¬A → ÷A                                                            U
      2 (¬A → ÷A) → (÷A ∨ A)                                               1, PC
      3 (¬A ∨ ÷A) → ((¬A ∨ ÷A)&(A ∨ ¬A))                                   2, PC
      4 ((¬A ∨ ÷A)&(A ∨ ¬A)) → (÷A&¬A) ∨ (A&¬A) ∨ A                        3, PC
      5 ((÷A&¬A) ∨ (A&¬A) ∨ A) → ((¬ ÷ A ∨ A) → ((¬A ∨ A) → A))            4, PC
      6 ((¬ ÷ A ∨ A) → ((¬A ∨ A) → A)) → ((A → A) → A)                     5, PC

9.5     Extensionality
If A ↔ B ∈ Cn(∅), then K ÷ A = K ÷ B
    Extensionality guarantees that the logic of contraction is extensionak in the
sense of allowing logically equivalent sentences to be freely substituted for each
other [8, p. 8].

Theorem 5. DML5               ` A ↔ B ⇒ ` ÷A ↔ ÷B

Proof. The proof of this rule can be easily obtained using the rule C.

Thus, we expressed the five postulates of AGM contraction and built their proof
in the system DM LC . Within the logic contraction can not formalize the postu-
late of recovery, because it requires a explicit use of the operator of expansion.
    So, for the modal operator of the contraction imposed by axioms DM LC ,
performed five basic postulates of contraction AGM: closure, inclusion, vacuity,
success, and extensionality. Thus, the modal operator of contraction reflects
the properties of the functions of contraction AGM. Now, we can formulate
appropriately representational theorem, analogous to [1].
                                                                                  33

   Representational Theorem. Sinse the modal operator of the contraction
DM LC satisfies the properties closure, inclusion, vacuity, success, and exten-
sionality, hence the operator of the contraction DM LC is equivalent to with-
drawal function AGM.
    Thus, the representation doxastic actions as modal operators allows to con-
struct axiomatical systems for the operator of the expansion and the operator of
the contraction. Within the system based on this interpretation, we can express
and prove the corresponding postulates of expansion and contraction AGM. It
demonstrates that these modal operators correspond to the functions of expan-
sion and contraction described in AGM, about that the representational theorem
has been formulated. This method of representation of doxastic actions makes it
possible to formulate rigorously known properties of expansion and contraction
and, moreover, to trace the new properties of doxastic actions, which manifest
themselves by virtue of this representation.


References
 1. Alchourron, C.E., Gar̈denfors, P., Makinson, D.: On the logic of theory change:
    Partial meet contraction and revision functions. Journal of Symbolic Logic 50(2),
    510–530 (1985). doi:10.2307/2274239
 2. Baltag, A., Fiutek, V., Smets, S.: Beliefs and evidence in justification models.
    In: Beklemishev L., Demri S., Máté A. (eds.) Advances in Modal Logic, vol. 11,
    pp. 156–176 (2016)
 3. Fermé, E.; Garapa, M., Reis, M.D.L.: On ensconcement and contraction. Journal
    of Logic and Computation 27(7), 2011–2042 (2017). doi:10.1093/logcom/exx008
 4. Fermé, E., Hansson, S.O.: AGM 25 Years: Twenty-Five Years of Research in Belief
    Change. Journal of Philosophical Logic 40(2), 295–331 (2011). doi:10.1007/s10992-
    011-9171-9
 5. Fermé, E., Hansson, S.O.: Belief Change: Introduction and Overview. Springer
    Briefs in Computer Science Series. Springer, Cham (2018). doi:10.1007/978-3-319-
    60535-7
 6. Gardenfors, P.: Knowledge in Flux: Modeling the Dynamics of Epistemic States.
    College Publications, London (2008)
 7. Girard, P., Rott, H.: Belief revision and dynamic logic. In: Baltag A., Smets S.
    (eds.) Johan van Benthem on Logic and Information Dynamics. Outstanding Con-
    tributions to Logic, vol. 5, pp. 203–233. Springer, Cham (2014). doi:10.1007/978-
    3-319-06025-5 8
 8. Hansson, S.O.: A Textbook of Belief Dynamics: Theory Change and Database
    Updating. Springer Netherlands, Dordrecht (1999)
 9. Hansson, S.O.: Ten Philosophical Problems in Belief Revision. Journal of Logic
    and Computation 13(1), 37–49 (2003). doi:10.1093/logcom/13.1.37
10. Kozachenko, N.P.: Doxastic Modal Logic and AGM. In: Markin V.I. (ed.) Smirnov’s
    Readings; 6nd International Conference, Moscow, 17–19 June 2009, pp. 18–19.
    Sovremennye tetradi, Moscow (2009)
11. Makinson, D.: On the status of the postulate of recovery in the logic
    of theory change. Journal of Philosophical Logic 16(4), 383–394 (1987).
    doi:10.1007/BF00431184
34

12. Segerberg, K.: Belief Revision from the Point of View of Doxastic Logic. Logic
    Journal of the IGPL 3(4), 535–553 (1995). doi:10.1093/jigpal/3.4.535
13. Shramko, Y.: Doxastic actions and doxastic commitments: belief revision as pure
    modal logic. In: Smirnov’s Readings; 2nd International Conference, pp. 90–92.
    Moscow (1999)