=Paper=
{{Paper
|id=Vol-2585/paper10
|storemode=property
|title=On interactive proof-search for constructive modal necessity
|pdfUrl=https://ceur-ws.org/Vol-2585/paper10.pdf
|volume=Vol-2585
|authors=Favio E. Miranda-Perea,Lourdes del Carmen González Huesca,P. Selene Linares-Arévalo
|dblpUrl=https://dblp.org/rec/conf/lanmr/Miranda-PereaGL19
}}
==On interactive proof-search for constructive modal necessity==
https://ceur-ws.org/Vol-2585/paper10.pdf
On interactive proof-search for constructive
modal necessity
Favio E. Miranda-Perea, Lourdes del Carmen González Huesca, and P. Selene
Linares-Arévalo
Departamento de Matemáticas, Facultad de Ciencias,
Universidad Nacional Autónoma de México
{favio,luglzhuesca,selene linares}@ciencias.unam.mx
Abstract. We present a dual sequent calculus for the necessity fragment
of the constructive modal logic S4 and show its adequacy for proof-search
in the style of modern interactive theorem provers. The main feature of
dual systems is the use of two contexts to capture the notions of true and
valid formulas, without using any formal semantics. This attribute allows
us to give simple rules for the operator that, most of the time, grant the
substitution of a strict modal reasoning by a pure propositional one, thus
simplifying the proof-search process. Moreover, we introduce a formal
notion of backward proof corresponding to a bottom-up construction of
a derivation tree by means of a left-to-right depth-first proof-search.
Keywords: Constructive Modal logic · Proof-search · necessity · sequent
calculus
1 Introduction
Modal logics play an important role in several areas of Computer Science and
Philosophy. For instance, various type systems for concurrent and distributed
computations [12,15] employ modalities and a modal lambda calculus has been
proposed to model information flow in computer networks[4]. In Artificial Intelli-
gence (AI) they are useful to model knowledge structures among agents, ontolo-
gies or the behaviour of computer systems. These and other applications oblige
to design effective and simple to use procedures for proof search in modal logics.
However, the existing processes are quite sophisticated, for instance [17,1], and
machine-oriented in the sense that their inference rules deviate from the natural
human reasoning, for they are or intend to be fully automated, like the bidirec-
tional approach of [10]. This makes the modelling of actual arguments involving
modal reasoning difficult. Such arguments arise for instance in AI, while veri-
fying an agent-based computer system; or in Philosophy, in the representation
of concrete cases in modal argumentation theory, where the operator usually
represents the argument attack relation [3,8].
In this paper we walk in the opposite direction by proposing a sequent cal-
culus adequate for proof-search but in an interactive style, as is understood and
Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0)
106
implemented in modern proof-assistants like Coq. This means that the proof-
search is driven by the human agent: the process starts with the desired sequent
S; if it is suitable as a conclusion of some rule, then the process continues with
the premises of this rule. If at the end all branches of this search end in an axiom
or initial rule, the procedure is succesful. The purpose of this work is to give a
precise formal definition of this process and to prove its equivalence with the
usual forward proof construction in the case of constructive modal logic S4 for
necessity.
2 A Dual Sequent Calculus for Necessity
The formal system GS4 hereby considered is a sequent calculus whose foun-
dations come from the analysis of [13]. Propositions are analysed judgmentally
without any semantic label (worlds). In the specific case of modal connectives by
means of judgments over propositions. The notion of so-called hypothetical judg-
ments is extended to categorical judgment where a conclusion does not depend
on hypotheses about the constructive truth of propositions. Hence, a distinction
of two forms of primitive judgments is essential: ‘A true’ means that we know
how to verify A under hypothetical judgments, whereas ‘A valid ’ represents the
fact that A is a proposition whose truth does not depend on any hypotheses, thus
internalizing a categorical judgment as a proposition syntactically represented
by the modal formula A. The system is called dual for it handles sequents
with two separate contexts of the form ∆|Γ ` A. We chose to implement such
contexts by means of two disjoint lists (instead of sets or multisets), ∆ for valid
and Γ for true hypotheses. This choice allows us to omit the labels valid, true
in context formulae, contrary to [16]. A similar separation is present in several
works: for instance the systems of [6] use global and local assumptions or the
work of [2] which discusses modal logic encodings by using separate consequence
relations (semantical and deductive) related to classical validity and truth. The
idea behind the context separation in GS4 is that formulae in ∆ are modal (i.e.
boxed formulae), whereas those in Γ are propositional. Nevertheless, like the
intuitive semantic qualifiers, this idea does not represent a syntactic restriction,
we can have arbitrary formulae in both contexts. Moreover, the succedent of a
sequent only considers true propositions, there is no need to consider valid con-
clusions explicitly as they are represented by the formula A. For the sake of
self-containment let us briefly review the elements of our syntax. Modal formulae
are generated by the following grammar:
A, B ::= pn | A → B | A ∧ B | A ∨ B | A
where pn denotes an element taken from an infinite supply of propositional
variables, indexed by a natural number. Let us also note that we do not consider
neither negation nor the constant ⊥. Therefore we will be dealing with minimal
propositional logic [18] extended with the necessity operator. A particular modal
logic is generated by adding suitable axioms. It is important to remark that
107
the logic here discussed is called constructive due to the approach of Martin-
Löf but also to distinguish it from both, the classical modal logics where the
operator obeys the axiom A ↔ ¬♦¬A and the intuitionistic modal logics which
include the axiom ¬♦⊥. In contrast, in the constructive modal logic S4 the above
axioms are omitted and both modalities are primitive. Our work only considers
the necessity modality . Contexts are implemented by means of so-called snoc
lists:
Γ, ∆ ::= · | Γ, A
These are finite lists built from the empty list, denoted here by ·, and a construc-
tor that generates a new list from a given one by adding a new element to its
right-end. The constructor called snoc is denoted by a comma. Therefore Γ, A is
the context obtained by adding A after the last element in Γ . This constructor
is opposed to the traditional cons operation, predefined in functional languages,
which adds elements at the left-end of the list 1 . The snoc lists provide a for-
malization akin to the usual practice in computer science logic where the last
context formula is the one introduced or discharged to prove an implication. The
concatenation operation is inductively defined in the obvious way and denoted
by Γ1 ; Γ2 . Also, whenever we write Γ, A; Γ 0 it means (Γ, A); Γ 0 , that is, the for-
mula A is associated to the left context. This should be clear, for the expression
Γ, (A; Γ 0 ) is ill-formed.
The system GS4 is defined by the following inference rules:
– Starting rules
(Thyp) (Vhyp)
∆|Γ, A; Γ 0 ` A ∆, A; ∆0 |Γ ` A
– Right rules
∆|Γ, A ` B ∆|Γ ` A ∆|Γ ` B
(→ R) (∧ R)
∆|Γ ` A → B ∆|Γ ` A ∧ B
∆|Γ ` A ∆|Γ ` B
(∨ R) (∨ R)
∆|Γ ` A ∨ B ∆|Γ ` A ∨ B
∆|· ` A
( R)
∆|Γ ` A
– Left rules for truth contexts.
∆|Γ, A; Γ 0 ` C ∆|Γ, B; Γ 0 ` C ∆|Γ, A, B; Γ 0 ` C
(∨ L) (∧L)
∆|Γ, A ∨ B; Γ 0 ` C ∆|Γ, A ∧ B; Γ 0 ` C
∆|Γ, A → B; Γ 0 ` A ∆, A|Γ ; Γ 0 ` B
(→L) ( L)
∆|Γ, A → B; Γ 0 ` B ∆|Γ, A; Γ 0 ` B
1
The name cons is for constructor and note that snoc is the backward reading of cons.
108
– Left rules for valid contexts.
∆, A; ∆0 |Γ ` C ∆, B; ∆0 |Γ ` C ∆, A, B; ∆0 |Γ ` C
(∨ LV) (∧LV)
∆, A ∨ B; ∆0 |Γ ` C ∆, A ∧ B; ∆0 |Γ ` C
∆, A → B; ∆0 |Γ ` A ∆, A; ∆0 |Γ ` B
(→LV) ( LV)
∆, A → B; ∆0 |Γ ` B ∆, A; ∆0 |Γ ` B
– Cut rules
∆|Γ ` A ∆|Γ, A ` B ∆|· ` A ∆, A|Γ ` B
(Cut) (CutV)
∆|Γ ` B ∆|Γ ` B
We have two starting rules allowing to use an hypothesis present in any of
the two contexts; the right rules for the connectives are the usual ones; the left
rules come in two versions, one for each context. For the case of conjunction and
disjunction these rules are also usual. The left rules for implication are new2 ,
to the best of our knowledge and capture the direct use of an implication to
prove its consequent. The right rule for corresponds to the necessitation rule.
Observe that we can introduce a formula A only in the case when we derive A
without resorting to any true hypothesis. This formulation is the key to validate
the deduction theorem in Hilbert axiomatic systems for modal logic. See for
instance [9]. The left rule L is discussed in our previous work [5] and represents
a transference principle between contexts: we can move a valid hypothesis A to
the truth context by modalizing it. Finally LV says that to use an assumption
A which is valid, it suffices to use only A. These left rules for necessity allow
to replace a modal reasoning about A, for a propositional reasoning about A.
Let us show a couple of derivations in our system.
Example 1. The following is a proof of
·|· ` (A → B) → A → (C → B)
(1) A → B , A|· ` A Vhyp
(2) A → B , A|C ` A R (1)
(3) A → B , A|C ` B → L (2)
(4) A → B , A|· ` C → B → R (3)
(5) A → B , A|· ` (C → B) R (4)
(6) A → B|A ` (C → B) L (5)
(7) A → B|· ` A → (C → B) → R (6)
(8) A → B|· ` A → (C → B) R (7)
(9) ·|(A → B) ` A → (C → B) L (8)
(10) ·|· ` (A → B) → A → (C → B) → R (9)
2
Except for a mention in our previous work [14]
109
Example 2. The following is a proof of
(B → A) ∧ (C → A) |· ` B ∨ C → A
(1) B → A , C → A|B ` B Thyp
(2) B → A , C → A|B ` A → LV (1)
(3) B → A , C → A|C ` C Thyp
(4) B → A , C → A|C ` A → LV (3)
(5) B → A , C → A|B ∨ C ` A ∨ L (2, 4)
(6) B → A , C → A|· ` B ∨ C → A → R (5)
(7) B → A , C → A|· ` (B ∨ C → A) R (6)
(8) (B → A) ∧ (C → A)|· ` (B ∨ C → A) ∧ L (7)
(9) ((B → A) ∧ (C → A))|· ` (B ∨ C → A) LV (8)
The above proofs can be read according to the usual definition of forward
derivation, though actually they were gained from a bottom-up proof construc-
tion process, which corresponds to the below notion of derivation given originally
by Kanger [11].
Definition 1 (Derivation à la Kanger). A proof or derivation of ∆|Γ ` A
is a finite sequence of sequents Π = hJ1 , . . . , Jk i such that J1 is ∆|Γ ` A and
for every 1 ≤ i ≤ k one of the following conditions hold:
– Ji is an instance of the (Hyp) or (VHyp) rules.
– For every 1 ≤ i ≤ k, Ji is the conclusion of an instance of some inference
rule with premise Jj with j > i, or premises Jj , Jl with j, l > i.
Thus, a derivation starts with the sequent sought after, whereas the usual
notion of formal proof ends with it. Also, for any given sequent, the premisses
that allow to conclude it appear later in the sequence. This gives an idea of
backward proof. Regrettably, even when this intuitive notion permeates Kanger’s
work, the concept is not engaged, for the proofs there are written forwards.
Moreover, like the examples above show, the mere sequence does not let us keep
a trace of the proof-search process. Our purpose here is to give a formal notion
of backward proof for modal logic that corresponds to the kind of techniques
implemented in proof assistants, thus resolving the just mentioned issues. But
first let us observe that GS4 indeed captures the constructive modal logic S4 for
necessity.
Theorem 1. The sequent calculus GS4 exactly captures the constructive modal
logic S4
Proof (Sketch). It is easy to show that the characteristic axioms of S4, namely
K, T and 4 are derivable in GS4. Moreover, by structural induction on the re-
spective derivability relations, we can show that GS4 is equivalent to the dual
natural deduction system NS4 of [5] (we omit the proof details due to lack of
space), where we also give a detailed and formally verified proof of the equiva-
lence of NS4 with an axiomatic system for S4.
110
3 Backward proofs in GS4
To being able to formalize our notion of backward proof, let us first introduce
a useful device to sequents, namely labelled hypotheses [7], which are pairs of
the form H : A where H is a label or shortcut to refer to A. The set of labels is
taken to be disjoint with the set of names in the current signature. A labelled
context Γ is a set of labelled hypotheses Γ = {H1 : A1 , . . . , Hn : An } where
Hi 6= Hj , if i 6= j. Moreover, in a context of the form Γ, H : A; Γ 0 we assume
that A is not in Γ ; Γ 0 and that H is a new label not used in Γ ; Γ 0 . The use of
labels does not contribute much to the usual system of forward derivations, but
as we will see soon it is very useful to the backward approach. In the following
we use labelled contexts where they account for simplicity. Otherwise, we use
conventional contexts.
The process of backward proof construction of a given sequent S consists
of searching for an inference rule R whose conclusion matches S and then to
continue the proof-search with the premisses S or S1 , S2 of R. This backward
reading of the inference rules is called a tactic. A backward proof will be a
particular sequence of tactics. Let us formalise these concepts.
Definition 2. A goal G is any sequent ∆|Γ ` A. The set of finite sequences of
goals GSeq is recursively defined as follows:
S ::= [·] | (G :: S)
where [·] denotes the empty goal sequence. Moreover, if S1 , S2 ∈ GSeq then by
S1 ; S2 we mean the concatenation3 of S1 with S2 .
We define now a transition system of tactics corresponding to backward
proof-search.
Definition 3. The transition system of tactics for GS4 is defined as follows:
– The non-empty set of states is the set of goal sequences GSeq.
– An initial state is a singleton sequence4 .
– [·] is the unique terminal state.
– The transition relation B ⊆ GSeq × GSeq is inductively defined by the below
axioms and inference rule, where a transition S1 B S2 can be read as “to
prove the sequents in S1 it suffices to prove the sequents in S2 ”.
Conclusion analysis (right sequent rules):
• intro H: ∆|Γ ` A → B B ∆|Γ, H : A ` B
• split: ∆|Γ ` A ∧ B B ∆|Γ ` A; ∆|Γ ` B
• left: ∆|Γ ` A ∨ B B ∆|Γ ` A
• right: ∆|Γ ` A ∨ B B ∆|Γ ` B
3
We use the ; for concatenation in both cases: contexts and goal sequences.
4
For clarity, a singleton sequence is identified with its unique element. That is, we
write ∆|Γ ` A instead of (∆|Γ ` A :: [·])
111
• necessitation: ∆|Γ ` A B ∆|· ` A
Premise analysis (left sequent rules):
• apply H: ∆|Γ, H : A → B; Γ 0 ` B B ∆|Γ, H : A → B; Γ 0 ` A
• apply H: ∆, H : A → B; ∆0 |Γ ` B B ∆, H : A → B; ∆0 |Γ ` A
• destruct H:∆|Γ, H : A ∧ B; Γ 0 ` C B ∆|Γ, H1 : A, H2 : B; Γ 0 ` C
• destruct H:∆, H : A ∧ B; ∆0 |Γ ` C B ∆, H1 : A, H2 : B; ∆0 |Γ ` C
• destruct H: ∆|Γ, H : A ∨ B; Γ 0 ` C B ∆|Γ, H1 : A; Γ 0 ` C ;
∆|Γ, H2 : B; Γ 0 ` C
• destruct H: ∆, H : A ∨ B; ∆ |Γ ` C B ∆, H1 : A; ∆0 |Γ ` C ;
0
∆, H2 : B; ∆0 |Γ ` C
• destruct H: ∆|Γ, H : A; Γ ` B B ∆, H1 : A|Γ ; Γ 0 ` B
0
• destruct H: ∆, H : A; ∆0 |Γ ` B B ∆, H : A; ∆0 |Γ ` B
Lemma Assertion:
• assert A: ∆|Γ ` C B ∆|Γ ` A; ∆|Γ, H : A ` C
• cut A: ∆|Γ ` C B ∆|Γ, H : A ` C; ∆|Γ ` A
• vassert A: ∆|Γ ` C B ∆|· ` A; ∆, H : A|Γ ` C
• vcut A: ∆|Γ ` C B ∆, H : A|Γ ` C ; ∆|· ` A
Discarding tactics:
• assumption: ∆|Γ, A; Γ 0 ` A B [·].
• vassumption: ∆, A; ∆0 |Γ ` A B [·].
Sequencing:
S1 B S2
(seq)
S1 ; S B S2 ; S
A basic transition transforms a singleton goal sequence into a, perhaps empty,
sequence of subgoals dictated by the backwards reading of an inference rule of
GS4. The (seq) rule determines the order in which goals are solved, namely from
the first (most left) goal in the current sequence of pending goals. Also observe
that each cut rule has two corresponding tactics, namely cut and assert. The
difference being only operational: either we first prove the lemma and then use
it or viceversa.
Finally we can give the promised definition of a backward proof.
Definition 4. A backward proof of ∆|Γ ` A is a finite sequence of states
S1 , . . . , Sk such that
– S1 is ∆|Γ ` A
– For every 1 ≤ i < k, Si B Si+1
– Sk is [·]
Therefore a backward proof of a sequent ∆|Γ ` A is a finite sequence of tactics
that ends in the empty sequence of goals [·], meaning that the proof-search of
the original goal ∆|Γ ` A has no pending subgoals left to prove. This transition
sequence of tactics corresponds to the bottom-up construction of a derivation
tree by means of a left-to-right depth-first proof search.
Let us present now some particular examples of backward proofs that intend
to show the adequacy of our secuent calculus GS4 for interactive proof-search.
112
Example 3. The following is a backward proof of
·|H1 : (P → Q) ∨ R ` (P ∨ R) → (Q ∨ R)
·|H1 : (P → Q) ∨ R ` (P ∨ R) → (Q ∨ R)
B destruct H1
H1 : (P → Q) ∨ R|· ` (P ∨ R) → (Q ∨ R)
B necessitation
H1 : (P → Q) ∨ R|· ` (P ∨ R) → (Q ∨ R)
B intro H2
H1 : (P → Q) ∨ R|H2 : (P ∨ R) ` (Q ∨ R)
B destruct H2
H1 : (P → Q) ∨ R , H2 : P ∨ R|· ` (Q ∨ R)
B necessitation
H1 : (P → Q) ∨ R , H2 : P ∨ R|· ` Q ∨ R
B destruct H2
H1 : (P → Q) ∨ R , H2 : P |· ` Q ∨ R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B destruct H1
H1 : P → Q , H2 : P |· ` Q ∨ R ;
H1 : R , H2 : P |· ` Q ∨ R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B left
H1 : P → Q , H2 : P |· ` Q ;
H1 : R , H2 : P |· ` Q ∨ R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B apply H1
H1 : P → Q , H2 : P |· ` P ;
H1 : R , H2 : P |· ` Q ∨ R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B vassumption
H1 : R , H2 : P |· ` Q ∨ R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B right
H1 : R , H2 : P |· ` R ;
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B vassumption
H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R
B right
H1 : (P → Q) ∨ R , H2 : R|· ` R
B vassumption
[·]
113
Example 4. The following is a proof of
∆|· ` (A ∧ D) → E
where ∆ =def H1 : A → (B ∧ C), H2 : (D ∧ C) → (E ∧ F ).
∆|· ` (A ∧ D) → E
B intro H3
∆|H3 : (A ∧ D) ` E
B destruct H3
∆ , H3 : A ∧ D|· ` E
B destruct H3
∆ , H3 : A , H4 : D|· ` E
B vassert (B ∧ C)
∆ , H3 : A , H4 : D|· ` (B ∧ C) ;
∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E
B apply H1
∆ , H3 : A , H4 : D|· ` A ;
∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E
B vassumption
∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E
B destruct H5
∆ , H3 : A , H4 : D , H5 : B ∧ C|· ` E
B destruct H5
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` E
B vassert (E ∧ F )
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` (E ∧ F ) ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B apply H2
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` (D ∧ C) ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B necessitation
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` D ∧ C ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B split
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` D ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` C ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B vassumption
∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` C ;
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B vassumption
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E
B destruct H7
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : E ∧ F |· ` E
B destruct H7
∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : E , H8 : F |· ` E
B vassumption
[·]
114
The above example shows the utility of the cut rule with a valid hypothesis,
implemented by means of the vassert tactic.
We discuss next the equivalence of backward and forward proofs.
4 Equivalence
In this section we formally prove that our backward approach is equivalent to
the usual notion of (forward) derivation. Let us start by noting that, according
to definition 4, a backward proof is a chaining sequence of particular instances of
the relation B. Therefore a backward proof of the sequent ∆|Γ ` A corresponds
to an instance of the transitive closure of the B relation. For the proof of the
equivalence, it will be useful to work directly with this relation.
Definition 5. The transitive closure of the relation B, denoted B+ , is induc-
tively defined by the following rules:
S B S0 S B S 0 S 0 B+ S 00
(tc1) (tc2)
S B+ S 0 S B+ S 00
Lemma 1. The following rule is admissible:
S1 B+ S2
(seq + )
S1 ; S B+ S2 ; S
Proof. Induction on S1 B+ S2 . If S1 B S2 , then the rule (seq) yields S1 ; S B S2 ; S
and by rule (tc1) we get S1 ; S B+ S2 ; S. Assume now that S1 B S10 and S10 B+ S2 .
By rule (seq) we have S1 ; S B S10 ; S and the I.H. yields S10 ; S B+ S2 ; S, therefore
rule (tc2) allows us to conclude S1 ; S B+ S2 ; S. t
u
Definition 6. We say that a goal sequence S =def G1 , . . . , Gk is solvable, if Gi
is derivable for all 1 ≤ i ≤ k.
The next lemma shows that solvability of sequences is rearward preserved by
the transition relation B.
Lemma 2. If S1 B S2 and the sequence S2 is solvable then S1 is solvable.
Proof. It is clear that the property holds for the basic transitions, since these
correspond to the inference rules of our sequent calculus. The result follows by
an easy induction on B. t
u
The above property is easily lifted to the transitive closure B+ .
Lemma 3. If S1 B+ S2 and the sequence S2 is solvable then S1 is solvable.
Proof. Induction on S1 B+ S2 . t
u
We are now ready to prove the desired equivalence.
115
Theorem 2 (Equivalence of forward and backward proofs). Let ∆|Γ ` A
be any sequent. The following conditions are equivalent:
– ∆|Γ ` A is derivable
– ∆|Γ ` A B+ [·]
Proof. The ⇐) direction is immediate from lemma 3, since the sequence [·] is
trivially solvable. We prove the ⇒) direction by induction on the derivability of
∆|Γ ` A.We show here only some cases leaving the others to the reader.
– Case (Vhyp). The vassumption tactic yields ∆, H : A; ∆0 |Γ ` A B [·].
– Case (∧ R). A backward derivation of ∆|Γ ` A ∧ B is the following:
∆|Γ ` A ∧ B B ∆|Γ ` A; ∆|Γ ` B B+ [·]; ∆|Γ ` B B+ [·]; [·] = [·]
The split tactic yields the first transition, after that, the second step is an
application of the rule (seq + ) using the IH ∆|Γ ` A B+ [·]; finally, the last
step is justified by the IH ∆|Γ ` B B+ [·].
– Case (→ LV). The backward derivation of ∆, A → B; ∆0 |Γ ` B is
∆, A → B; ∆0 |Γ ` B B ∆, A → B; ∆0 |Γ ` A B+ [·]
where the first step corresponds to the apply tactic and the second is given
by the IH.
– Case (Cut). A backward derivation of ∆|Γ ` B is given by the following
transition sequence:
∆|Γ ` B B ∆|Γ ` A ; ∆|Γ, A ` B B+ [·]; ∆|Γ, A ` B B+ [·]; [·] = [·]
where the first step is an instance of the assert A tactic, and the remaining
are gained from the inductive hypotheses.
The above theorem guarantees the reliability of the proof-search process: if
∆|Γ ` A is derivable then the interactive proof-search process succeeds and
viceversa. This finishes our exposition.
5 Final Remarks
In this paper we presented a dual sequent calculus GS4 for the constructive
modal logic S4 of necessity, and showed that it is adequate for interactive back-
ward proof-search. The rules for handling the necessity operator are simple and
intuitive due to the use of dual contexts, a feature that also let us define, in a
simple way, a bottom-up construction process by means of a left-to-right depth-
first proof-search. This procedure was captured with a formal notion of backward
proof which results equivalent to the usual definition of forward proof. This work
is the first step in a study of proof-search in modal logic whose natural continu-
ation consists in the proof of the cut-elimination theorem in order to validate if
GS4 is loop-free and then can be also adequate for full automatization. As usual,
116
a proof of cut-elimination is not trivial. In our particular case we actually need
to eliminate the two versions (Cut) and (CutV) of the cut-rule. However, the
rules (L) and (LV) for the necessity operator allow us to prove the admissi-
bility of (CutV) from that of (Cut) in a direct way. We are currently finding out
if we can do the same for the left rules for valid contexts, a feature that would
heavily simplify the proof of cut-elimination for the rule (Cut). Another part
of this future inquiry is the extension of the current approach to the full modal
logic S4, both constructively, where ♦ is not a dual of , but also classically. In
this last case additional research about proof-search with negation is required.
The final purpose of this program is to show the utility of our deductive systems
for actual case studies in some specific areas, like argumentation theory in the
lines of [3,8] or proof-search in multi-agent dialogues related to the work of [19].
References
1. Julius Andrikonis. Loop-free calculus for modal logic s4. i. Lithuanian Mathemat-
ical Journal, 52(1):1–12, Jan 2012.
2. Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano. Encoding
Modal Logics in Logical Frameworks. Studia Logica, 60(1):161–208, Jan 1998.
3. Guido Boella, Joris Hulstijn, and Leendert van der Torre. A logic of abstract argu-
mentation. In Simon Parsons, Nicolas Maudet, Pavlos Moraitis, and Iyad Rahwan,
editors, Argumentation in Multi-Agent Systems, pages 29–41, Berlin, Heidelberg,
2006. Springer Berlin Heidelberg.
4. Tijn Borghuis and Loe Feijs. A constructive logic for services and information flow
in computer networks. The Computer Journal, 43(4):274–289, 01 2000.
5. Lourdes del Carmen Gonzlez-Huesca, Favio E. Miranda-Perea, and P. Selene
Linares-Arévalo. Axiomatic and dual systems for constructive necessity, a formally
verified equivalence. Journal of Applied Non-Classical Logics, 29(3):255–287, 2019.
6. Melvin C. Fitting. Proof Methods for Modal and Intuitionistic Logics. Synthese
Library. Springer Netherlands, 1983.
7. D. M. Gabbay. Introduction to labelled deductive systems. In Handbook of Philo-
sophical Logic, pages 179–266. Springer Netherlands, 2014.
8. Davide Grossi. Argumentation in the view of modal logic. In Peter McBurney,
Iyad Rahwan, and Simon Parsons, editors, Argumentation in Multi-Agent Systems,
pages 190–208, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
9. Raul Hakli and Sara Negri. Does the deduction theorem fail for modal logic?
Synthese, 187(3):849–867, 2012.
10. Samuli Heilala and Brigitte Pientka. Bidirectional decision procedures for the
intuitionistic propositional modal logic is4. pages 116–131, 09 2007.
11. Stig Kanger. Provability in logic. In Ghita Holmström-Hintikka, Sten Lindström,
and Rysiek Sliwinski, editors, Collected Papers of Stig Kanger with Essays on
His Life and Work, volume 1 of Synthese Library: Studies in Epistemology, Logic,
Methodology, and Philosophy of Science, pages 8–41. Kluwer Academic Publishers
(Kluwer Academic Publishers Group), 2001. Originally published as Provability
in Logic. Acta Universitatis Stockholrnensis, Stockholm Studies in Philosophy I.
University of Stockholm 1957.
117
12. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concur-
rent linear logic programming. In Proceedings of the 7th International ACM SIG-
PLAN Conference on Principles and Practice of Declarative Programming, July
11-13 2005, Lisbon, Portugal, pages 35–46, 2005.
13. Per Martin-Löf. On the meanings of the logical constants and the justifications of
the logical laws. Nordic J. Philos. Logic, 1(1):11–60, 1996.
14. Favio E. Miranda-Perea, P. Selene Linares-Arévalo, and Atocha Aliseda-Llera. How
to prove it in natural deduction: A tactical approach. CoRR, abs/1507.03678, 2015.
15. Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric
modal lambda calculus for distributed computing. In Proceedings of the 19th An-
nual IEEE Symposium on Logic in Computer Science, LICS ’04, pages 286–295,
Washington, DC, USA, 2004. IEEE Computer Society.
16. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic.
Mathematical Structures in Comp. Sci., 11(4):511–540, 2001.
17. Regimantas Pliukeviius and Aida Pliukeviien. A new method to obtain termination
in backward proof search for modal logic s4. Journal of Logic and Computation,
20(1):353–379, 11 2008.
18. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Iso-
morphism, Volume 149 (Studies in Logic and the Foundations of Mathematics).
Elsevier Science Inc., New York, NY, USA, 2006.
19. Martin Sticht. Proof Search in Multi-Agent Dialogues for Modal Logic. PhD thesis,
University of Bamberg Press, Universitätsbibliothek Bamberg, 2018. doctoralthe-
sis.
118