=Paper=
{{Paper
|id=Vol-3242/paper2
|storemode=property
|title=Public Announcements for Intuitionistic Epistemic Logic IEL
|pdfUrl=https://ceur-ws.org/Vol-3242/paper2.pdf
|volume=Vol-3242
|authors=Alexandra Pavlova
|dblpUrl=https://dblp.org/rec/conf/ki/Pavlova22
}}
==Public Announcements for Intuitionistic Epistemic Logic IEL ==
https://ceur-ws.org/Vol-3242/paper2.pdf
Public Announcement and Intuitionistic Epistemic
Logic
Alexandra M. Pavlova∗
TU Wien; SPbU
Abstract
We introduce intuitionistic public announcement logic: system for public announcement in
intuitionistic logic as well as in a variant of intuitionistic epistemic logic, namely IEL with a
knowledge modal operator K interpreted as “it is verified that the formula holds intuitionisticly",
i.e., that it has a proof which is not necessarily specified in the process of verification. Hilbert-
style axiomatisations and Kripke-style semantics for the systems are provided and soundness
and completeness of the axiomatisation are discussed. The completeness theorem is proved by
the standard method of translation and reduction of the question of completeness of the PA
systems to the systems without PA operators.
Keywords
Intuitionistic Epistemic Logic, Public Announcement, Kripke Semantics, Axiomatisation
1. Introduction
Logic has traditionally been preoccupied with the study of correct reasoning and ar-
guments without any reference to agents and their abilities. Nevertheless, in the late
XXth century the focus of attention has partially moved towards modeling of interaction
between agents. This led to development of different types of multi-agent systems giving
rise to a number of new questions considering the variety of agents. It became obvious that
multi-agent modeling should account for the existence of different types of agent. And
indeed, we observe that in reality different agents possess unequal reasoning capacities,
memory and presumptions. This is true not only of human agents, but also artificial
intelligence. One can identify those characteristics that are pertinent for formal logical
modeling that yield various agent types. Hence, by the variety of agents we understand
the logical diversity that results from various attempts to develop formal systems capable
of modelling actions, reasoning and behaviour of actual ration agents. The question is
mostly studied in two branches of contemporary philosophical logic: in epistemic logic
and numerous action models. The roots of the logical problem of agent diversity lie in
the idea that various agents might have different capacities with respect to knowledge,
beliefs, and desires, as well as use diverse rules of inference. The question has arisen
8th Workshop on Formal and Cognitive Reasoning, September 19, 2022, Trier, Germany
∗
Corresponding author.
$ alexandra@logic.at (A. M. Pavlova)
0000-0002-1877-1167 (A. M. Pavlova)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0
International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
29
quite recently, as it was traditionally believed that logical laws represent some universal
norms using which everyone arrives at the same conclusion given the identical premises.
However, if we want to model real agents, we should be able to embrace the limited
character of their capacities, for instance, in case of imperfect or fallible information.
Although, intuitionistic logic has been very well studied both from technical point of
view and the one on the constructive philosophy, the question of knowledge progress and
belief change was undeservedly put aside. There has been proposed a vast number of
different intuitionistic and constructive modal systems without rising a question of how to
model the knowledge accumulation in the intuitionistic setting. Nevertheless, one should
mention the paper [1] where public announcement was introduced to the epistemic logic.
That being said, we insist that our approach extends that result and applied PAL to
a, epistemic logic IEL that differs significantly from other know intuitionistic epistemic
systems because of how knowledge is understood.
Another reason for choosing this logic is that intuitionistic logic enjoys several nice
properties, e.g., the disjunctive property, finite model property, and it allows for an analytic
calculus. Thus, it is of a particular interest to study its possible extensions. Moreover,
there is a wide range of different logical games for intuitionistic logic (e.g. [2, 3, 4])
that can be extended to the modal level and provide not only technical results but also
philosophical insight on the intuitionistic epistemology in general. Finally, intuitionistic
logic is important for computer science due to the Curry-Howard-Lambek correspondence
(or the Curry-Howard isomorphism) which states a strong connection between types in
programming languages and propositions in intuitionistic logic. Thus, the research might
be relevant for applications to semantics of programming languages.
How would our model change, once we get a proof of a statement? This is the question
we are answering in section 2. In section 2, we propose two systems (that can be combined
into one with two separate operators) that yield the same model change but capture it
differently. The IPALhi (cf. 2.1) system with ♢-type operator suggest a more conservative
change model: after a truthful update h!ϕiψ, we delete all the worlds where ϕ is not
true. The IPAL[] (cf. 2.2) system captures a more interesting relation between public
announcement and non-modal formulae. In section 3 we introduce a knowledge operator
into the two previously discussed systems. we prove soundness and completeness for the
proposed systems.
2. PAL in Intuitionistic logic
In the present chapter we discuss the simplest dynamic extension (i.e. with the public
announcement operator) of the standard intuitionistic propositional logic where the truth
of a formula ϕ is understood as ϕ is provable. Intuitionistic logic is one of the most
studied logics along with the classical logic. It gives rise to families of other logics if
we impose additional restrictions or add new elements, e.g., modalities. Yet, it enjoys a
number of nice properties as mentioned in section 1 The developement of intuitionistic
logic was originally motivated by the philosophy of mathematics and research in the
area of foundations of mathematics. The general idea of intuitionism was proposed by
30
Brouwer [5], however he did not provide any formal system for the logic as his main
concern was that of proofs in mathematics. Now it is common to understand the "truth" in
intuitionistic logic as provability. This is called an informal Brouwer-Heyting-Kolmagorov
semantic (simply BHK):
• a proof of ϕ ∧ ψ consists in a proof of ϕ and a proof of ψ;
• a proof of ϕ ∨ ψ consists in a proof of ϕ or a proof of ψ;
• a proof of ϕ → ψ consists in a construction which given a proof of ϕ returns a
proof of ψ;
• ¬ϕ is an abbreviation for ϕ → ⊥, and ⊥ is a proposition that has no proof.
The formal system for intuitionism was first suggested in the form of Hilbert style (i.e.
axiomatic) calculus independently first by Kolmogorov [6], and then by Heyting [7, 8, 9],
and Glivenko [10] (however, this was a feeble system whose implicative fragment contained
only the identity law and transitivity of implication). Intuitionistic calculus has one
axiom less than the classical one, namely it does not contain the principle tertium non
datur: ϕ ∨ ¬ϕ (alternatively, to obtain the classical calculus, one can add the double
negation elimination (¬¬ϕ → ϕ) to the intuitionistic calculus). In 1935, Gentzen [11]
introduced two new proof systems that were supposed to both better capture reasoning
in mathematics and provide a simpler proof search: Natural Deduction for classical (NK)
and intuitionistic (NI) logics; and Sequent Calculi LK, and LI respectively. Sequent
calculus for intuitionistic logic is analytic which is an important proof-theoretical feature
as it simplifies the proof search. Sequent calculi are based on rewriting rules for sequents,
which are objects of the form Γ ` ∆ where Γ and ∆ are sequences of formulae. In
the most cases (for instance, for classical and intuitionistic calculi), Γ is interpreted as
a big conjunction of the formulae inside, whereas ∆ represents a disjunction. In the
case of intuitionistic logic, the most widespread calculi restricts ∆ to only one formula.
Intuitively, this can be interpreted as follows: at least one formula from ∆ follows from
the conjunction of formulae in Γ. Unfortunately, sequent calculi are not capable of
capturing many interesting logics, so various extensions have been suggested in the last
thirty years, such as hypersequents, nested sequents, labelled calculi etc.
As for the semantics for intuitionistic propositional logic, it has been proved by
Gödel [12] that intuitionistic logic cannot be characterised by a fixed finite number
of truth values. It is well-known that Intuitionistic logic Int can be embedded into
modal logic S4 by means of the Gödel translation. Hence, the standard semantics for
intuitionistic logic is Kripke semantics for modal logic S4 with monotonicity of valuations
(which leads to the monotonicity of forcing). Alternatively, there is a neighbourhood
semantics for intuitionistic logic, but our research mostly concentrates on the Kripke
style one.
Finally, an important result with respect to intuitionistic logic, called Curry-Howard iso-
morphism, relates intuitionistic logic to computability theory and programming languages.
Haskell Curry and William Howard noticed the correspondence between intuitionistic
natural deduction and simply typed lambda calculus. The inference rules and axioms
31
for typing programs resemble the inference rules and axioms for proving formulae in
intuitionistic logic. Propositions-as-types correspondence, and proofs-as-programs corre-
spondence establish an isomorphism between types and formulae, on the one hand, and
between programs and proofs, on the other hand.
We now extend standard intuitionistic propositional logic with a new operator of public
announcement. In what follows we define the language, semantics and axioms for the
system IPAL. In fact, there are several ways of defining public announcement operator
for intuitionistic logic. In what follows we suggest two different operators: h!ϕi and [!ϕ].
In classical PAL, these are dual operators. However, like for quantifiers in intuitionistic
FOL, these operators are not dual any more in IPAL. We first describe IPALhi , i.e.,
the extension with h!ϕi operator, and then IPAL[] with the [!ϕ] operator respectively.
Note that the presented public announcement operators do not only give the truthful
information that the announced formula is true (i.e., there is a proof of it), but also
provides us with the proof. That is so, because, as it is formally defined in the following
sections, the announcement leads to model transformation and those worlds where the
announced formula ϕ is not true are erased, i.e., not only worlds where ¬ϕ is true, but
also such x ∈ W that M, x ⊮ ϕ. As weaker announcement is the subject of further
research.
2.1. System IPALhi
Definition 1. Let P be a countable set of propositional variables. The language LIPALhi :
ϕ ::= p | ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | h!ϕiϕ | ⊥,
where p ∈ P .
Negation is an abbreviation for ϕ → ⊥. Formula h!ϕiψ operator of public announcement
is read as "after some truthful public announcement of ϕ, it holds that ψ", as it is essentially
a ♢-type modal operator. It assumes that ϕ can indeed be truthfully announced (unlike
the □-based operator we introduce in 2.2). Note that in the BNF form h!ϕiϕ we express
the type of the formulae, which is the same for the announcement formula and the one
that is following it. We introduce a Hilbert-style proof system for IPALhi :
Definition 2. Intuitionistic Public Announcement Logic with h!ϕi operator, IPALhi , is
defined by the following axioms:
I Axioms of propositional intuitionistic logic:
1 : ϕ → (ψ → ϕ) 6 : ϕ → (ϕ ∨ ψ)
2 : (ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ)) 7 : ψ → (ϕ ∨ ψ)
3 : (ϕ ∧ ψ) → ϕ 8 : (ϕ → χ) → ((ψ → χ) → ((ϕ ∨ ψ) → χ))
4 : (ϕ ∧ ψ) → ψ 9:⊥→ϕ
5 : ϕ → (ψ → (ϕ ∧ ψ))
32
II Axioms for h!ϕi operator:
10 : h!ϕip ↔ (ϕ ∧ p) 13 : h!ϕi(ψ ∨ χ) ↔ (h!ϕiψ ∨ h!ϕiχ)
11 : h!ϕi¬ψ ↔ (ϕ ∧ ¬h!ϕiψ) 14 : h!ϕih!ψiχ ↔ h!ϕ ∧ h!ϕiψiχ
12 : h!ϕi(ψ ∧ χ) ↔ (h!ϕiψ ∧ h!ϕiχ) 15 : h!ϕi(ψ → χ) → (h!ϕiψ → h!ϕiχ)
• Inference rule: Modis ponens (MP).
Kripke Semantics for IPALhi . Kripke semantics is a triple M = hW, R, υ, where W is
a non-empty set of possible worlds, R is a partial order on W , and υ : W × W → {0, 1} is
the variable valuation function. The function υ is required to be monotonic with respect
to R, i.e., if xRy, then υ(p, x) ≤ υ(p, y) for any p ∈ P and x, y ∈ W . Given the definition
of the forcing relation, it is straitforward that the monotonicity of forcing is preserved as
well: if M, x ⊨ ϕ and xRy, then M, y ⊨ ϕ.
Definition 3. We write M, x « ϕ of formula ϕ is true in the world x of model M. We
define the forcing relation, denoted by «, as follows:
• M, x ⊮ ⊥;
• M, x « p iff υ(p, x) = 1 (truth of variables is prescribed by the valuation function);
• M, x « ϕ ∧ ψ iff M, x « ϕ and M, x « ψ;
• M, x « ϕ ∨ ψ iff M, x « ϕ or M, x « ψ;
• M, x « ϕ → ψ iff for all y ∈ R(x) either M, y ⊮ ϕ or M, y « ψ.
• M, x « h!ϕiψ iff M, x « ϕ and Mϕ , x « ψ, where Mϕ = hW ϕ , Rϕ , υ ϕ i. We define
W ϕ := {w ∈ W | M, w « ϕ}. If W ϕ = ∅, then Mϕ is undefined. If W ϕ = 6 ∅, then
Rϕ := R ∩ (W ϕ × W ϕ ) and υ ϕ (p) := W ϕ ∩ υ(p).
Additionally, by R(x) := {y | xRy}.
Theorem 1 (Soundness). If `IPALhi ϕ, then « ϕ for all ϕ ∈ LIPALhi .
Proof. To prove soundness, one needs to prove two following statements: (1) if ϕ is an
axiom in IPALhi , then « ϕ; (2) that the forcing relation is closed under application of
modus ponens. The proof of (2) is standard for propositional intuitionistic logic.
For (1), one needs to check all the axioms. The soundness of axioms 1–9 is due to the
soundness of standard propositional intuitionistic logic. Thus, one needs to check only
axioms 10–15. This proof is similar to 4 and is based on the forcing relation definition,
thus it is left to the reader to check.
The proof of completeness is done the standard way for PAL, i.e., via translation and
reduction [13]. All formulae with public announcement operators are translated into
formulae without them. This reduces the question of completeness of the PA systems to
the systems without PA operators. We first define a complexity function:
33
Definition 4 (Complexity function). Complexity function c assigns numbers to formulae:
• c(p) := 1
• c(¬ϕ) := 1 + c(ϕ)
• c(ϕ ? ψ) := 1 + max(c(ϕ), c(ψ)) where ? ∈ {∧, ∨, →}
• c(Kϕ) := 1 + c(ϕ)
• c(h!ϕiψ) := (4 + c(ϕ)) · ψ
• c([!ϕ]ψ) := (4 + c(ϕ)) · ψ 1
Our translation uses the equivalences that we used as axioms.
Lemma 1 ((Decreasing-Complexity Lemma). For all p ∈ P and all ϕ, ψ, χ ∈ L
• c(ψ) ≤ c(ϕ) if ψ ∈ Sub(ϕ) where Sub is the set of subformulae;
• c(h!ϕip) > c(ϕ ∧ p);
• c(h!ϕi¬ψ) > c(ϕ ∧ ¬h!ϕiψ);
• c(h!ϕi(ψ ∧ χ)) > c(h!ϕiψ ∧ h!ϕiχ);
• c(h!ϕi(ψ ∨ χ)) > c((h!ϕiψ ∨ h!ϕiχ))
• c(h!ϕih!ψiχ) > c(h!ϕ ∧ h!ϕiψiχ);
• c(h!ϕi(ψ → χ)) > c(h!ϕiψ → h!ϕiχ)
Proof. Given the definition of the complexity function, the proof is trivial and left to the
reader to the sake of space.
We finally define the translation function:
Definition 5. The function t by recursion on complexity c(ϕ):
• t(p) := p
• t(¬ϕ) := ¬t(ϕ)
• t(ϕ ? ψ) := t(ϕ) ? t(ψ) where ? ∈ {∧, ∨, →}
• t(Kϕ) := Kt(ϕ)
• t(h!ϕip) := t(ϕ ∧ p)
• t(h!ϕi¬ψ) := t(ϕ ∧ ¬h!ϕiψ)
1
We give the general definition that works for all of our systems.
34
• t(h!ϕi(ψ ∧ χ)) := t(h!ϕiψ ∧ h!ϕiχ)
• t(h!ϕi(ψ ∨ χ)) := t(h!ϕiψ ∨ h!ϕiχ)
• t(h!ϕih!ψiχ) := t(h!ϕ ∧ h!ϕiψiχ)
• t(h!ϕi(ψ → χ)) := t(h!ϕiψ → h!ϕiχ)
Lemma 2. t(ϕ) ∈ LIP C for each ϕ ∈ LIPALhi , i.e., t(ϕ) has no announcements.
Proof. By induction on c(ϕ).
Lemma 3. `IPALhi ϕ ↔ t(ϕ) for all ϕ ∈ LIPALhi .
Proof. By induction on c(ϕ).
Theorem 2 (Completeness). If S4 « ϕ, then `IPALhi ϕ for all ϕ ∈ LIPALhi .
Proof. 1. S4 « ϕ assumption;
2. `IPALhi ϕ ↔ t(ϕ) by lemma 3;
3. S4 « ϕ ↔ t(ϕ) from 2. by soundness of IPALhi ;
4. S4 « t(ϕ) MP from 1. and 3.;
5. `S4 (ϕ) by completeness of S4;
6. `IPALhi (ϕ) from 5. because S4 ⊆ IPALhi ;
7. `IPALhi ϕ from 2. and 6.
2.2. System IPAL[]
The idea behind [!ϕ] operator is that even if in the possible world in question we do not
have a prove of ϕ, we can still reason about what other statements (formulae) will be
proved once the proof of ϕ is given to us.
Definition 6. The language for Intuitionistic propositional logic LIPAL[] = LIPC ∪ [!ϕ]ϕ.
Formula [!ϕ]ψ operator of public announcement is read as "after every public announce-
ment of ϕ, it holds that ψ". We introduce a Hilbert-style proof system for IPAL[] :
Definition 7. Intuitionistic Public Announcement Logic with [!ϕ] operator, IPAL[] , is
defined by the following axioms:
I Axioms of propositional intuitionistic logic;
II Axioms for [!ϕ] operator:
10. [!ϕ]p ↔ (¬ϕ ∨ (ϕ → p));
35
11. [!ϕ]¬ψ ↔ (ϕ → ¬[!ϕ]ψ);
12. [!ϕ](ψ ∧ χ) ↔ ([!ϕ]ψ ∧ [!ϕ]χ);
13. [!ϕ](ψ ∨ χ) → (ϕ → ([!ϕ]ψ ∨ [!ϕ]χ));
14. [!ϕ][!ψ]χ ↔ [!ϕ ∧ [!ϕ]ψ]χ;
15. [!ϕ](ψ → χ) → ([!ϕ]ψ → [!ϕ]χ).
• Inference rule: Modis ponens (MP).
Kripke Semantics for IPAL[] . Kripke semantics for IPAL[] is defined the same way as
the one for IPALhi ‘(in 2.1), except for the condition on public announcement operator.
Definition 8. Instead of h!ϕiψ we have the following condition for [!ϕ]:
• M, x « [!ϕ]ψ iff M, x « ¬ϕ, or else for all y ∈ R(x), such that y ∈ Mϕ ,
Mϕ , y « ψ, where Mϕ = hW ϕ , Rϕ , υ ϕ i.
Theorem 3 (Soundness and Completeness). If `IPAL[] ϕ iff « ϕ for all ϕ ∈ LIPAL[] .
Proof. The proofs are analogous to the one for IPALhi , theorem 2.
3. PAl for Intuitionistic Epistemic Logic
In this section we are considering previously described public announcements in the setting
of intuitionistic epistemic logic IEL. The system was proposed by Tudor Protopopescu
and Sergei Artemov [14, 15]. Here we consider only their system IEL which models
knowledge as opposed to the system IEL− corresponding to belief.
IEL extends intuitionistic logic by a new modal operator K interpreted as knowledge.
It is based on the intuition behind the BHK semantics, where truth of a formula ϕ is
interpreted as having a proof ϕ. Knowledge Kϕ is then interpreted as "it is verified that
ϕ holds intuitionisticly", i.e., that ϕ has a proof which is not necessarily specified in the
process of verification (cf. [14]). The idea that knowledge corresponds to the existence
of a verification for some formula in question yields specific conditions on K operator
different from the standard classical account. Thus, following Artemov and Protopopescu
[14, 15], one can extend the semi-formal BHK semantics to capture this understanding
of knowledge as follows:
• a proof of Kϕ is a conclusive evidence of verification that ϕ has a proof.
As a real-world example of the K operator, one can name a plenty of things: zero-
knowledge protocol, when a prover gives us an answer that a statement in question is true
without providing the proof; testimony of an authority which applied even in science (we
may know that a theorem is true without being able to reproduce its proof); existential
generalisation and many others. In what follows, we deliberately add K operator to the
systems described above in section 2
36
3.1. System IEPAL
Definition 9. The language LIEPAL = (LIPDhi ∩ LIPBhi ) ∪ Kϕ.
Definition 10. Now we introduce the axiomatisation for IEPAL:
I axioms of IPALhi and IPAL[] ;
II Axioms of IEL:
16. K(ϕ → ψ) → (Kϕ → Kψ);
17. ϕ → Kϕ;
18. Kϕ → ¬¬ϕ;
III An axiom relating K and h!·i:
20. h!ϕiKψ ↔ (ϕ ∧ Kh!ϕiψ)2 ;
21. [!ϕ]Kψ ↔ (¬ϕ ∨ K[!ϕ]ψ);
IV Modus ponens rule.
The K-neccessitation rule is derivable, the deduction theorem and uniform substitution
hold for IEL, as well as negative and positive introspection (for proof and other properties
of IEL cf. [14]). The above axioms for K are not the only possible ones. Other acceptable
formulations that yield equivalent systems (without public announcement) can be found
in [14].
Kripke Semantics for IEPAL. We take an intuitionistic model with h!·i and add a
new binary knowledge relation:
Definition 11. A model M for IEPAL is a quadruple M = hW, R, υ, Ei such that
1. hW, R, υi is an intuitionistic model for IPALhi ‘defined in 2.1;
2. E is a binary knowledge relation on W coordinated with the relation R:
a) E(u) ⊆ R(u) for any state u3 , i.e., if uEv, then uRv;
b) uRv yields E(v) ⊆ E(u), i.e., if uRv and vEw, then uEw;
c) seriality, i.e., for all u, there is a v such that uEv. (alternatively, denoted as
E(u) 6= ∅ for each u ∈ W ).
3. the forcing relation is extended to epistemic assertions:
• M, x « Kϕ iff for all y ∈ E(x): M, y « ϕ.
Theorem 4 (Soundness). If `IEPAL ϕ, then S4V « ϕ4 for all ϕ ∈ LIEPAL .
2
The theorem h!ϕiKψ ↔ (ϕ → Kh!ϕiψ) is derivable.
3
R(u) and E(u) denote for some state u its the R-successors and the E-successors, respectively.
4
S4V is an extension of S4 with a verification modality.
37
Proof.
IEPAL = IEL + axioms 10 − 21.
Soundness for IEL has been proved in [14]. We have also proved soundness for IPALhi 1
and IPAL[] 3. Thus, we need to check only the soundness of the axiom 20 : h!ϕiKψ ↔
(ϕ ∧ Kh!ϕiψ). The case for axiom 21 is analogous.
→-direction
Assume that ⊮ h!ϕiKψ → (ϕ ∧ Kh!ϕiψ). Then there exists a model M and a world x,
such that: M, x ⊮ h!ϕiKψ → (ϕ ∧ Kh!ϕiψ). Then there exists an y ∈ W , y ∈ R(x):
M, y « h!ϕiKψ and M, y ⊮ (ϕ ∧ Kh!ϕiψ). Then M, y « ϕ and Mϕ , y « Kψ. Then for
all z ∈ E(y), z ∈ Mϕ : Mϕ , z « ψ.
From M, y ⊮ (ϕ ∧ Kh!ϕiψ) by def. follows either (1) M, y ⊮ ϕ or (2) M, y ⊮ Kh!ϕiψ.
Consider these two cases separately;
Case 1: M, y ⊮ ϕ, this contradicts M, y « h!ϕiKψ.
Case 2: M, y ⊮ Kh!ϕiψ. Then there exists w ∈ E(y): M, w ⊮ h!ϕiψ. Then either (1)
M, w ⊮ ϕ or (2) Mϕ , w ⊮ ψ. Consider these two cases separately:
Case 2.1: M, w ⊮ ϕ. This contradicts M, y « h!ϕiKψ (by monotonicity of forcing and
condition 2a for E, M, w « ϕ).
Case 2.2: Mϕ , w ⊮ ψ. As w ∈ E(y) and w ∈ Mϕ , then w ∈ Z where Z is a set of all
z ∈ E(y), z ∈ Mϕ . Thus contradiction with Mϕ , z « ψ.
←-direction
Assume that ⊮ (ϕ ∧ Kh!ϕiψ) → h!ϕiKψ. Then there exists a model M and a world x,
such that: M, x ⊮ (ϕ ∧ Kh!ϕiψ) → h!ϕiKψ. Then there exists an y ∈ W , y ∈ R(x):
M, y « (ϕ ∧ Kh!ϕiψ) and M, y ⊮ h!ϕiKψ. Then M, y « ϕ and M, y « Kh!ϕiψ. Then
for all z ∈ E(y): M, z « h!ϕiψ. Then M, z « ϕ and Mϕ , z « ψ.
From M, y ⊮ h!ϕiKψ by def. follows either (1) M, y ⊮ ϕ or (2) Mϕ , y ⊮ Kψ. Consider
these two cases separately:
Case 1: M, y ⊮ ϕ. Contradiction with M, y « (ϕ ∧ Kh!ϕiψ);
Case 2: Mϕ , y ⊮ Kψ. Then there exists w ∈ E(y), w ∈ Mϕ : Mϕ , w ⊮ ψ. As for
all M, z « ϕ, then w ∈ Z where Z is a set of all z ∈ E(y). Thus, contradiction with
Mϕ , z « ψ.
Theorem 5 (Completeness). If S4V « ϕ, then `IEPAL ϕ for all ϕ ∈ LIEPAL .
Proof. The proof is analogous to the one for IPALhi , theorem 2.
As a corollary, we get that S4, IPALhi and IPAL[] are equiexpressive; and S4V ,
IEPAL are equiexpressive as well.
4. Summary and Conclusion
We have investigated the possibility of a dynamic extension of the two related logics:
intuitionistic propositional logic and epistemic intuitionistic logic IEL. The epistemic
38
logic we have extended has a special understanding of knowledge as a weaker notion that
the notion of proof. We believe that this treatment of knowledge is more applicable to the
epistemology of scientific research, scientism and philosophy of science that the standard
classical S5 knowledge (justified true belief). In general, we believe that intuitionistic
logic is a useful tool for formal epistemology and our study of information update in
IEL with serve also as a useful tool for philosophical research. The study of public
announcement in IEL can shed light on the nature of information update in intuitionism
in general.
We have added two dynamic operators of public announcement that are dual in
the classical case but not in the intuitionistic. The first one can also deal with the
announcements that have already been proved w.r.t. the possible world in question
deleting only the preceding worlds. Thus, it is the most trivial update option. The second
one allows us to reason about announcements in worlds where the announced formula is
not yet true. As a result, we introduced four new formal systems (with both Hilbert-style
axiomatisation and Kripke semantics): IPALhi , IPAL[] , IEPALhi , and IEPAL[] . We
have proved soundness and completeness for all four systems. We have seen that in case
of intuitionistic epistemic logic even the simplest type of information update, i.e., public
announcement, leads to more complex system (at least because of the lack of duality).
4.1. Future research: further extensions
The above considered systems were related to non-pointed models, i.e., models where the
current state, or world, is not specified. However, in order to further develop intuitionistic
epistemology (especially knowledge progress and belief change) with the help of the
IEL system and its dynamic extensions, we should look into applying them to the
pointed models. The task of transforming Kripke models for IPALhi and IEPALhi is a
trivial. However, for IPAL[] and IEPAL[] rise questions on how to deal with the models
where the current (pointed) state x: M, x ⊮ ϕ and ϕ is the announced formula. This
problem does not arise in the classical S5 PAL as it treats truth differently and thus
such an announcement is impossible. Our conjecture is that in IPAL[] and IEPAL[]
in case of a successful announcement [!ϕ]ψ with Mϕ « ψ in the new model we should
substitute the pointed world with the one x0 that differs from the pointed one at most by
the values of ϕ and ψ. Thus, this is the topic of the future research.
Another direction of research would be to make the announcement less strict, meaning
that the announcement would give evidence of the truth of a formula but not the proof
itself. This should lead to much different systems as it will mostly relate to the knowledge
modality.
The most straightforward to ask is to add multiple agents to the system, which does not
seem to be problematic. A more intriguing question concerns the possibility of modelling
common knowledge in the above system IEL and its public announcement extensions.
Finally, the ultimate goal of the future work is to examine the possibility of other types
of information updates, rather than a simple announcements. It is also of a particular
interest to study systems of intuitionistic belief, like IEL− with respect to information
change.
39
Acknowledgments
We thank the two anonymous reviewers whose comments helped improve this paper.
The research was supported by RSF (project No.20-18-00158 “Formal philosophy of
argumentation and a comprehensive methodology for finding and selecting solutions to a
dispute”.
References
[1] P. Balbiani, D. Galmiche, About intuitionistic public announcement logic, in:
Advances in Modal Logic, 2016.
[2] I. Mezhirov, Game Semantics for Intuitionistic and Modal (Grz) Logic, Master’s
thesis, Moscow State University, Moscow, 2006.
[3] P. Lorenzen, K. Lorenz, Dialogische Logik, Wissenschaftliche Buchgesellschaft ed.,
Darmstadt, 1978.
[4] P. Urzyczyn, Intuitionistic games: Determinacy, completeness, and normalization,
Studia Logica 104 (2016) 957–1001. doi:10.1007/s11225-016-9661-4.
[5] L. E. Brouwer, Über die bedeutung des satzes vom ausgeschlossenen dritten in
der mathematik, insbesondere in der funktionentheorie. 1925 (1925) 1–7. URL:
https://doi.org/10.1515/crll.1925.154.1. doi:doi:10.1515/crll.1925.154.1.
[6] A. N. Kolmogorov, O principe tertium non datur, Matematiceskij Sbornik 32 (1925)
646–667.
[7] A. Heyting, Die formalen regeln der intuitionistischen logik i, Sitzungsberichte der
Preussischen Akademie der Wissenschaften (1930) 42–56.
[8] A. Heyting, Die formalen regeln der intuitionistischen logik ii, Sitzungsberichte der
Preussischen Akademie der Wissenschaften (1930) 57–71.
[9] A. Heyting, Die formalen regeln der intuitionistischen logik iii, Sitzungsberichte der
Preussischen Akademie der Wissenschaften (1930) 158–169.
[10] V. I. Glivenko, Sur la logique de m.brouwer, Académie Royale de Belgique. Bulletins
de la classe de sciences 5 (1928) 225–228.
[11] G. Gentzen, Untersuchungen über das logische schließen. i, Mathematische Zeitschrift
39 (1935) 176–210.
[12] K. Goedel, Zum intuitionistischen aussagenkalkül, Anzeiger der Akademie der
Wissenschaften in Wien 69 (1932) 65–66.
[13] H. van Ditmarsch, W. van der Hoek, J. Halpern, B. Kooi (Eds.), Handbook of
Epistemic Logic, College Publications, 2015.
[14] S. Artemov, T. Protopopescu, Intuitionistic epistemic logic, The Review of Symbolic
Logic 9 (2016) 266–298. doi:10.1017/S1755020315000374.
[15] T. Protopopescu, Three Essays in Intuitionistic Epistemology, Ph.D. thesis, City
University of New York, New York, 2016.
40