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 particular w.r.t. termination, if not for the folk observations that only negative 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 intuitionistic 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.
Introduction and related work
Focusing [
Γ, A, A ` Δ Γ, A ` Δ
Γ ` A, A, Δ Γ ` A, Δ
point contraction is a rather worrisome rule: it can be applied at any time making 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 [
There is a further element: Gentzen’s presentation of intuitionistic logic is
obtained 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 [
Γ, A ` B Γ ` A → B, Δ → R
is not. According to the focusing diktat, → L would be classified as left asynchronous and eagerly applied, and this makes the asynchronous phase endless.
used, we exploit a well-known formulation of a contraction-free calculus, known
as G4ip [
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
satisfactory for our purposes:
1. The permutation-based approach, dating back to Andreoli [
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
focused 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 [
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 [
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 [
The proof system
atoms, the constant ⊥ and the connectives ∧, ∨ and →; ¬A stands for A → ⊥.
G4ip of Vorob’ev, Hudelmeier and Dyckhoff [
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
– Θ; Γ =⇒ Δ; Ψ . Active sequent; – Θ; A Ψ . Left-focused sequent; – Θ A; Ψ . Right-focused sequent. Γ and Δ denote multisets of formulas, while Θ and Ψ denote multisets of SF.
formulas are considered, and a synchronous phase, where synchronous ones are.
chronous phase we eagerly apply the asynchronous rules to active sequents
Θ; Γ =⇒ Δ; Ψ . If the main formula is an AF, the formula is decomposed;
otherwise, 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).
Differently 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 [
⊥L Θ; Γ, A, B =⇒ Δ; Ψ Θ; Γ, A ∧ B =⇒ Δ; Ψ ∧L
Θ; Γ =⇒ Δ; Ψ Θ; Γ, ⊥ → B =⇒ Δ; Ψ
⊥ → L Θ; Γ, A → B → C =⇒ Δ; Ψ Θ; Γ, (A ∧ B) → C =⇒ Δ; Ψ Θ; Γ, A → C, B → C =⇒ Δ; Ψ Θ; Γ, (A ∨ B) → C =⇒ Δ; Ψ ∧ → L
∨ → L Θ; Γ, A =⇒ Δ; Ψ Θ; Γ, B =⇒ Δ; Ψ Θ; Γ, A ∨ B =⇒ Δ; Ψ ∨L Θ; Γ =⇒ A, B, Δ; Ψ Θ; Γ =⇒ A ∨ B, Δ; Ψ ∨R
Θ; Γ =⇒ Δ; Ψ Θ; Γ =⇒ ⊥, Δ; Ψ
⊥R Θ; Γ =⇒ A, Δ; Ψ Θ; Γ =⇒ B, Δ; Ψ Θ; Γ =⇒ A ∧ B, Δ; Ψ
∧R Θ; Γ =⇒ ⊥ → B, Δ; Ψ Θ; Γ =⇒ A → B → C, Δ; Ψ Θ; Γ =⇒ (A ∧ B) → C, Δ; Ψ ⊥ → R
∧ → R Θ; Γ =⇒ A → C, Δ; Ψ Θ; Γ =⇒ B → C, Δ; Ψ Θ; Γ =⇒ (A ∨ B) → C, Δ; Ψ ∨ → R
Θ,ΘS;−S; −·=⇒Ψ·; Ψ FocusL Θ; Θ·=⇒S·;; SΨ, Ψ FocusR ΘΘ;T; T=⇒ ·Ψ; Ψ BlurL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Θ, a
a; Ψ Θ, a; B Θ, a; a → B
Init Ψ Ψ Θ Θ; K =⇒ B; ·
K → B; Ψ
→ R → at Θ; A, B → C =⇒ B; · Θ; (A → B) → C Θ; 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.
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. 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
→ at
FocusL [⊥R, ⊥ → L, ActL] ¬a; ¬¬a · ¬a, ¬¬a; · =⇒ ·; · ·; ¬(a ∨ ¬a) =⇒ ⊥ · ; · ¬¬(a ∨ ¬a); · ·; · =⇒ ·; ¬¬(a ∨ ¬a) ·; · =⇒ ¬¬(a ∨ ¬a); ·
→ R
¬a; ⊥ =⇒ ·; · ⊥L
¬a; ⊥ · →→ L [⊥R, ∨ → L, ActL × 2]
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
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
3.1
Termination
wg(a) = wg(⊥) = 2 wg(A ∨ B) = 1 + wg(A) + wg(B) wg(A ∧ B) = wg(A) + wg(A) · wg(B) wg(A → B) = 1 + wg(A) · wg(B)
– 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).
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
have rules where the conclusion and the premise have the same weight (Focus,
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, Ψ )
wg(σ1) = wg(σ2).
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).
σa = Θ; H1 =⇒ ·; Ψ, σ1 = Θ; H1 σb = Θ, Hn; · =⇒ ·; Ψ Ψ, . . . σn = Θ; Hn Ψ
tu
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.
let D be a (possibly open) derivation of σ1 and let σ1, σ2, . . . be a branch of D.
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.
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 [
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, α
K, α – K, α – K, α Θ; Γ =⇒ Δ; Ψ iff
Θ; A Ψ iff K, α Θ; A =⇒ ·; Ψ .
Θ A; Ψ iff K, α Θ; · =⇒ A; Ψ .
A sequent σ = Θ; Γ =⇒ Δ; Ψ is realizable if there exists a model K = hP, ≤, ρ, V i such that K, ρ σ; in this case we say that K is a model of σ. We point out that σ is realizable iff the formula V(Θ, Γ ) → W(Δ, Ψ ) 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.
Proposition 2. The rules of G4ipf are sound.
Theorem 1 (Soundness). If σ is provable in G4ipf then σ is not realizable. 3.3
Completeness
and this proves the completeness of G4ipf . Henceforth, by unprovable we mean ‘not provable in G4ipf ’.
(i) H is an AF+ and the sequent Θ; H =⇒ ·; Ψ is unprovable; (ii) H = A → B and Θ; B Ψ is strongly unprovable.
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.
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.
K1 ρ1 ....
ρ
Kn
ρn
Let S = {K1, . . . Kn} be a (possibly empty) set of models Ki = hPi, ≤i, ρi, Vii (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:
V (ρ) = At. 2. Let n ≥ 1. Then (see Fig. 2): - ρ is new (namely, ρ 6∈ Si∈{1,...,n} Pi) and P = {ρ} ∪ Si∈{1,...,n} Pi; - ≤ = { (ρ, α) | α ∈ P } ∪ Si∈{1,...,n} ≤i; - V (ρ) = At and, for every i ∈ {1, . . . , n} and α ∈ Pi, V (α) = Vi(α).
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.
Lemma 6. Let σ = Θ; · =⇒ ·; Ψ be an unprovable sequent such that, for every 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; ·. (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 σ.
Ψ 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, V1i, . . . , Kn = hPn, ≤n, ρn, Vni (n ≥ 1) and let K = hP, ≤, ρ, V i be the model Model(At, S); we show that K is a model of σ.
{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.
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.
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
we have K, ρj A and K, ρj 1 B. Since ρ < ρj in K, we get K, ρ 1 A → B. By
hence K, ρ 1 H. Let H = A → B. By (ii), S contains a model Kj of Θ; A =⇒ B; ·.
Proposition 3 (Completeness). Let σ = Θ; Γ =⇒ Δ; Ψ . If σ is unprovable, then σ is realizable.
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 strongly unprovable. Ψ is
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 strongly unprovable. Ψ is not 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. tu
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.
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
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. Unfortunately, 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 Θ; n
n, Ψ Θ; · =⇒ ·; n Θ; n → B Θ; B
Ψ InitL Ψ → at− Θ; P =⇒ ·; Ψ Θ; P Ψ Θ, p; B Θ, p; p → B
Ψ Ψ → at+ where n is a negative atom, p is a positive atom, P an AF or a positive atom.
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 (n → p) → n; n → p p p → at− 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
n → p; (n → p) → n p →→ L
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
natural focused version. We aim to test this “universality” hypothesis further by
investigating its applicability to a rather peculiar logic, G¨odel-Dummett’s,
which is well-known to lead a double life as a super-intuitionistic (but not
constructive) and as a quintessential fuzzy logic [
· · · ≺s σ3 ≺s σ2 ≺s σ1
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).
Proof of Proposition 1
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
Proof of Proposition 2
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
Proof of Theorem 1 (Soundness of G4ipf )
conclusion of an axiom-rule, we get a contradiction.