We present a proof search procedure for the minimal coreflection logic iCK4, an intuitionistic modal logic with the normality axiom and the coreflection principle. The procedure is based on a sequent calculus Gbu-iCK4 that ensures strong termination of backward proof search. Gbu-iCK4 is shown to be complete via a dual refutation calculus that enables the extraction of countermodels when the proof search fails. To support practical experimentation, we provide an implementation of the proof search and the countermodel extraction procedures.
tree is either a subformula of the root sequent or a subformula of the sequent obtained by removing all occurrences of the □ modality from the root sequent.
Regarding the comparison with existing literature, to the best of our knowledge, the only available calculus for iCK4 is the natural deduction system introduced in [2], which is not designed to support proof search efectively.
To complement our theoretical results with an applied contribution, we have implemented both the proof search procedure and the countermodel extraction in the Java framework JTabWB [9]; the implementation is available online at [10].
Formulas, denoted by lowercase Greek letters, are built from an enumerable set of propositional variables , the constant ⊥ and the connectives ∨, ∧, → and □ ; ¬ is an abbreviation for → ⊥ and ↔ an abbreviation for ( → ) ∧ ( → ). We denote multisets (and sets) of formulas by uppercase Greek letters. Let be a formula and Γ a multiset of formulas; by □ Γ we denote the multiset {□ | ∈ Γ}. By − , we denote the formula obtained from by erasing every occurrence of □ ; Γ− is the multiset { − | ∈ Γ}. We write Sf( ) to denote the set of the subformulas of , including itself; Sf(Γ) is the union of the sets Sf( ), for every in Γ. The size of , denoted by | |, is the number of symbols in ; the size of Γ, denoted by |Γ|, is the sum of the sizes of formulas in Γ, taking into account their multiplicity.
We introduce the semantics of logic iCK4; to simplify the presentation, we assume that iCK4 enjoys the finite model property (for a more general discussion see e.g. [ 11]). A (bi-relational) strong frame ℱ is a tuple ⟨, ≤ , , ⟩, where is a finite non-empty set (worlds), ≤ (the intuitionistic relation) is a partial order with minimum element (the root of ℱ ), ⊆ × is the modal relation satisfying the following properties: (normality) if 0 ≤ 1 and 12, then 02; (strongness1) ⊆≤ . Note that these two properties imply the transitivity of .
A (bi-relational) strong model is a tuple ⟨, ≤ , , , ⟩ where ⟨, ≤ , , ⟩ is a bi-relational strong frame, and (the valuation function) is a map associating a subset of to every ∈ and satisfying the persistence property: 0 ≤ 1 implies (0) ⊆ (1).
Given a strong model , the forcing relation ⊩ between worlds of and formulas is defined as follows: , ⊩ if ∈ (), ∀ ∈ , ⊮ ⊥ , ⊩ ∧ if , ⊩ and , ⊩ , ⊩ ∨ if , ⊩ or , ⊩ , ⊩ → if ∀′ ≥ , if , ′ ⊩ then , ′ ⊩ , ⊩ □ if ∀′ ∈ , if ′ then , ′ ⊩ .
Hereafter, we write ⊩ instead of , ⊩ when the model at hand is clear from the context. It is easy to prove, by induction on the structure of a formula, that the forcing relation is persistent w.r.t. ≤ (hence, w.r.t. , since ⊆≤ ); formally: Lemma 1 (Strong monotonicity lemma) Let = ⟨, ≤ , , , ⟩ be a strong model. For every formula , if ⊩ and ≤ ′, then ′ ⊩ A world is reflexive if holds; in a strong model the following holds: Lemma 2 Let = ⟨, ≤ , , , ⟩ be a strong model and let ∈ .
(i) If is a reflexive world then, for every formula , ⊩ ↔ − . (ii) If ⊮ □ , then there exists ⋆ ∈ such that ⋆, ⋆ ⊮ and either (a) ∀′ ∈ : ⋆′, ′ ⊩ or (b) ⋆ is reflexive. 1Also called coreflection.
5 : ⊩ □ ⊮ □
→ ⊮ = (□ (□ → ) → □ ) ∨ (□ → ((□ → □ ) ∨ □ )) ≤
′ if = ′ or there is a path from to ′ ′ if there is a path from to ′ ending with → every 0 ≤ ≤ . We proceed as follows: • We set 0 = (thus, 0).
Proof.
Point (i). Note that ⊩ subformula □ strongness of , ⊩ □ with , we get , ⊩
↔ − . → by reflexivity of . Since − is obtained from by replacing every ↔ □ , for every formula . Indeed, ⊩ → □ follows by Point (ii). Since ⊮ □ , there exists
∈ such that and ⊮ . We build a finite sequence of pairwise distinct worlds 0, . . . , of such that 01 . . . and ⊮ for world of . • Suppose that the last defined world of is ( ≥ 0). If there exists ′ such that ′ ̸∈ {0, . . . , } and ′ and ′ ⊮ , we set +1 = ′; otherwise, the construction of halts and is the last Since the worlds in are pairwise distinct and is finite, the construction of eventually halts. Let ⋆ be the last element of . We have ⋆ ⊮ and 01 . . . ⋆ hence, by transitivity of , ⋆. If ⋆ is reflexive, then ⋆ matches (b). Let us assume that ⋆ is not reflexive; we show that (a) holds. Let us assume, by contradiction, that there exists ′ such that ⋆′ and ′ ⊮ . Note that ′ ̸∈ , otherwise, by transitivity of , we would get ⋆⋆, against the hypothesis that ⋆ is not reflexive. This proves that, for every ′ such that ⋆′, ′ ⊩ ; accordingly, ⋆ matches (a). Since ′ ̸∈ and ′ ⊮ , we can extend by adding ′, a contradiction (⋆ is the last element of ). □ Let Γ be a multiset of formulas. By ⊩ Γ we mean that ⊩ for every in Γ. The iCK4-consequence relation ⊨ iCK4 is defined as follows: Γ ⊨ iCK4 if
∀ ∀ (︀ , ⊩ Γ ⇒ , ⊩ )︀ . a strong model such that ⊮ , with the root of ; we call a countermodel for . The logic iCK4 is defined as the set of formulas such that ∅ ⊨ iCK4 . Hence, if ̸∈ iCK4, there exist Example 3 Fig. 6 displays a countermodel for the formula = □ (□ → ) → □ ) ∨ (□ → ((□ → □ ) ∨ □ )) is the disjunction between the Gödel-Löb the axiom □ (□ → ) → □ , characterizing logic iSL, and an instance of axiom □ → (( → ) ∨ ) (with = □ and = □ ) characterizing the Modalized Γ, Δ ⇒u Γ, □ Δ ⇒u □
Γ ⇒ Γ ⇒ → u□
Ax◁
if Γ ◁ Γ ⇒ , ,
Heyting calculus mHC. iSL and mHC are proper extensions of iCK4 and their proper axioms are not valid in iCK4. The worlds of are 0 (the root), 2, 3, 5, 8, 10, 11, 13. The relations ≤ and can be inferred by the displayed arrows, as accounted for in the figure. E.g., 0 ≤ 10, since there is a path from 0 and 10 (actually, a unique path); 0 ≤ 11 and 011, since the path from 0 and 11 ends with the solid arrow →. However, it is not the case that 010, since the path from 0 to 10 ends with the dashed arrow ‧‧➡. The only reflexive worlds are 5 and 13. In each world , the ifrst line displays the value of (); for instance, (0) = ∅, (11) = {}. The remaining lines report (separated by commas) some of the formulas forced and not forced in . Since 0 ⊮ , is a countermodel for . ♢
In this section, we introduce the Gbu-iCK4 calculus (Gentzen calculus for iCK4 with b, u-labelled sequents), which we will simply refer to as from now on. The calculus acts on labelled sequents of the form Γ ⇒ , with ∈ {b, u} where Γ is a multiset of formulas and is a formula; Γ and are referred to as the lhs (lhs( )) and the rhs (rhs( )) (left/right hand side) of respectively. We call -sequent a sequent with label . Let = Γ ⇒ ; with − we denote the sequent Γ− ⇒ − , Sf( ) = Sf(Γ ∪ { }) (the set of subformulas of ) and Sf+( ) = Sf( ) ∪ Sf( − ) (the set of extended subformulas of ). To define the calculus, we introduce the following evaluation relation: Definition 4 (Evaluation) Let Γ be a multiset of formulas and a formula. Γ evaluates , written Γ ◁ , if matches the following BNF: := | ∧ | ∨ | ∨ | → | □ with ∈ Γ and any formula.
By Γ ◁ Δ we mean that Γ ◁ , for every ∈ Δ. We state some properties of the evaluation relation which are proved in [6].
Lemma 5 (i) If Γ ◁ and Γ ⊆ Γ′, then Γ′ ◁ . (ii) If Γ ∪ Δ ◁ and Γ′ ◁ Δ, then Γ ∪ Γ′ ◁ . (iii) If Γ ◁ , then Γ ∩ Sf( ) ◁ . (iv) If Γ ◁ and , ⊩ Γ, then , ⊩ .
□ , ¬□ , ⇒ □ (
Ax◁ = □ ¬□ ¬ 6 = ⊥, □ , ⇒ 9 = ⊥, ¬ ⇒ 10 = ⊥, ⇒ ⊥ 6 ⊥
→
¬□ , ⇒ □ (
¬, ¬¬ ⇒ (
Ax◁ 9 ⊥ → 10 ⊥ →
The rules of the calculus are displayed in Fig. 2. They consist of the axiom rules Ax◁ and ⊥, together with left/right rules for each logical connective and right rules for □ . For calculi and derivations we use the definitions and notations of [ 12]. Applications of rules are depicted as trees with sequents as nodes, we call them -trees; a -derivation is a tree where every leaf is an axiom sequent, i.e., a sequent obtained by applying a zero-premise rule of . A sequent is provable in , and we write ⊢ , if there exists a -derivation with root sequent .
The calculus is oriented to backward proof search, where rules are applied bottom-up. If the conclusion of a rule has label b, the (bottom-up) application of left rules is blocked. There are two rules for right implication, namely →◁ and →⋫; the choice between them is settled by the evaluation relation ◁. Right □ -formulas are handled by rules u□ and b□ ; here the choice is determined by the label of the conclusion. We remark that if = Γ, □ Δ ⇒b □ and Γ ∪ □ Δ ◁ □ , then is an axiom sequent (see rule Ax◁) and an application of rule b□ to is prevented by the side condition of b□ . In backward proof search, a b-sequent starts the construction of a branch only containing b-sequents, where only right rules are applied. This phase ends either when an axiom sequent is obtained or when no rule can be applied or when one of the rules turning a label b into u is applied (namely, rules ⋫ and b□ ). →
Inspecting the rules of the calculus, one can easily check that every rule, except b□ , meets the subformula property, i.e., every formula occurring in the premises is a subformula of a formula occurring in the conclusion. This does not hold for b□ since the formulas in the rightmost premise Γ− , Δ− u − might not belong to Sf(Γ, □ Δ ⇒b □ ). However, every formula in Γ− , Δ− u − be⇒ ⇒ longs to Sf+(Γ, □ Δ ⇒b □ ). Accordingly, the calculus meets a weaker form of the subformula property, we call extended subformula property, namely: every formula occurring in a -tree having as root belongs to Sf+( ).
Example 6 In Fig.3 we show a -derivation of the u-sequent 0 = ⇒u ¬(¬□ ∧ ), where = □ ¬□ ¬ (we recall that ¬ is an abbreviation for → ⊥). In sequents are marked with an index () and, hereafter, are referred to as . highlights some of the peculiarities of . In backward proof search, 3 is obtained by a (backward) application of rule → to 2; the label b in 2 is crucial to block the application of rule →, which would generate an infinite branch. In sequent 4 (the left premise of rule b□ with conclusion 3) the key feature is the presence of the formula □ (also called diagonal formula); without it, the sequent 4 would be ¬□ , ⇒u and, after the application of → (the only applicable rule), the left premise would be 5 = ¬□ , ⇒b □ , which yields a loop ( 5 = 3). We stress that the sequent 7, corresponding to the right premise of b□ , is a pure intuitionistic sequent, since it is obtained from 3 by removing all the boxes. ♢
The following theorem states the main properties of : Theorem 7 (i) enjoys the extended subformula property. (ii) is terminating. (iii) ⊢ Γ ⇒ implies Γ |=iCK4 (Soundness).
(iv) Γ |=iCK4 implies ⊢ Γ ⇒u (Completeness).
We remark that in soundness is any label; instead, in completeness the label is set to u. For instance, since ∨ ⊨ iCK4 ∨ , completeness guarantees that the u-sequent u = ∨ ⇒u ∨ is provable in . A -derivation of u is obtained by first (upwards) applying rule ∨ to u and then one of the rules ∨0 or ∨1; if we first apply a right rule, we are stuck (e.g., if we apply ∨0 to u, we get the unprovable sequent ∨ ⇒u ). On the contrary, the b-sequent ∨ ⇒b ∨ is not provable in , since the label b inhibits the application of rule ∨ and forces the application of a right rule.
The soundness of the calculus can be proved by showing that its rules preserve the iCK4-consequence relation ⊨ iCK4, namely: Lemma 8 Let be an application of rule of having conclusion Γ ⇒ and premises Γ1 ⇒1 1,. . . , Γ ⇒ ( ∈ {1, 2}). If Γ ⊨ iCK4 for every ∈ {1, . . . , }, then Γ ⊨ iCK4 .
Proof. We only treat the cases of rule b□ , the other cases being straightforward. Let us suppose that Γ, □ Δ ⊭ iCK4 □ ; we show that either □ , Γ, Δ ⊭ iCK4 or Γ− , Δ− ⊭ iCK4 − . Since Γ, □ Δ ⊭ iCK4 □ , there exists a model and a world of s.t. ⊩ Γ, □ Δ and ⊮ □ . By Lemma 2(ii) there exists ⋆ such that ⋆, ⋆ ⊮ and one of the conditions (a) or (b) holds. Note that ⋆ ⊩ Δ and, since ≤ ⋆, ⋆ ⊩ Γ. Let us assume that (a) holds; then, ⋆ ⊩ □ and ⋆ ⊮ , hence □ , Γ, Δ ⊭ iCK4 . Let us assume that (b) holds. Then, ⋆ is reflexive hence, by Lemma 2(i), we get ⋆ ⊩ Γ− , Δ− and ⋆ ⊮ − ; we conclude Γ− , Δ− ⊭ iCK4 − . □ To prove the termination of we need to introduce a proper well-founded relation ≺ bu on labelled sequents. The main problem stems from rule →. Let and ′ be the conclusion and the left premise of an application of rule →; we stipulate that ′ ≺ bu since ′ has label b and has label u; thus, we establish that b weighs less than u. Now, we need a way out to accommodate the rules ⋫ and → b□ that, read bottom-up, switch b with u. We observe that the lhs of the left premise evaluates a new formula; e.g., in the application of rule →⋫ having premise , Γ ⇒u and conclusion Γ ⇒ → , it holds that Γ ⋫ (side condition) and Γ ∪ { } ◁ (definition of ◁); this suggests that here we can exploit the evaluation relation.
Let Ev be defined as follows:
Ev(Γ ⇒ ) = { | ∈ Sf(Γ ∪ { }) and Γ ◁ } Note that Ev( ) ⊆ Sf( ). We also have to take into account the size of a sequents, where |Γ ⇒ | = |Γ| + | |.
Finally, we observe that the conclusion of rule b□ is a modal sequent (it contains at least one □ ), while the right premise is intuitionistic (no □ ). To convey this property in the denfiition of ≺ bu, we introduce the following function: isModal( ) = {︃1 if contains at least one □
0 otherwise We write ′ ≺ bu if one of the following conditions holds: (a) isModal( ′) < isModal( ); (b) isModal( ′) = isModal( ) and Sf( ′) ⊂ Sf( ); (c) isModal( ′) = isModal( ) and Sf( ′) = Sf( ) and Ev( ′) ⊃ Ev( ); (d) isModal( ′) = isModal( ) and Sf( ′) = Sf( ) and Ev( ′) = Ev( ) and label( ′) = b and label( ) = u; (e) isModal( ′) = isModal( ) and Sf( ′) = Sf( ) and Ev( ′) = Ev( ) and label( ′) = label( ) and | ′| < | |.
Proposition 9 The relation ≺ bu is well-founded.
Proof. Assume, by contradiction, that there is an infinite descending chain . . . ≺ bu 1 ≺ bu 0. There is ≥ 0 such that isModal( ) stabilizes, namely: isModal( ) = isModal( ) for every ≥ . We have Sf( ) ⊇ Sf( +1) ⊇ . . . ; since Sf( ) is finite, the sets Sf( ) eventually stabilize, namely: there is ≥ such that Sf( ) = Sf( ) for every ≥ . Since Ev( ) ⊆ Sf( ), we get Ev( ) ⊆ Ev( +1) ⊆ . . . ⊆ Sf( ). Since Sf( ) is finite, there is ≥ such that Ev( ) = Ev( ) for every ≥ . This implies that there exists ≥ such that all the sequents , +1, . . . have the same label; accordingly | | > | +1| > | +2| > . . . ≥ 0, a contradiction. We conclude that ≺ bu is well-founded. □ To prove that the rules of are decreasing w.r.t.≺ bu, we need the following: Lemma 10 Let be an application of a rule of , let be the conclusion of and ′ any of the premises of . For every formula , if lhs( ) ◁ and ′ is not the right premise of b□ , then lhs( ′) ◁ . Proof. The assertion can be proved by applying Lemma 5. For instance, let = Γ, □ Δ ⇒u □ and ′ = Γ, Δ ⇒u be the conclusion and the premise of rule u□ ; assume that Γ ∪ □ Δ ◁ . Since Δ ◁ □ Δ, by Lemma 5(ii) get Γ ∪ Δ ◁ . □ Proposition 11 Every rule of the calculus is decreasing w.r.t. ≺ bu.
Proof. Let and ′ be the conclusion and one of the premises of an application of a rule of . Note that isModal( ′) ≤ isModal( ). If ′ is not the right premise of b□ , it holds that Sf( ′) ⊆ Sf( ); moreover, if Sf( ′) = Sf( ), by Lemma 10 we get Ev( ′) ⊇ Ev( ). We can prove ′ ≺ bu by a case analysis; we only detail two significant cases.
′ = → , Γ ⇒b , = → , Γ ⇒u → If isModal( ′) < isModal( ), then ′ ≺ bu by point (a) of the definition; otherwise we have isModal( ′) = isModal( ). If Sf( ′) ⊂ Sf( ), then ′ ≺ bu by point (b) of the definition; otherwise, as discussed above, it holds that Sf( ′) = Sf( ) and Ev( ′) ⊇ Ev( ). If Ev( ′) ⊃ Ev( ), then ′ ≺ bu by point (c); otherwise, ′ ≺ bu follows by point (d).
′ = □ , Γ, Δ ⇒u
′′ = Γ− , Δ− ⇒u − = Γ, □ Δ ⇒ □ b□ Γ ∪ □ Δ ⋫ □ Note that isModal( ′) = isModal( ) = 1. If Sf( ′) ⊂ Sf( ), then ′ ≺ bu by point (b). Otherwise, Sf( ′) = Sf( ) and Ev( ′) ⊇ Ev( ). Note that □ ∈ Ev( ′) and, by the side condition, □ ̸∈ Ev( ). This implies that Ev( ′) ⊃ Ev( ), hence ′ ≺ bu by point (c). As for the right premise, we have isModal( ′′) = 0 and isModal( ) = 1, thus ′′ ≺ bu by point (a). □ By Prop. 9 and 11, we conclude that the calculus is terminating.
A common technique to prove the completeness of a sequent calculus consists in showing that, whenever a sequent is not provable in the calculus, then a countermodel for can be built; we prove the completeness of according with this plan. Following the ideas in [13, 7, 8, 14], we formalize the notion of “non-provability in ” by introducing the refutation calculus Rbu-iCK4, a dual calculus to = Gbu-iCK4. Hereafter, we will refer to Rbu-iCK4 simply as ℛ. Sequents of ℛ, called antisequents, have the form Γ ⇏ . Intuitively, a derivation in ℛ of Γ ⇏ witnesses that the sequent Γ ⇒ is refutable, that is, not provable, in . Henceforth, Γat denotes a finite multiset of propositional variables, Γ→ denotes a finite multiset of →-formulas (i.e., formulas of the kind → ). The axioms of ℛ are the irreducible antisequents, namely the antisequents Γ ⇏ such that the corresponding dual sequents Γat is a multiset of propositional variables, Γ→ is a multiset of →-formulas Irr , Γ ⇏u 0 ∨ 1, Γ ⇏u
Γ ⇏ Γ ⇏ → □ , Γ, Δ ⇏u →◁
Γ ◁ b□ Γ ⋫ □ , , Γ ⇏u ∧ , Γ ⇏u Γ ⇏b
Γ ⇏b Γ ⇏b ∨ , Γ ⇏u Γ ⇏ → ∧
∨ →⋫ Γ ⋫ { Γ ⇏b } → ∈Γ→ Γat, Γ→, □ Δ ⇏u ⏟ Γ⏞
Γ ⇏ Γ ⇏ 0 ∧ 1
, Γ ⇏u → , Γ ⇏u ∧
→
Ref Γ ⋫ □ Γ− ⇏u − Γ ⇏b □ SAt Γ→ ̸= ∅ u ∈ ( ∪ {⊥}) ∖ Γat { Γ ⇏b } → ∈Γ→ Γ ⇏b 0 Γ ⇏b 1 Γat, Γ→, □ Δ ⇏u 0 ∨ 1 ⏟ Γ⏞ Γ ⇒ are not the conclusion of any of the rules of . Irreducible antisequents are characterized as follows:
An antisequent is irreducible if = Γat, Γ→, □ Δ ⇏ and both The rules of ℛ are displayed in Fig. 4. In rules SuAt, Su∨ and S□u (we call Succ rules) the notation {Γ ⇏b } → ∈Γ→ means that, for every → ∈ Γ→, the b-antisequent Γ ⇏b is a premise of the rule. Note that all of the Succ rules have at least one premise (in rule SuAt this is imposed by the condition Γ→ ̸= ∅). ℛ-trees and ℛ-derivations are defined analogously to the case of the sequent calculus . The next theorem, proved below, states the soundness of ℛ: Theorem 13 (Soundness of ℛ) If ⊢ℛ Γ ⇏u , then Γ ̸|=iCK4 .
Example 14 In Fig. 5 we show an ℛ-derivation of 0 = ⇏u where is the same formula considered in Ex. 3. By Th. 13, we get ̸|=iCK4 , namely ̸∈ iCK4. ♢ Countermodel extraction. A strong model with root is a model for = Γ ⇏u (a countermodel for = Γ ⇒u , respectively) if ⊩ Γ and ⊮ ; thus certifies that Γ ̸|=iCK4 . Let be an ℛ-derivation of a u-antisequent 0u; we show that from we can extract a model Mod() for 0u. A u-antisequent of is prime if is the conclusion of rule Irr or of a Succ rule. We introduce the relations ⪯ and ≺ between antisequents occurring in : • 1 ≺ 2 if 1 and 2 belong to the same branch of and 1 is below 2; • 1 ⪯ 2 if either 1 = 2 or 1 ≺ 2.
Let be the set of prime antisequents occurring in . We introduce a map Ψ between the u-antisequents of and . • Ψ( u) = u if u is the ⪯ -minimum prime antisequent such that u ⪯ .
Irr
→ ⇏ (
Ref
□ → ⇏ □ (
→⋫
⇏ (□ (□ → ) → □ ) ∨ (□
□
□
, □ ⇏ □ (
Irr
Ref
We define Mod() as the structure ⟨, ≤ , , u , ⟩ where: • is the set of the prime antisequents of ; • ≤ is the restriction of ⪯ to ; • is the transitive closure of + ∪ * ; • u is the ≤ -minimum prime antisequent of ; • ( Γ ⇏u ) = Γ ∩ .
It is easy to check that Mod() is a strong model; in particular, u exists since the antisequent at the root of has label u. The map Ψ defined above is referred to as the canonical map Ψ between the u-antisequents of and Mod().
We state the main properties of Mod().
Theorem 15 Let be an ℛ-derivation of a u-antisequent 0u.
(i) For every u-antisequent u = Γ ⇏u in , Ψ( u) ⊩ Γ and Ψ( u) ⊮ .
(ii) Mod() is a model for 0u.
Point (ii) follows from (i) and the fact that Ψ( 0u) is the root of Mod(). The proof of (i) is deferred below. Note that point (ii) of Th. 15 immediately implies the soundness of ℛ (Th. 13). Example 16 In Fig. 6 we represent the structure of the ℛ-derivation in Fig. 5, displaying the information relevant to the definition of Mod(). The model Mod() for 0 coincides with the strong model in Fig. 1 (described in Ex. 3), where is an alias for . Fig. 6 also reports the canonical map Ψ and the relations ≪ , ≪ and ≪ * defined below. ♢ Proof search. We investigate more deeply the duality between and ℛ. A sequent = Γ ⇒ is regular if = u or Γ = Γat, Γ→, □ Δ; by we denote the antisequent Γ ⇏ . Let be a regular sequent; in the next proposition we show that either is provable in or is provable in ℛ. The proof conveys a proof search strategy to build the proper derivation, based on backward application of the rules of . We give priority to the invertible rules of , namely: ∧, ∧, ∨, →◁, →⋫, b□ ; as
SAt
→ ⇏ (
4∙ RSeAft
□ → ⇏ (
1∙ →⋫ ⇏ (□ (□ → ) → □ ) ∨ (□ □
Irr →⋫ discussed in the proof of Prop. 17, the application of such rules does not require backtracking. If the search for a -derivation of fails, we get an ℛ-derivation of .
Proposition 17 Let be a regular sequent. One can build either a -derivation of or an ℛ-derivation of .
Proof. Since ≺ bu is well-founded (Prop. 9), we can inductively assume that the assertion holds for every regular sequent ′ such that ′ ≺ bu (IH). If or is an axiom (in the respective calculus), the assertion immediately follows. If an invertible rule of is (backward) applicable to , we can build the proper derivation by applying or its dual image in ℛ. For instance, let us assume that rule b□ of is applicable with conclusion = Γ, □ Δ ⇒b □ and premises 0 = □ , Γ, Δ ⇒u and 1 = Γ− , Δ− u − . Let ∈ {0, 1}; since ≺ bu (see Prop. 11), by (IH) there exists either a ⇒ -derivation of or an ℛ-derivation ℰ of . According to the case, we can build one of the following derivations:
0 □ , Γ, Δ ⇒u
1 Γ− , Δ− ⇒u − b□
ℰ0 □ , Γ, Δ ⇏u b□
ℰ1 Γ− , Δ− ⇏u − Let us assume that no invertible rule can be applied to ; then: • = Γ ⇒u with Γ = Γat, Γ→, □ Δ and ∈ ∪ { ⊥, 0 ∨ 1, □ 0 }.
We only discuss the case = □ 0. Let 0 = Γat, Γ→, Δ ⇒u 0 be the premise of the application of rule u□ of to ; for every → ∈ Γ→, let = Γ ⇒b and = Γ ∖ { → }, ⇒u be the two premises of an application of rule → of to with main formula → . By the (IH): • we can build either a -derivation 0 of 0 or an ℛ-derivation ℰ0 of 0. • for every → ∈ Γ→ and for every ∈ {,
ℛ-derivation ℰ of .
One of the following four cases holds: (A) We get 0. (B) There is (C) There is → ∈ Γ→ such that we get both and .
→ ∈ Γ→ such that we get ℰ . (D) We get ℰ0 and, for every → ∈ Γ→, ℰ .
}, we can build either a -derivation of or an According to the case, we can build one of the following derivations:
0 ℰ0 In the proof search strategy, this corresponds to a backtrack point, since we cannot predict which case holds. by Prop. 17, is provable in ; this proves the Completeness of (Th. 7(iv)).
Let us assume Γ ⊨ iCK4 and let = Γ ⇒u . By Soundness of ℛ (Th. 13) is not provable in ℛ, hence,
. It remains to prove point (i) of Th. 15. By Sf− ( ) we denote the set Sf( ) ∖ { }; < ′ means that ≤ ′ and ̸= ′. below; at the same time, we define the relations ≪ , ≪ and ≪ * between u-antisequents in .
Let be an ℛ-derivation having a Succ rule at the root. To display , we introduce the schema (
· · · b = Γat, Γ→, □ Δ ⇏b · · ·
u = Γat, Γ→, Δ ⇏u u = Γat, Γ→, □ Δ ⇏u
Succ • b is any of the premises of Succ having label b. • u is only defined if Succ is S□u (thus = □ ); in this case we set u ≪ u . • The ℛ-derivation of b has the form . . . 11ub 1 · · · . . . u b
b b = Γ ⇏b 1b Irr . . .
b Irr + ≥ 0
b only contains b-antisequents Γ = Γat, Γ→, □ Δ - The ℛ-tree b has root b and leaves 1b, . . . , b, 1b, . . . , b . - For every ∈ {1, . . . , }, either (A) = →⋫ or (B) = b□ or (C) = Ref, namely: (A) u = , Γ ⇏u b = Γ ⇏b → →⋫ or (B) u = □ , Γat, Γ→, Δ ⇏u b = Γ ⇏b □
b□ or (C) u = Γ− ⇏u − b = Γ ⇏b □
Ref
We set u ≪ u in case (A), u ≪ u in case (B), u ≪ * u in case (C).
Note that, if u ≪ * u, then the world Ψ( u) of Mod() is reflexive.
Fig. 6.
Example 18 The relations ≪ , ≪ and ≪ * induced by the ℛ-derivation of Fig. 5 are displayed in
Now we introduce two technical lemmas which are needed to prove Th. 15. = ⟨, ≤ , , , ⟩ and ∈ such that: (I1) ⊮ ′, for every leaf Γat, Γ→, □ Δ ⇏b ′ of b; (I2) ⊩ (Γ→ ∩ Sf− ( )) ∪ □ Δ; Lemma 19 Let
b be an ℛ-tree only containing b-antisequents having root Γat, Γ→, □ Δ ⇏b ; let (I3) () = Γat.
Then, ⊮ .
Proof. By induction on depth( b). The case depth( b) = 0 is trivial, since the root of b is also a leaf. Let depth( b) > 0; we only discuss the case where
0b
b = 0b = Γ ⇏b
Γ ⇏b →
→◁
Γ = Γat, Γ→, □ Δ
Γ ◁
By applying the induction hypothesis to the ℛ-tree 0b, having root 0b and the same leaves as b,
we get ⊮ . Let Γ = Γ ∩ Sf( ); by Lemma 5(iii), Γ ◁ . Since Sf( ) ⊆ Sf− ( → ), by
hypotheses (I2)–(I3) we get ⊩ Γ , which implies ⊩ (Lemma 5(iv)). This proves ⊮ → . □
Lemma 20 Let be an ℛ-derivation of u = Γ ⇏u having form (
Then, ⊩ Γ and ⊮ .
Proof. We show that: (P1) ⊮ , for every premise b = Γ ⇏b of Succ; (P2) ⊩ → , for every → ∈ Γ→.
We introduce the following induction hypothesis: (IH1) to prove Point (P1) for a formula , we inductively assume that Point (P2) holds for every formula → such that | → | < | |; (IH2) to prove Point (P2) for a formula → , we inductively assume that Point (P1) holds for every formula such that | | < | → |.
We prove Point (P1). Let b be the premise of Succ displayed in schema (
We prove (I1). Let b = Γ ⇏b any leaf of b ; we show that ⊮ . By definition of schema (
In case (a), by hypothesis (J3) there is ′ ∈ such that ≤ ′ and ′ ⊩ and ′ ⊮ , hence ⊮ → . In case (b), by hypothesis (J4) there is ′ such that ′ and ′ ⊮ , hence ⊮ □ . Let us consider case (c). By hypothesis (J5) there exists a reflexive world ′ such that ′ and ′ ⊮ − . By Lemma 2, ′ ⊩ ↔ − ; it follows that ′ ⊮ , hence ⊮ □ . In case (d), we have ∈ ∪ {⊥} and ̸∈ Γat. Since () = Γat (hypothesis (J6)), we get ⊮ . This proves that hypothesis (I1) holds.
We prove (I2). Let ∈ Γ→ ∩ Sf− ( ); since | | < | |, by (IH1) we get ⊩ . Moreover, ⊩ □ Δ by (J2), thus (I2) holds. Finally, (I3) coincides with (J6). We can apply Lemma 19 and conclude ⊮ , and this proves Point (P1).
We prove Point (P2). Let → ∈ Γ→, let ′ ∈ be such that ≤ ′ and ′ ⊩ ; we show that ′ ⊩ . Note that b = Γ ⇏b is a premise of Succ; since | | < | → |, by (IH2) we get ⊮ . This implies that < ′. By hypothesis (J1), ′ ⊩ → , hence ′ ⊩ ; this proves (P2).
We prove the assertion of the lemma. By (P2) and hypotheses (J2) and (J6), we get ⊩ Γ. The proof that ⊮ depends on the specific rule Succ at hand and follows from Point (P1) and hypothesis (J6). □
We are now in position to complete the proof of Th. 15.
Proof. [Th. 15(i)] By induction on the depth of u = Γ ⇏u in . Let be the rule of ℛ having conclusion u. We proceed by a case analysis, only detailing some significant cases.
If = Irr, then Γ = Γat, □ Δ and ∈ ( ∪ {⊥}) ∖ Γat and Ψ( u) = u. Note that ( u) = Γat, hence u ⊩ Γat and u ⊮ ; it remains to show that u ⊩ □ Δ. If u is reflexive, then u is the premise of Ref, hence Δ is empty. Otherwise, there is no in Mod() such that u, hence u ⊩ □ Δ.
If = →◁, then, u = Γ ⇏u → , where Γ ◁ , and the premise of is 1u = Γ ⇏u . By the induction hypothesis, Ψ( 1u) ⊩ Γ and Ψ( 1u) ⊮ . By Lemma 5(iv) we get Ψ( 1u) ⊩ , which implies Ψ( 1u) ⊮ → . Since Ψ( u) = Ψ( 1u), we conclude Ψ( u) ⊩ Γ and Ψ( u) ⊮ → .
If = S□u , then u = Γ ⇏u □ , where Γ = Γat, Γ→, □ Δ, and Ψ( u) = u. Let u be the subderivation of having root u; we apply Lemma 20 setting = u, = Mod() and = u. We check that hypotheses (J1)–(J6) hold.
We prove hypothesis (J1). Let ′ be a world of Mod() such that u < ′; we show that ′ ⊩ Γ→. There exists an u-antisequent ′ = Γ′ ⇏u ′ such that u ≺ ′ ⪯ ′ and either u ≪ ′ or u ≪ ′ or u ≪ * ′ (see the definition of schema 1). Since depth( ′) < depth( u), by the induction hypothesis we get Ψ( ′) ⊩ Γ′. If u ≪ ′ or u ≪ ′, we get Γ→ ⊆ Γ′, hence Ψ( ′) ⊩ Γ→. Let u ≪ * ′. Then, (Γ→)− ⊆ Γ′, hence Ψ( ′) ⊩ (Γ→)− . Since Ψ( ′) is reflexive, by Lemma 2 we get Ψ( ′) ⊩ Γ→. Having proved Ψ( ′) ⊩ Γ→, by the fact that Ψ( ′) ≤ ′ we conclude ′ ⊩ Γ→.
We prove hypothesis (J2). Let ′ be a world of Mod() such that u′; we show that ′ ⊩ Δ. There exists an u-antisequent ′ = Γ′ ⇏u ′ such that u ≺ ′ ⪯ ′ and either u ≪ ′ or u ≪ * ′. Reasoning as in the case concerning (J1), we get Ψ( ′) ⊩ Δ; since Ψ( ′) ≤ ′, we conclude ′ ⊩ Δ.
We prove (J3). Let u ≪ ′ = , Γ ⇏u ; we show that there exists ′ such that u ≤ ′ and ′ ⊩ and ′ ⊮ . By the induction hypothesis, Ψ( ′) ⊩ and Ψ( ′) ⊮ . Since u ≤ Ψ( ′), we can set ′ = Ψ( ′).
We prove (J4). Let u ≪ ′ = Γ ⇏u ; we show that there exists ′ such that u′ and ′ ⊮ . By the induction hypothesis, Ψ( ′) ⊮ . Since u Ψ( ′), we can set ′ = Ψ( ′).
We prove (J5). Let u ≪ * ′ = Γ− ⇏u − ; we show that there exists ′ such that u′, ′ is reflexive and ′ ⊮ − . By the induction hypothesis, Ψ( ′) ⊮ − . Since u Ψ( ′) and Ψ( ′) is reflexive, we can set ′ = Ψ( ′).
Hypothesis (J6), namely ( u) = Γat, holds by the definition of . By applying Lemma 20, we conclude that u ⊩ Γ and u ⊮ □ . □ Conclusions. In this paper we have presented a terminating sequent calculus Gbu-iCK4 for iCK4 enjoying a weak variant of the subformula property. If a sequent is not derivable in Gbu-iCK4, then is derivable in the dual calculus Rbu-iCK4, and from the Rbu-iCK4-derivation we can extract a countermodel for . We leave as future work the investigation of cut-admissibility for Gbu-iCK4; this is a rather tricky task since labels impose strict constraints on the shape of derivations. We also aim to extend our approach to the other provability logics with the coreflection principle related with iCK4 and iSL, such as iGL, mHC and KM (for an overview, see, e.g., [11]).
The author(s) have not employed any Generative AI tools.