=Paper=
{{Paper
|id=None
|storemode=property
|title=Focusing on Contraction
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-l05.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/AvelloneFM13
}}
==Focusing on Contraction==
https://ceur-ws.org/Vol-1068/paper-l05.pdf
Focusing on contraction
Alessandro Avellone1 , Camillo Fiorentini2 , Alberto Momigliano2
1
DISMEQ, Università degli Studi di Milano-Bicocca
2
DI, Università degli Studi di Milano
Abstract. Focusing [1] is a proof-theoretic device to structure proof
search in the sequent calculus: it provides a normal form to cut-free
proofs in which the application of invertible and non-invertible inference
rules is structured in two separate and disjoint phases. It is commonly
believed that every “reasonable” sequent calculus has a natural focused
version. Although stemming from proof-search considerations, focusing
has not been thoroughly investigated in actual theorem proving, in par-
ticular w.r.t. termination, if not for the folk observations that only neg-
ative formulas need to be duplicated (or contracted if seen from the top
down) in the focusing phase. We present a contraction-free (and hence
terminating) focused proof system for multi-succedent propositional intu-
itionistic logic, which refines the G4ip calculus of Vorob’ev, Hudelmeier
and Dyckhoff. We prove the completeness of the approach semantically
and argue that this offers a viable alternative to other more syntactical
means.
1 Introduction and related work
Focusing [1] is a proof-theoretic device to structure proof search in the sequent
calculus: it provides a normal form to cut-free proofs in which the application
of invertible and non-invertible inference rules is structured in two separate and
disjoint phases. In the first, called the negative or asynchronous phase, we apply
(reading the proof bottom up) all invertible inference rules in whatever order,
until none is left. The second phase, called the positive or synchronous phase,
“focuses” on a formula, by selecting a not necessarily invertible inference rule.
If after the (reverse) application of that introduction rule, a sub-formula of that
focused formula appears that also requires a non-invertible inference rule, then
the phase continues with that sub-formula as the new focus. The phase ends
either with success or when only formulas with invertible inference rules are en-
countered and phase one is re-entered. Certain “structural” rules are used to
recognize this switch. Compare this to standard presentation of proof search,
such as [22], where Waaler and Wallen describe a search strategy for the intu-
itionistic multi-succedent calculus LB by dividing rules in groups to be applied
following some priorities and a set of additional constraints. This without a proof
of completeness. Focusing internalizes in the proof-theory a stringent strategy,
and a provably complete one, from which many additional optimizations follow.
66 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
Contraction (or duplication, seen from the bottom up) is one of Gentzen’s
original structural rules permitting the reuse of some formula in the antecedent
or succedent of a sequent:
Γ, A, A ` ∆ Γ ` A, A, ∆
Contr L Contr R
Γ, A ` ∆ Γ ` A, ∆
We are interested in proof search for propositional logics and from this stand-
point contraction is a rather worrisome rule: it can be applied at any time mak-
ing termination problematic even for decidable logics, thus forcing the use of
potentially expensive and non-logical methods like loop detection. It is therefore
valuable to ask whether contraction can be removed, in particular in the context
of focused proofs.
As it emerged from linear logic, focusing naturally fits other logics with strong
dualities, such as classical logic. As such, it is maybe not surprising that issue
of contraction has not been fully investigated: in linear logic contraction (and
weakening) are tagged by exponentials, while in classical logic duplication does
not affect completeness. As far as intuitionistic logic, an important corollary of
the completeness of focusing is that contraction is exactly located in between
the asynchronous and synchronous phases and can be restricted to negative
formulas3 . This is a beginning, but it is well-known (see the system G3ip [21])
that the only propositional connective we do need to contract is implication.
There is a further element: Gentzen’s presentation of intuitionistic logic is ob-
tained from his classical system LK by means of a cardinality restriction imposed
on the succedent of every sequent: at most one formula occurrence. This has been
generalized by Maehara (see [15]), who retained a multiple-conclusion version,
provided that the rules for right implication (and universal quantification) can
only be performed if there is a single formula in the succedent of the premise to
which these rules are applied. As these are the same connectives where in the
Kripke semantics a world jump is required, this historically opened up a fecund
link with tableaux systems. Moreover, Maehara’s LB (following [22]’s terminol-
ogy) has more symmetries from the permutation point of view and therefore may
seem a better candidate for focusing than mono-succedent LJ. The two crucial
rules are:
Γ, A → B ` A, ∆ Γ, B ` ∆ Γ, A ` B
→L →R
Γ, A → B ` ∆ Γ ` A → B, ∆
Interestingly here, in opposition to LJ, the → L rule is invertible, while → R
is not. According to the focusing diktat, → L would be classified as left asyn-
chronous and eagerly applied, and this makes the asynchronous phase endless.
While techniques such as freezing [4] or some form of loop checking could be
used, we exploit a well-known formulation of a contraction-free calculus, known
as G4ip [21], following Vorob’ev, Hudelmeier and Dyckhoff, where the → L rule
is replaced by a series of rules that originate from the analysis of the shape of
3
Recall that in LJ a formula is negative (positive) if its right introduction rule is
invertible (non-invertible).
Focusing on contraction 67
the subformula A of the main formula A → B of the rule. It is then routine that
such a system is indeed terminating, in the sense that any bottom-up derivation
of any given sequent is of finite length4 . It is instead not routine to focalize such
a system, called G4ipf , and this is the main result of the present paper.
As the focusing strategy severely restricts proofs construction, it is paramount
to show that we do not lose any proof – in other terms that focusing is complete
w.r.t. standard intuitionistic logic. There are in the literature several ways to
prove that, all of them proof-theoretical and none of them completely satisfac-
tory for our purposes:
1. The permutation-based approach, dating back to Andreoli [1], works by
proving inversion properties of asynchronous connectives and postponement
properties of synchronous ones. This is very brittle and particularly prob-
lematic for contraction-free calculi: in fact, it requires to prove at the same
time that contraction is admissible and in the focusing setting this is far
from trivial.
2. One can establish admissibility of the cut and of the non-atomic initial rule
in the focused calculus and then show that all ordinary rules are admissible
in the latter using cut. This has been championed in [8]. While a syntactic
proof of cut-elimination is an interesting result per se, the sheer number
of the judgments involved and hence of the cut reductions (principal, focus,
blur, commutative and preserving cuts in the terminology of the cited paper)
makes the well founded-ness of the inductive argument very delicate and hard
to extend.
3. The so-called “grand-tour through linear logic” strategy of Miller and Liang [14].
Here, to show that a refinement of an intuitionistic proof system such as ours
is complete, we have to provide an embedding into LLF (the canonical fo-
cused system for full linear logic) and then show that the latter translation
is entailed by Miller and Liang’s 1/0 translation. The trouble here is that
contraction-free systems cannot be faithfully encoded in LLF [18]. While
there are refinements of LLF, namely linear logic with sub-exponentials [20],
which may be able to faithfully encode such systems, a “grand-tour” strategy
in this context is uncharted territory. Furthermore, sub-exponential encod-
ings of focused systems tend to be very, very prolix, which makes closing the
grand-tour rather unlikely.
4. Finally, Miller and Saurin propose a direct proof of completeness of focusing
in linear logic in [19] based on the notion of focalization graph. Again, this
seems hard to extend to asymmetric calculi such as intutionism, let alone
those contraction-free.
In this paper, instead, we prove completeness adapting the traditional Kripke
semantic argument. While this is well-worn in tableaux-like systems, it is the first
time that the model-theoretic semantics of focusing has been considered. The
highlights of our proof are explained in Section 3.3.
4
With some additional effort, one can prove that contraction is admissible in the
contraction-free calculus [10].
68 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
Although stemming from proof-search considerations, focusing has still to
make an impact in actual theorem proving. Exceptions are:
– Inverse-based systems such as Imogen [16] and LIFF [7]: because the inverse
method is forward and saturation-based, the issue of contraction does not
come into play – in fact it exhibits different issues w.r.t. termination (namely
subsumption) and is in general not geared towards finite failure.
– TAC [5] is a prototype of a family of focused systems for automated inductive
theorem proving, including one for LJF. Because the emphasis is on the
automation of inductive proofs and the objective is to either succeed or
quickly fail, most care is applied to limit the application of the induction
rule by means of freezing. Contraction is handled heuristically, by letting the
user set a bound for how many time an assumption can be duplicated for
each initial goal; once the bound is reached, the system becomes essentially
linear.
– Henriksen’s [13] presents an analysis of contraction-free classical logic: here
contraction has an impact only in the presence of two kinds of disjunc-
tion/conjunctions, namely positive vs. negative, as in linear logic. The au-
thor shows that contraction can be disposed of by viewing the introduction
rule for positive disjunction as a restart rule, similar to Gabbay’s [12]:
` Θ, pos(A) ⇓ B
plus dual
` Θ ⇓ A ∨+ B
where pos(A) = A ∧+ t+ delays the non-chosen branch if A is negative (Θ is
positive only), and the focus left rule does not make any contraction. This
is neat, but not helpful as far as LB is concerned.
2 The proof system
We consider a standard propositional language based on a denumerable set of
atoms, the constant ⊥ and the connectives ∧, ∨ and →; ¬A stands for A → ⊥.
Our aim is to give a focalized version of the well-known contraction-free calculus
G4ip of Vorob’ev, Hudelmeier and Dyckhoff [21]. To this end, one starts with
a classification of formulas in the (a)synchronous categories. In focused versions
of LJ such as LJF [14], an asynchronous formula has a right invertible rule
and a non-invertible left one – and dually for synchronous. The contraction-
free approach does not enjoy this symmetry – the idea is in fact to consider
the possible shape that the antecedent of an implication can have and provide
a specialized left (and here right5 ) introduction rule, yielding a finer view of
implicational connectives, which now come in pairs. As we shall see shortly,
formulas of the kind (A → B) → C have non-invertible left and right rules, while
the intro rules for (A ∧ B) → C and (A ∨ B) → C are both invertible. Formulas
5
And in this sense our calculus is reminiscent of Avron’s decomposition proof sys-
tems [3].
Focusing on contraction 69
a → B, with a an atom, have a peculiar behaviour: right rule is non-invertible,
left rule is invertible, but can be applied only if the left context contains the
atom a. This motivates the following, slight unusual, classification of formulas –
we discuss the issue of polarization of atoms in Section 4.
Async Formula (AF) ::= ⊥ | A ∧ B | A ∨ B | ⊥ → B | (A ∧ B) → C | (A ∨ B) → C
Sync Formula (SF) ::= a | a → B | (A → B) → C where a is an atom
AF+ ::= a | AF
SF− ::= a non-atomic SF
The calculus is based on the following judgments, whose rules are displayed in
Figure 1:
– Θ; Γ =⇒ ∆; Ψ . Active sequent;
– Θ; A Ψ . Left-focused sequent;
– Θ A; Ψ . Right-focused sequent.
Γ and ∆ denote multisets of formulas, while Θ and Ψ denote multisets of SF.
We use the standard notation of [21]; for instance, by Γ, ∆ we mean multiset
union of Γ and ∆.
Proof search alternates between an asynchronous phase, where asynchronous
formulas are considered, and a synchronous phase, where synchronous ones are.
The dotted lines highlights the rule that govern the phase change. In the asyn-
chronous phase we eagerly apply the asynchronous rules to active sequents
Θ; Γ =⇒ ∆; Ψ . If the main formula is an AF, the formula is decomposed; oth-
erwise, it is moved to one of the outer contexts Θ and Ψ (rule ActL or ActR ).
When the inner contexts are emptied (namely, we get a sequent of the form
Θ; · =⇒ ·; Ψ ), no asynchronous rule can be applied and the synchronous phase
starts by selecting a formula H in Θ, Ψ for focus (rule FocusL or FocusR ). Dif-
ferently from the asynchronous phase, the rules to be applied are determined by
the formula under focus. Note that the choice of H determines a backtracking
point: if proof search yields a sequent where Θ only contains atoms and Ψ is
empty, no formula can be picked and the construction of the derivation fails; to
continue proof search, one has to backtrack to the last applied FocusL or FocusR
rule and select, if possible, a new formula for focus. The left-focused phase is
started by the application of rule FocusL and involves left-focused sequents of
the form Θ; A Ψ . Here we analyze implications whose antecedents are either a
or A → B. In the first case (rule → at), we perform a sort of forward application
of modus ponens, provided that a ∈ Θ, otherwise we backtrack. The application
of rule →→ L determines a transition to a new asynchronous phase in the left
premise, while focus is maintained in the right premise. The phase terminates
when an AF+ formula is produced with a call to rule BlurL . Alternatively, a
right-focused phase begins by selecting a formula H in Ψ (rule FocusR ). Let us
assume that H is an atom. If H ∈ Θ, we apply the axiom-rule Init and the
construction of a closed branch succeeds; otherwise, we get a failure and we have
to backtrack. If H = K → B, we apply → R, which ends the synchronous phase
and starts a new asynchronous phase. This is similar to the LJQ system [9].
70 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
⊥L Θ; Γ =⇒ ∆; Ψ
Θ; Γ, ⊥ =⇒ ∆; Ψ ⊥R
Θ; Γ =⇒ ⊥, ∆; Ψ
Θ; Γ, A, B =⇒ ∆; Ψ Θ; Γ =⇒ A, ∆; Ψ Θ; Γ =⇒ B, ∆; Ψ
∧L ∧R
Θ; Γ, A ∧ B =⇒ ∆; Ψ Θ; Γ =⇒ A ∧ B, ∆; Ψ
Θ; Γ, A =⇒ ∆; Ψ Θ; Γ, B =⇒ ∆; Ψ Θ; Γ =⇒ A, B, ∆; Ψ
∨L ∨R
Θ; Γ, A ∨ B =⇒ ∆; Ψ Θ; Γ =⇒ A ∨ B, ∆; Ψ
Θ; Γ =⇒ ∆; Ψ ⊥→R
⊥→L Θ; Γ =⇒ ⊥ → B, ∆; Ψ
Θ; Γ, ⊥ → B =⇒ ∆; Ψ
Θ; Γ, A → B → C =⇒ ∆; Ψ Θ; Γ =⇒ A → B → C, ∆; Ψ
∧→L ∧→R
Θ; Γ, (A ∧ B) → C =⇒ ∆; Ψ Θ; Γ =⇒ (A ∧ B) → C, ∆; Ψ
Θ; Γ, A → C, B → C =⇒ ∆; Ψ Θ; Γ =⇒ A → C, ∆; Ψ Θ; Γ =⇒ B → C, ∆; Ψ
∨→L ∨→R
Θ; Γ, (A ∨ B) → C =⇒ ∆; Ψ Θ; Γ =⇒ (A ∨ B) → C, ∆; Ψ
Θ, S; Γ =⇒ ∆; Ψ L
Θ; Γ =⇒ ∆; S, Ψ R
Θ; Γ, S =⇒ ∆; Ψ Act Θ; Γ =⇒ S, ∆; Ψ Act
.....................................................................................
Θ; S − Ψ Θ S; Ψ Θ; T =⇒ ·; Ψ
FocusL Θ; · =⇒ ·; S, Ψ Focus
R
BlurL
Θ, S − ; · =⇒ ·; Ψ Θ; T Ψ
.....................................................................................
Init Θ; K =⇒ B; ·
Θ, a a; Ψ →R
Θ K → B; Ψ
Θ, a; B Ψ Θ; A, B → C =⇒ B; · Θ; C Ψ
→ at →→ L
Θ, a; a → B Ψ Θ; (A → B) → C Ψ
A, B and C are any formulas, S is a SF, S − is a SF− , T is a AF+ and K → B is a SF.
Fig. 1. The G4ipf calculus
We remark that the main difference between G4ipf and a standard focused
calculus such as LJF is that the rule FocusL does not require the contraction of
the formula selected for focus. This is a crucial point to avoid the generation of
branches of infinite length and to guarantee the termination of the proof search
procedure outlined above (see Section 3.1).
A derivation D of a sequent σ in G4ipf is a tree of sequents built bottom-up
starting from σ and applying backward the rules of G4ipf . A branch of D is a
sequence of sequents corresponding to the path from the root σ of D to a leaf
σl of D. If σl is the conclusion of one of the axiom-rules ⊥L, ⊥ → R and Init
(the rules with no premises), the branch is closed. A derivation is closed if all
its branches are closed. A sequent σ is provable in G4ipf if there exists a closed
derivation of σ; a formula A is provable if the active sequent ·; · =⇒ A; · with
empty contexts Θ, Γ and Ψ is provable.
Focusing on contraction 71
Example 1. Here we provide an example of a G4ipf -derivation of the formula
¬¬(a ∨ ¬a). Recall that a derivation of such a formula in the standard calculus
requires an application of contraction.
⊥L
a; ⊥ =⇒ ·; L
a; ⊥ · Blur
a; ¬a · → at L
¬a, a; · =⇒ ·; · Focus ¬a; ⊥ =⇒ ·; ·
⊥L
[⊥R, ⊥ → L, ActL ] L
¬a; a, ⊥ → ⊥ =⇒ ⊥; · ¬a; ⊥ · Blur
¬a; ¬¬a · →→ L
L
¬a, ¬¬a; · =⇒ ·; · Focus
[⊥R, ∨ → L, ActL × 2]
·; ¬(a ∨ ¬a) =⇒ ⊥; ·
→R
· ¬¬(a ∨ ¬a); ·
FocusR
·; · =⇒ ·; ¬¬(a ∨ ¬a)
ActR
·; · =⇒ ¬¬(a ∨ ¬a); ·
The double line corresponds to an asynchronous phase where more than one rule
is applied. The only backtracking point is the choice of the formula for left-focus
in the active sequent ¬a, ¬¬a; · =⇒ ·; ·. If we select ¬a instead of ¬¬a, we get the
sequent ¬¬a; ¬a · and the construction of the derivation immediately fails.
3 Meta-theory
We show that proof search in G4ipf can be performed in finite time. We define
a well-founded relation ≺ such that, if σ is the conclusion of a rule R of G4ipf
and σ 0 any of the premises of R, then σ 0 ≺ σ. As a consequence, branches of
infinite length cannot be generated in proof search and the provability of σ in
G4ipf can be decided in finite time.
3.1 Termination
We assign to any formula A a weight wg(A) following [21]:
wg(a) = wg(⊥) = 2 wg(A ∧ B) = wg(A) + wg(A) · wg(B)
wg(A ∨ B) = 1 + wg(A) + wg(B) wg(A → B) = 1 + wg(A) · wg(B)
The weight wg(σ) of a sequent σ is the sum of wg(A), for every A in σ. One can
easily prove that the following properties hold:
– wg(A → (B → C)) < wg((A ∧ B) → C);
– wg(A → C) + wg(B → C) < wg((A ∨ B) → C);
– wg(A) + wg(B → C) + wg(C) < wg((A → B) → C).
72 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
The above properties suffice to prove that proof search in the calculus G4ip
terminates. Indeed, if R is a rule of G4ip, σ1 the conclusion of R and σ2 any
of the premises of R, it holds that wg(σ2 ) < wg(σ1 ); since weights are positive
numbers, we cannot generate branches of infinite length. On the other hand, in
G4ipf we cannot use the weight of the whole sequent as a measure, since we
have rules where the conclusion and the premise have the same weight (Focus,
Act and Blur).
Let ≺s (≺d ) be the smallest relation between two sequents related by a rule
of the same (different) judgment such that σ1 ≺s σ2 (σ1 ≺d σ2 ) if there exists a
rule R of G4ipf such that σ2 is the conclusion of R and σ1 is any of the premises
of R. For instance:
( Θ; Γ, A =⇒ ∆; Ψ ) ≺s ( Θ; Γ, A ∨ B =⇒ ∆; Ψ ) ( Θ, a; B Ψ ) ≺s ( Θ, a; a → B Ψ )
( Θ; A =⇒ B; · ) ≺d ( Θ A → B; Ψ ) ≺d ( Θ; · =⇒ ·; A → B, Ψ )
Note that σ1 ≺s σ2 implies wg(σ1 ) ≤ wg(σ2 ); moreover, if σ1 ≺d σ2 then
wg(σ1 ) = wg(σ2 ).
Using as a measure the lexicographic ordering of hwg(A), wg(Γ ), wg(∆)i we
can show (see the proof in the Appendix):
Lemma 1. ≺s is a well-founded relation.
The relation ≺d corresponds to the application of a rule which starts or ends
a synchronous phase. Note that a synchronous phase cannot start by selecting
an atom (indeed, the formula S − chosen for focus by FocusL must be a SF− ),
otherwise we could generate an infinite loop where an atom a is picked for focus
by FocusL and immediately released by BlurL . As a consequence, we cannot have
chains of the form σ1 ≺d σ2 ≺d σ3 , but between two ≺d at least an ≺s must
occur. In the following lemma we show that two active sequents immediately
before and after a synchronous phase have decreasing weights.
Lemma 2. Let σa and σb be two active sequents, let σ1 , . . . , σn be n ≥ 1 focused
sequents such that σa ≺d σ1 ≺s · · · ≺s σn ≺d σb . Then wg(σa ) < wg(σb ).
Proof. By definition of ≺d , σn is obtained by applying FocusL or FocusR to
σb , σa is obtained by applying BlurL or → R to σ1 , while in σ1 , . . . , σn only
synchronous rules are applied. If n = 1, we have two possible cases:
1. σa = Θ; A, B → C =⇒ B; ·
σ1 = Θ; (A → B) → C Ψ
σb = Θ, (A → B) → C; · =⇒ ·; Ψ ;
2. σa = Θ; A =⇒ B; ·
σ1 = Θ A → B; Ψ
σb = Θ; · =⇒ ·; A → B, Ψ (where A is an atom or an implication).
In both cases wg(σa ) < wg(σb ). Let n > 1. We have:
σa = Θ; H1 =⇒ ·; Ψ, σ1 = Θ; H1 Ψ, ... σn = Θ; Hn Ψ
σb = Θ, Hn ; · =⇒ ·; Ψ
Since wg(H1 ) < wg(Hn ), it holds that wg(σa ) < wg(σb ). t
u
Focusing on contraction 73
Let ≺ be the transitive closure of the relation ≺s ∪ ≺d . Note that σ1 ≺ σ2
implies wg(σ1 ) ≤ wg(σ2 ). Using lemmas 1 and 2, one can prove that (see the
proof in the Appendix):
Proposition 1. ≺ is a well-founded order relation.
By Proposition 1, every branch of a derivation of G4ipf has finite length. Indeed,
let D be a (possibly open) derivation of σ1 and let σ1 , σ2 , . . . be a branch of D.
We have σi+1 ≺ σi for every i ≥ 1, hence the branch has finite length.
3.2 Semantics
A Kripke model is a structure K = hP, ≤, ρ, V i, where hP, ≤, ρi is a finite poset
with minimum element ρ; V is a function mapping every α ∈ P to a subset of
atoms such that α ≤ β implies V (α) ⊆ V (β). We write α < β to mean α ≤ β
and α 6= β. The forcing relation K, α H (α forces H in K) is defined as follows:
– K, α 1 ⊥;
– for every atom a, K, α a iff a ∈ V (α);
– K, α A ∧ B iff K, α A and K, α B;
– K, α A ∨ B iff K, α A or K, α B;
– K, α A → B iff, for every β ∈ P such that α ≤ β, K, β 1 A or K, β B.
Monotonicity property holds for arbitrary formulas, i.e.: K, α A and α ≤ β
imply K, β A. A formula A is valid in K iff K, ρ A. It is well-known that
intuitionistic propositional logic Int coincides with the set of formulas valid in
all (finite) Kripke models [6].
Given a Kripke model K = hP, ≤, ρ, V i, a world α ∈ P and a sequent σ, the
relation K, α σ (K realizes σ at α) is defined as follows:
– K, α Θ; Γ =⇒ ∆; Ψ iff
K, α A for every A ∈ Θ, Γ and K, α 1 B for every B ∈ ∆, Ψ .
– K, α Θ; A Ψ iff K, α Θ; A =⇒ ·; Ψ .
– K, α Θ A; Ψ iff K, α Θ; · =⇒ A; Ψ .
A sequent σ = Θ; Γ =⇒ ∆; Ψ is realizable if there exists a model K = hP, ≤, ρ, V i
such that K, ρ σ; in this case weVsay that KWis a model of σ. We point out
that σ is realizable iff the formula (Θ, Γ ) → (∆, Ψ ) is not intuitionistically
valid. Moreover, it is easy to check that, if σ is the conclusion of one of the
axiom-rules ⊥L, ⊥ → R and Init, then σ is not realizable. A rule R is sound iff,
if the conclusion of R is realizable, then at least one of its premises is realizable.
We can esaily proof that (see the Appendix):
Proposition 2. The rules of G4ipf are sound.
By Proposition 2 the soundness of G4ipf follows (see the proof in the Appendix):
Theorem 1 (Soundness). If σ is provable in G4ipf then σ is not realizable.
74 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
3.3 Completeness
We show that, if proof search for a sequent σ fails, we can build a model K of σ,
and this proves the completeness of G4ipf . Henceforth, by unprovable we mean
‘not provable in G4ipf ’.
A left-focused sequent Θ; H Ψ is strongly unprovable iff one of the following
conditions holds:
(i) H is an AF+ and the sequent Θ; H =⇒ ·; Ψ is unprovable;
(ii) H = A → B and Θ; B Ψ is strongly unprovable.
By definition of the rules of G4ipf , we immediately get:
Lemma 3. If σ = Θ; H Ψ is strongly unprovable, then σ is unprovable.
Let σ = Θ; H Ψ be a left-focused sequent.
– σ is at-unprovable w.r.t. a → B iff, for some m ≥ 0, it holds that
H = H1 → · · · → Hm → a → B and a 6∈ Θ (if m = 0, then H = a → B);
– σ is at-unprovable if, for some a → B, σ is at-unprovable w.r.t. a → B;
– σ is →-unprovable w.r.t. (A → B) → C iff, for some m ≥ 0, it holds that
H = H1 → · · · → Hm → (A → B) → C and Θ; A, B → C =⇒ B; · is
unprovable (if m = 0, then H = (A → B) → C);
– σ is →-unprovable if, for some (A → B) → C, σ is →-unprovable w.r.t. (A →
B) → C.
Note that a sequent can match the above definitions in more than one way. For
instance, let σ = ·; a1 → (a2 → a3 ) → a4 → a5 a6 ; then:
– σ is at-unprovable w.r.t. a1 → (a2 → a3 ) → a4 → a5 and w.r.t. a4 → a5 ;
– σ is →-unprovable w.r.t. (a2 → a3 ) → a4 → a5 .
Lemma 4. Let σ = Θ; H Ψ be an unprovable sequent. Then, σ is strongly
unprovable or at-unprovable or →-unprovable.
Proof. By induction on ≺. Let us assume that, for every σ 0 ≺ σ, the lemma
holds for σ 0 ; we prove the lemma for σ by a case analysis.
– Let H be an AF+ . Since the sequent σ is unprovable then Θ; H =⇒ ·; Ψ is
unprovable. Hence by definition σ is strongly unprovable.
– Let H = a → B. If a 6∈ Θ then σ is at-unprovable w.r.t. a → B. Let a ∈ Θ
and let σ 0 = Θ; B Ψ . Then σ 0 is unprovable. Since σ 0 ≺ σ, by IH σ 0
is strongly unprovable or at-unprovable or →-unprovable. If σ 0 is strongly
unprovable, by definition σ is strongly unprovable. Let us assume that σ 0 is
at-unprovable w.r.t. a0 → C. Then B = H1 → · · · → Hm → a0 → C and
a0 6∈ Θ. This implies that σ is at-unprovable w.r.t. a0 → C. Finally, let us
assume that σ 0 is →-unprovable w.r.t. (C → D) → E. Then B = H1 →
· · · → Hm → (C → D) → E and the sequent Θ; C, D → E =⇒ D; · is
unprovable. If follows that σ is →-unprovable w.r.t. (C → D) → E.
Focusing on contraction 75
K1 Kn
....
ρ1 ρn
ρ
Fig. 2. The model Model(At, {K1 , . . . , Kn })
– Let H = (B → C) → D. If Θ; B, C → D =⇒ C; · is unprovable, then by
definition σ is →-unprovable w.r.t. (B → C) → D. Otherwise, let Θ; B, C →
D =⇒ C; · be provable. Then σ 0 = Θ; D Ψ is unprovable. Since σ 0 ≺ σ, by
IH σ 0 is strongly unprovable or at-unprovable or →-unprovable. Reasoning
as above, the lemma holds for σ. t
u
Let S = {K1 , . . . Kn } be a (possibly empty) set of models Ki = hPi , ≤i , ρi , Vi i
(1 ≤ i ≤ n), let At be a set of atoms such that, for every 1 ≤ i ≤ n, At ⊆ Vi (ρi );
without loss of generality, we can assume that the sets Pi are pairwise disjoint.
By Model(At, S) we denote the Kripke model K = hP, ≤, ρ, V i defined as follows:
1. If S is empty, then K is the Kripke model consisting of only the world ρ and
V (ρ) = At.
2. Let n ≥ 1. Then (see Fig. S2): S
- ρ is new (namely, ρ 6∈ i∈{1,...,n} Pi ) and P = {ρ} ∪ i∈{1,...,n} Pi ;
S
- ≤ = { (ρ, α) | α ∈ P } ∪ i∈{1,...,n} ≤i ;
- V (ρ) = At and, for every i ∈ {1, . . . , n} and α ∈ Pi , V (α) = Vi (α).
It is easy to check that K is a well-defined Kripke model. In Point 2, for every
1 ≤ i ≤ n, every α ∈ Pi and every formula A, it holds that K, α A iff Ki , α A.
A world β of a model K is an immediate successor of α if α < β and, for every
γ such that α ≤ γ ≤ β, either γ = α or γ = β.
Lemma 5. Let H = H1 → · · · → Hm → A → B (m ≥ 0), let K = hP, ≤, ρ, V i
be a model such that K, ρ 1 A and, for every immediate successor α of ρ, it holds
that K, α H. Then K, ρ H.
In the next lemma we show how to build a Kripke model of an unprovable
sequent.
Lemma 6. Let σ = Θ; · =⇒ ·; Ψ be an unprovable sequent such that, for ev-
ery non-atomic H ∈ Θ, the sequent Θ \ {H}; H Ψ is at-unprovable or →-
unprovable. Let At be the set of atoms of Θ and let Θ1 be the set of non-atomic
formulas H of Θ such that the sequent Θ \ {H}; H Ψ is not at-unprovable.
Let S be a (possibly empty) set of models satisfying the following conditions:
(i) For every H ∈ Θ1 , let (A → B) → C such that Θ \ {H}; H Ψ is →-
unprovable w.r.t. (A → B) → C; then S contains a model of the sequent
Θ \ {H}; A, B → C =⇒ B; ·.
76 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
(ii) For every A → B ∈ Ψ , S contains a model of the sequent Θ; A =⇒ B; ·.
(iii) Every model of S is of type (i) or (ii).
Then, Model(At, S) is a model of σ.
Proof. Let us assume that the set of models S is empty. Then Θ1 is empty and
Ψ only contains atoms not belonging to At. By definition, K = Model(At, S)
has only the world ρ. Since V (ρ) = At, we immediately get K, ρ a, for every
a ∈ At, and K, ρ 1 a0 , for every a0 ∈ Ψ . Let H be a non-atomic formula of Θ.
Since Θ1 = ∅, the sequent Θ \ {H}; H Ψ is at-unprovable. This means that
H = H1 → · · · → Hm → a → B, where a 6∈ At, hence K, ρ H. This proves
that K, ρ σ, thus K is a model of σ.
Let us assume that S contains the models K1 = hP1 , ≤1 , ρ1 , V1 i, . . . , Kn =
hPn , ≤n , ρn , Vn i (n ≥ 1) and let K = hP, ≤, ρ, V i be the model Model(At, S); we
show that K is a model of σ.
If a ∈ At, then K, ρ a by definition of V .
Let H be a non-atomic formula of Θ. If H 6∈ Θ1 , then the sequent Θ \
{H}; H Ψ is at-unprovable, namely H = H1 → · · · → Hm → a → B, where
a 6∈ At. Firstly, we note that Ki , ρi H, for every 1 ≤ i ≤ n; indeed, by (i)–
(iii), Ki is a model of a sequent of the form Θ0 ; Γ 0 =⇒ ∆0 ; · such that H ∈ Θ0 .
It follows that Ki , ρi H, for every 1 ≤ i ≤ n; hence K, ρi H. By definition
of V , we have K, ρ 1 a. By Lemma 5, we get K, ρ H.
Let H ∈ Θ1 and let Θ \ {H}; H Ψ be →-unprovable w.r.t. (A → B) → C.
This mean that H = H1 → · · · → Hm → (A → B) → C and, by (i), S contains
a model Kj of Θ \ {H}; A, B → C =⇒ B; ·. This implies that:
(P1) Kj , ρj A;
(P2) Kj , ρj B → C;
(P3) Kj , ρj 1 B.
By (P1) and (P2) it follows that Kj , ρj (A → B) → C, which implies Kj , ρj
H. Moreover, if i ∈ {1, . . . , n} and i 6= j, then by (i)– (iii) Ki is a model of a
sequent Θ0 ; Γ 0 =⇒ ∆0 ; · such that H ∈ Θ0 , hence Ki , ρi H. Thus, for every
1 ≤ i ≤ n, it holds that Ki , ρi H, which implies K, ρi H. By (P1) and (P3),
we have K, ρj A and K, ρj 1 B. Since ρ < ρj in K, we get K, ρ 1 A → B. By
Lemma 5, we conclude K, ρ H.
Let H ∈ Ψ . If H is an atom, then H 6∈ At, otherwise σ would be provable;
hence K, ρ 1 H. Let H = A → B. By (ii), S contains a model Kj of Θ; A =⇒ B; ·.
Thus, Kj , ρj A and Kj , ρj 1 B, which implies K, ρ 1 A → B. We conclude
that K is a model of σ. t
u
We can now prove the completeness of G4ipf .
Proposition 3 (Completeness). Let σ = Θ; Γ =⇒ ∆; Ψ . If σ is unprovable,
then σ is realizable.
Focusing on contraction 77
Proof. By induction on ≺. If Γ, ∆ is not empty, the proposition easily fol-
lows by the induction hypothesis. For instance, let σ = Θ; Γ, A ∨ B =⇒ ∆; Ψ .
By definition of the rule ∨L, one of the sequents σA = Θ; Γ, A =⇒ ∆; Ψ or
σB = Θ; Γ, B =⇒ ∆; Ψ is unprovable. Since σA ≺ σ and σB ≺ σ, by induction
hypothesis there exists a model K of σA or of σB . In either case K is a model of
σ, hence σ is realizable.
Let σ = Θ; · =⇒ ·; Ψ . We distinguish two cases (C1) and (C2).
(C1) There is a non-atomic formula H ∈ Θ such that σ 0 = Θ \ {H}; H Ψ is
strongly unprovable.
By Lemma 3, σ 0 is unprovable. Since σ 0 ≺ σ, by induction hypothesis there exists
a model K of σ 0 ; since K is also a model of σ, we conclude that σ is realizable.
(C2) For every non-atomic H ∈ Θ, the sequent σ 0 = Θ \ {H}; H Ψ is not
strongly unprovable.
We build a model of σ by applying Lemma 6. We point out that the hypothesis
of Lemma 6 are satisfied. Indeed, for every non-atomic H ∈ Θ, since σ 0 =
Θ \ {H}; H Ψ is not strongly unprovable, by Lemma 4 σ 0 is at-unprovable or
→-unprovable. The (possibly empty) set of models S can be defined as follows:
(a) For every H ∈ Θ1 , let us assume that Θ \ {H}; H Ψ is →-unprovable
w.r.t. (A → B) → C. Then H = H1 → · · · → Hm → (A → B) → C and the
sequent σH = Θ \ {H}; A, B → C =⇒ B; · is unprovable. Since σH ≺ σ, by
induction hypothesis there exists a model of σH .
(b) For every K = A → B ∈ Ψ , the sequent σK = Θ; A =⇒ B; · is unprovable
(otherwise σ would be provable). Since σK ≺ σ, by induction hypothesis
there exists a model of σK .
Thus, we can define S as the set of models K = hP, ≤, ρ, V i mentioned in (a) and
in (b); note that, since At ⊆ Θ, we have At ⊆ V (ρ). By Lemma 6, Model(At, S)
is a model of σ, hence σ is realizable. t
u
The above proof shows how to build a model of an unprovable sequent (see in
particular points (a) and (b)). We remark that, in the model construction, only
active sequents are relevant, while focused sequents are skipped. This justifies
why standard model construction techniques are not directly applicable and a
more involved machinery is needed.
By soundness and completeness of G4ipf , a sequent σ is provable in G4ipf
iff σ is not realizable. By definition, A ∈ Int iff the sequent ·; · =⇒ A; · is not
realizable. We conclude that A ∈ Int iff A is provable in G4ipf .
4 Conclusions and future work
We have presented a focused version of the contraction-free calculus G4ip [21].
Essentially, every treatment of focusing [14] extends the (a)synchronous clas-
sification of connectives to atoms, assigning them a bias or polarity. Different
78 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
polarizations of atoms do not affect provability, but do influence significantly
the shape of the derivation, allowing one to informally characterize forward and
backward reasoning via respectively positive and negative bias assignments. Un-
fortunately, the contraction-free approach is essentially forward and negative bias
do not work as expected. Here is why: standard presentations, where contraction
on focus is allowed, use the following rules
L Θ; P =⇒ ·; Ψ
Θ; n n, Ψ Init Θ; P Ψ Blur
L
Θ; · =⇒ ·; n Θ; B Ψ Θ, p; B Ψ
→ at− → at+
Θ; n → B Ψ Θ, p; p → B Ψ
where n is a negative atom, p is a positive atom, P an AF or a positive atom.
These rules without contraction give rise to an incomplete calculus. For instance,
let us consider the non-realizable sequent σ = n → p, (n → p) → n; · =⇒ ·; p.
The only rule applicable to σ is FocusL . If we select n → p we get:
..
.
(n → p) → n; · =⇒ ·; n (n → p) → n; p p
→ at−
(n → p) → n; n → p p
But the left premise is unprovable. On the other hand, if we choose (n → p) → n
we get:
..
.
n → p; n, p → n =⇒ p; · n → p; n p
→→ L
n → p; (n → p) → n p
But the right premise is unprovable because there is no rule that can blur a
negative atom from focus. To get a complete calculus we should allow BlurL on
negative atoms, but in this case the calculus does not properly capture “backward
chaining”.
This paper is but a beginning of our investigation of focusing:
– It is commonly believed that every “reasonable” sequent calculus has a natu-
ral focused version. We aim to test this “universality” hypothesis further by
investigating its applicability to a rather peculiar logic, Gödel-Dummett’s,
which is well-known to lead a double life as a super-intuitionistic (but not
constructive) and as a quintessential fuzzy logic [17].
– We plan to investigate counterexample search in focused systems. The natu-
ral question is: considering that focused calculi restrict the shape of deriva-
tions, what kind of counter models do they yield, upon failure? How do they
compare to calculi such as [2] or the calculus [11] designed to yield models
of minimal depth?
– There seems to be a connection between contraction-free calculi and Gab-
bay’s restart rule [12], a technique to make goal oriented provability with
diminishing resources complete for intuitionistic provability. Focusing could
be the key to understand this.
Focusing on contraction 79
References
1. J. Andreoli. Logic programming with focusing proofs in linear logic. Journal of
Logic and Computation, 2(3):297–347, 1992.
2. A. Avellone, G. Fiorino, and U. Moscato. Optimization techniques for propositional
intuitionistic logic and their implementation. TCS, 409(1):41–58, 2008.
3. A. Avron and B. Konikowska. Decomposition proof systems for Gödel-Dummett
logics. Studia Logica, 69(2):197–219, 2001.
4. D. Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput.
Log., 13(1):2, 2012.
5. D. Baelde, D. Miller, and Z. Snow. Focused inductive theorem proving. In J. Giesl
et al., editors, IJCAR, volume 6173 of LNCS, pp. 278–292. Springer, 2010.
6. A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press, 1997.
7. K. Chaudhuri. The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie
Mellon University, 2006.
8. K. Chaudhuri, F. Pfenning, and G. Price. A logical characterization of forward
and backward chaining in the inverse method. JAR, 40(2-3):133–177, 2008.
9. R. Dyckhoff and S. Lengrand. LJQ: a strongly focused calculus for intuitionistic
logic. In A. Beckmann et al., editors, Computability in Europe 2006, volume 3988,
pages 173–185. Springer, 2006.
10. R. Dyckhoff and S. Negri. Admissibility of structural rules for contraction-free
systems of intuitionistic logic. J. Symb. Log., 65(4):1499–1518, 2000.
11. M. Ferrari, C. Fiorentini, and G. Fiorino. Contraction-Free Linear Depth Sequent
Calculi for Intuitionistic Propositional Logic with the Subformula Property and
Minimal Depth Counter-Models. JAR, pages 1–21, 2012.
12. D. Gabbay and N. Olivetti. Goal-Directed Proof Theory, volume 21 of Applied
Logic Series. Kluwer Academic Publishers, August 2000.
13. A.S. Henriksen. A contraction-free focused sequent calculus for classical proposi-
tional logic. Leibnitz International Proc. in Informatics, Daghstul, April 2011.
14. C. Liang and D. Miller. Focusing and polarization in linear, intuitionistic, and
classical logics. Theor. Comput. Sci., 410(46):4747–4768, 2009.
15. S. Maehara. Eine darstellung der intuitionistischen logik in der klassischen. Nagoya
Mathematical Journal, pages 45–64, 1954.
16. S. McLaughlin and F. Pfenning. Imogen: Focusing the polarized inverse method
for intuitionistic propositional logic. In I. Cervesato et al., editors, LPAR, volume
5330 of LNCS, pages 174–181. Springer, 2008.
17. G. Metcalfe, N. Olivetti, and D. Gabbay. Proof Theory for Fuzzy Logics. Springer
Publishing Company, Incorporated, 1st edition, 2008.
18. D. Miller and E. Pimentel. A formal framework for specifying sequent calculus
proof systems. Theor. Comput. Sci., 474:98–116, 2013.
19. D. Miller and A. Saurin. From proofs to focused proofs: A modular proof of
focalization in linear logic. In J. Duparc et al., editors, CSL, volume 4646 of
LNCS, pages 405–419. Springer, 2007.
20. V. Nigam, E. Pimentel, and G. Reis. Specifying proof systems in linear logic with
subexponentials. Electr. Notes Theor. Comput. Sci., 269:109–123, 2011.
21. A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory, volume 43 of Cambridge
Tracts in Theoretical Computer Science. Cambridge University Press, 1996.
22. A. Waaler and L. Wallen. Tableaux for Intuitionistic Logics. In M. D’Agostino et
al., editors, Handbook of Tableaux Methods, pages 255–296. Kluwer, 1999.
80 Alessandro Avellone, Camillo Fiorentini and Alberto Momigliano
Appendix
Proof of Lemma 1
To prove that ≺s is a well-founded relation, we have to show that there is no
infinite descending ≺s -chain of the form
· · · ≺s σ 3 ≺s σ 2 ≺s σ 1
Note that all the sequents in the ≺s -chain have the same kind. Thus, either all
the sequents in the ≺s -chain are focused or all are active.
Let σ1 = Θ1 ; A1 Ψ1 and σ2 = Θ2 ; A2 Ψ2 be two focused sequents
such that σ1 ≺s σ2 . Then, Θ1 = Θ2 , Ψ1 = Ψ2 and wg(A1 ) < wg(A2 ), hence
wg(σ1 ) < wg(σ2 ). Since the weight of a sequent is a positive number, every
descending ≺s -chains containing focused sequents has finite length.
Let σ1 = Θ1 ; Γ1 =⇒ ∆1 ; Ψ1 and σ2 = Θ2 ; Γ2 =⇒ ∆2 ; Ψ2 be two active
sequents such that σ1 ≺s σ2 . Then, one of the following conditions holds:
1. wg(σ1 ) < wg(σ2 );
2. wg(σ1 ) = wg(σ2 ) and wg(Γ1 , ∆1 ) < wg(Γ2 , ∆2 ).
Thus, every descending ≺s -chains containing active sequents has finite length.
Proof of Proposition 1
We have to prove that ≺ is a well-founded order relation. By definition, ≺ is
transitive. We show that there exists no infinite descending ≺-chain; this also
implies that ≺ is not reflexive. Let us assume, by absurd, that there exists
an infinite ≺-chain C of sequents σi (i ≥ 1) such that σi+1 ≺ σi for every
i ≥ 1. We have wg(σi+1 ) ≤ wg(σi ) for every i ≥ 1. Since, by Lemma 1, the
relation ≺s is well-founded, C contains infinitely many occurrences of ≺d . By
Lemma 2, from C we can extract an infinite sequence of active sequents σi0 such
0
that wg(σi+1 ) < wg(σi0 ) for every i ≥ 1, a contradiction. We conclude that every
descending ≺-chain has finite length, hence ≺ well-founded.
Proof of Proposition 2
We have to prove that the rules of G4ipf are sound. All the cases except the
one for →→ L and → R rules are immediate.
Let R be the rule → R, let σ = Θ A → B; Ψ be the conclusion of R and
let K = hP, ≤, ρ, V i be a Kripke model such that K, ρ σ. Since K, ρ 1 A → B,
there exists β ∈ P such that K, β A and K, β 1 B. It follows that the submodel
of K having root β realizes the premise Θ; A =⇒ B; · of R.
Let R be the rule →→ L , let σ = Θ; (A → B) → C Ψ be the conclusion
of R and let us assume K, ρ σ. If K, ρ C, we get K, ρ Θ; C Ψ , hence
the right-most premise of R is realizable. Let us assume K, ρ 1 C. Since K, ρ
(A → B) → C, we have K, ρ 1 A → B. Then, there exists β ∈ P such that
K, β A and K, β 1 B. It follows that K, β B → C, and this implies
K, β Θ; A, B → C =⇒ B; ·; thus, the left-most premise of R is realizable.
Focusing on contraction 81
Proof of Theorem 1 (Soundness of G4ipf )
Let D be a closed derivation of σ and let us assume that σ is realizable. By
Proposition 2, one of the initial sequents σ of D is realizable. Since σ is the
conclusion of an axiom-rule, we get a contradiction.