A Kruskal Decision Procedure for Intuitionistic Modal Logic $\mathsf{IK4}$

Root the underlying undirected tree temporarily at $v$ and define $I^{\prime}$ by induction on the distance from $v$. Put $I^{\prime}(v)=x$. Suppose the value of a node has been fixed and consider an adjacent node not yet assigned.

If $s$ is assigned and $t$ is an original child of $s$, then $I(s)\leq I^{\prime}(s)$ and $I(s)RI(t)$. Applying F2 to these two relations gives a world $I^{\prime}(t)$ such that

$$I^{\prime}(s)RI^{\prime}(t),\qquad I(t)\leq I^{\prime}(t).$$

If instead $t$ is assigned and $s$ is its original parent, then $I(s)RI(t)\leq I^{\prime}(t)$. F1 gives a world $I^{\prime}(s)$ with

$$I(s)\leq I^{\prime}(s),\qquad I^{\prime}(s)RI^{\prime}(t).$$

Every node has a unique predecessor in the temporary rooting at $v$, so it is assigned exactly once. Since $T$ is finite, every node is reached after finitely many steps, and every original modal edge is respected in its original direction. ∎

For a rule with premises $P_{1},\ldots,P_{k}$, it suffices to prove the following contrapositive statement: every assignment which falsifies the conclusion can be turned into an assignment which falsifies at least one premise. When $k=0$ there is no such assignment. An $id$-conclusion would require the same atom to be true as an input and false as the output at one node, while a $\bot^{\bullet}$-conclusion would require $\bot$ to be true. For the propositional rules other than implication, the claim follows directly from the truth clauses. In the branching cases, truth of an input disjunction or falsity of an output conjunction selects the required premise.

Let $I$ falsify a conclusion whose principal formula is $(A\to B)^{\circ}$ at a node $u$, and put $x=I(u)$. There is $y\geq x$ with $y\Vdash A$ and $y\nVdash B$. By section˜2.3, $I$ lifts to an edge-respecting assignment $I^{\prime}$ such that $I^{\prime}(u)=y$ and $I(v)\leq I^{\prime}(v)$ at every inherited node. Persistence keeps all inherited inputs true; the added input $A^{\bullet}$ is true at $u$, whereas the new output $B^{\circ}$ is false there. Thus the premise is falsified.

Suppose next that $(A\to B)^{\bullet}$ is principal at $u$. The conclusion assignment makes $A\to B$ true at $I(u)$. By reflexivity of $\leq$, either $I(u)\nVdash A$ or $I(u)\Vdash B$: if $A$ is true, the implication clause at $I(u)$ forces $B$. In the first case delete the previous output and make $A^{\circ}$ the output at $u$; all inputs, including $(A\to B)^{\bullet}$, remain true, so the first premise is false. In the second case use the second premise: its distinguished $(A\to B)^{\bullet}$ occurrence is replaced by $B^{\bullet}$, while any equal occurrence belonging to the side context is retained. The previous false output is unchanged, so this premise is falsified.

If $(\Diamond A)^{\bullet}$ is principal at $u$, choose $y$ with $I(u)Ry$ and $y\Vdash A$. Extending $I$ by assigning $y$ to the fresh child makes every premise input true and leaves the previous output false. If $(\Box A)^{\circ}$ is principal at $u$, its falsity gives worlds $y,z$ with $I(u)\leq y$, $yRz$, and $z\nVdash A$. Lift the original assignment at $u$ to $y$, use persistence for every inherited input, and assign $z$ to the fresh child. The premise output $A^{\circ}$ is then false.

Propagation deserves a separate line: strict descendancy in the nested tree must be read as a genuine non-empty $R$-path. If $u\prec v$, write the unique modal path as

$$u=v_{0}\to v_{1}\to\cdots\to v_{n}=v\qquad(n\geq 1).$$

An edge-respecting assignment gives $I(v_{0})RI(v_{1})R\cdots RI(v_{n})$; induction on $n$, using transitivity, yields $I(u)RI(v)$. Hence falsity of $\Diamond A$ at $I(u)$ implies falsity of $A$ at $I(v)$, which falsifies the premise of $p_{\Diamond}$. Likewise, if $\Box A$ is true at $I(u)$, reflexivity gives $I(u)\leq I(u)$, and together with $I(u)RI(v)$ the box clause yields $I(v)\Vdash A$. Adding $A^{\bullet}$ at $v$ therefore falsifies the premise of $p_{\Box}$. These cases exhaust the rules. ∎

By Lyon’s Remark 2, replace every instance of $\Diamond r$ or $\Box l$ by the height-preserving propagation instance along its displayed edge [13, Remark 2]. Read the normalized proof upwards. Propositional and propagation rules leave the relational graph unchanged. The rules $\Diamond l$ and $\Box r$ each add an atom $xRy$, where $x$ already labels the principal formula in the conclusion and $y$ is fresh. The new edge therefore attaches a single leaf and cannot duplicate an existing edge. No rule changes the root. The refined calculus for $\mathcal{A}_{4}$ has no seriality rule, and $S_{0,2}$ has been eliminated. Hence tree shape and root are preserved. This is Lyon’s Lemma 3 for non-degenerate relational trees [13, Lemma 3]; the same inspection covers the one-vertex case admitted here.

An induction on the height of $\mathcal{D}$ carries the translation through the proof, with each labelled sequent read by $N_{r}$. For the initial rules and the propositional rules other than $\to l$, the relational graph is unchanged and every displayed formula remains at the same label; applying $N_{r}$ therefore yields the corresponding nested rule in figure˜1. For $\to l$, the first labelled premise moves the output to the node carrying the principal implication and places $A$ there. Its translation is $\mathcal{C}^{\downarrow}\{(A\to B)^{\bullet},A^{\circ}\}$. The second premise keeps the previous output and replaces the distinguished implication occurrence by $B^{\bullet}$. These are precisely the two premises of $\to^{\bullet}$, including deletion of the previous output in the first.

The eigenlabel rules $\Diamond l$ and $\Box r$ translate to $\Diamond^{\bullet}$ and $\Box^{\circ}$, with the fresh label becoming the fresh child. A propagation step from $x$ to $y$ is licensed by a word in $L_{g(\mathcal{A}_{4})}(\Diamond)$, hence by a non-empty forward path; in the rooted tree this says that $y$ is a strict descendant of $x$. It therefore translates to $p_{\Diamond}$ or $p_{\Box}$. Each labelled inference becomes one nested inference, with root, output node, and output formula preserved. Since the list of rule schemes is finite and each translation is syntactic, the construction is effective and height-preserving. ∎

Let $A$ be valid on transitive Fischer–Servi frames. The frame condition for $\mathcal{A}_{4}$ is $R^{2}\subseteq R$, so the labelled sequent

$$\varnothing,\varnothing\vdash w:A$$

is $\mathcal{A}_{4}$-valid. Lyon’s Theorem 4 yields a proof in the refined labelled calculus $\mathsf{IK}(\mathcal{A}_{4})\mathsf{L}$ [13, Theorem 4]. Since cut is not a rule of $\mathsf{IK}(\mathcal{A}_{4})\mathsf{L}$, the resulting labelled proof is cut free. Its conclusion is the one-vertex tree with root $w$, and section˜2.4 translates the proof into a proof of $N_{w}(\varnothing,\varnothing\vdash w:A)=A^{\circ}$ in the multiset presentation. ∎

Both directions come from the same elementary observation. If

$$C\Longrightarrow_{r}(P_{1},\ldots,P_{k})$$

is a multiset inference, then

$$C^{\flat}\Longrightarrow_{r}(P_{1}^{\flat},\ldots,P_{k}^{\flat})$$

is an inference of the corresponding rule with set inputs. Indeed, for input multisets $M,N$, erasing repetitions commutes with filling an input hole. Writing $M\uplus N$ for multiset union,

$$(M\uplus N)^{\flat}=M^{\flat}\cup N^{\flat}.$$

The modal tree, the unique output, freshness, and the chosen propagation path are unchanged. Distinguished input occurrences may be followed before repetitions are erased. If a principal occurrence has an equal copy in the side context, the latter remains after the principal occurrence is removed or replaced; if no such contextual copy was chosen, it does not. These are exactly the two applications allowed by the convention preceding the rules. Coincident displayed subformulae and branching rules require no new argument: the required multiset copies are distinguished before erasure, and the same erased context occurs in every branch. The first premise of $\to^{\bullet}$ changes only the output, while the modal rules change only the fresh child or the propagation path. Thus the displayed local fact holds for every rule.

Induction on derivation height lifts this local observation to whole proofs. Apply it to the last inference and the induction hypothesis to each immediate premise; the height does not increase.

Conversely, fix an inference with set inputs, including its chosen side contexts. Give every contextual input one multiset occurrence and add the distinguished principal occurrences required by the rule. When a principal formula also belongs to the chosen side context, these are two occurrences; when two displayed subformulae coincide, use the corresponding number of distinguished copies. Keep the output, tree, fresh child, and propagation path unchanged. This is a multiset inference, and erasing its repeated inputs recovers the given inference with set inputs. ∎

Soundness is theorem˜2.4. Conversely, validity gives a cut-free proof in the multiset presentation by section˜2.4. Since $A^{\circ}$ contains no input occurrences, $(A^{\circ})^{\flat}=A^{\circ}$; hence section˜2.4 turns that proof into a $\mathsf{NIK4}$ proof of the same endsequent. ∎

Reading a cut-free rule upwards, every formula newly displayed in a premise is a subformula of a principal formula in the conclusion; propagation merely moves such a subformula. The nullary rules add nothing to a branch: they only close a nested sequent already reached. Hence every formula in the proof belongs to $\Phi$. In particular, $\bot$ can occur only when it is already a subformula of $A_{0}$. ∎

Fix a multiset presentation of $I$. At every conclusion node $x$ on which the rule acts, its principal input formulae occur in $\Gamma_{C}(x)$ and hence in $\Gamma_{D}(f(x))$. Choose a multiset presentation of $D$ with one contextual occurrence for each occurrence designated contextual in $I$. Put every input formula of $D$ not used by $I$ into the side context, and add the distinguished principal occurrences required by the rule. Thus a formula which is both contextual and principal receives two occurrences. Applying $r$ at the image positions and then erasing repetitions gives an inference

$$J:\quad D\Longrightarrow_{r}(Q_{1},\ldots,Q_{k}).$$

For a modal introduction, the fresh child of $Q_{i}$ is attached to the image of the principal node inherited from the conclusion.

Define $f_{i}$ on inherited nodes by

$$f_{i}(\iota_{i}^{I}(x))=\iota_{i}^{J}(f(x))\qquad(x\in V_{C}),$$

and, when $P_{i}$ has a fresh child, send it to the fresh child of $Q_{i}$. The map is injective and sends root to root. Let $A$ be an input formula at an inherited node $\iota_{i}^{I}(x)$ of $P_{i}$. Relative to the fixed multiset inference, either $A$ is inherited from the side context of $C$ or it is supplied by the rule. In the first case $A\in\Gamma_{C}(x)$, hence $A\in\Gamma_{D}(f(x))$, and the chosen side context retains it in $Q_{i}$. In the second case the lifted inference supplies $A$ at $\iota_{i}^{J}(f(x))$. The same alternative covers a fresh child, where every displayed formula is supplied by the modal rule. Therefore

$$\Gamma_{P_{i}}(v)\subseteq\Gamma_{Q_{i}}(f_{i}(v))\qquad(v\in V_{P_{i}}).$$

For the output there are three possibilities. It is inherited unchanged by all input rules, by $p_{\Box}$, and by the second premise of $\to^{\bullet}$; it is then preserved by $f$. An output rule, the first premise of $\to^{\bullet}$, or $p_{\Diamond}$ places the corresponding output formula at corresponding inherited nodes. Finally, $\Box^{\circ}$ places it at the two corresponding fresh children. Hence $f_{i}$ maps the unique output node of $P_{i}$ to that of $Q_{i}$ and preserves its formula.

Every edge of $P_{i}$ between inherited nodes comes from an edge of $C$; use for it the path by which $f$ represents that edge in $D$. These paths retain clause (iv) of section˜3.1. If $P_{i}$ has a fresh child and $x$ is the principal conclusion node, the edge from $\iota_{i}^{I}(x)$ to that child is represented by the corresponding fresh edge in $Q_{i}$. Its parent is $\iota_{i}^{J}(f(x))$, the inherited copy of an $f$-image node; clause (iv) for $f$ says that $f(x)$ is not internal to any path representing an inherited edge. The fresh edge therefore meets every path representing an inherited edge only at its parent, if at all. For a propagation rule, an active relation $u\prec v$ in $C$ is sent by $f$ to a non-empty path from $f(u)$ to $f(v)$, so the same side condition holds in $D$.

When $k=0$, there are no premises to treat. If $r=id$, clause (ii) for $f$ preserves the matching input atom at the output node; if $r=\bot^{\bullet}$, it preserves $\bot$ at the active node. Thus the same nullary rule applies to $D$. For $k>0$, the preceding paragraphs verify all clauses of section˜3.1 for each $f_{i}$. Every step uses only the finite data carried by $I$ and $f$, so the inference $J$ and the embeddings $f_{i}$ are obtained effectively. ∎

Induct on the height of the given proof of $S$. If its last inference is the nullary inference $S\Longrightarrow_{r}()$, apply section˜3.2 to that inference and to $f$; the result is the corresponding nullary inference with conclusion $T$.

Otherwise write the last inference as

$$S\Longrightarrow_{r}(P_{1},\ldots,P_{k}).$$

By section˜3.2, the embedding $f$ effectively yields an inference $T\Longrightarrow_{r}(Q_{1},\ldots,Q_{k})$ and embeddings $f_{i}:P_{i}\preceq Q_{i}$. Applying the induction hypothesis to each $f_{i}$ and the corresponding premise proof gives proofs of all $Q_{i}$ of no greater height. Reapplying $r$ proves $T$. ∎

We mark the root in the label, rather than pass to pointed trees, so that the appeal to the labelled Tree Theorem is literal. Let

$$Q_{\Phi}=\{\mathsf{root},\mathsf{other}\}\times\mathcal{P}(\Phi)\times(\Phi\cup\{\varnothing\}).$$

The first coordinate is the root marker; the third is empty at every node except the unique output node. Declare a triple $(\rho,\Gamma,o)$ to be below $(\rho^{\prime},\Gamma^{\prime},o^{\prime})$ exactly when

$$\rho=\rho^{\prime},\qquad\Gamma\subseteq\Gamma^{\prime},\qquad o=o^{\prime}.$$

This is a finite quasi-order and hence a wqo.

Kruskal states the Tree Theorem for finite rooted structured trees whose vertices are labelled in a wqo [11, §2, pp. 211–212]. His structured trees carry a linear order on the edges leaving each vertex. To apply the theorem here, choose an arbitrary such order at every node of every tree in an infinite sequence of nested sequents. Kruskal then gives a pair related by an order-preserving labelled monomorphism. For these trees, each source edge is represented by an oriented path whose interior contains no image node; paths representing distinct source edges meet only in the image of a common endpoint and are otherwise vertex-disjoint. After the auxiliary orders are forgotten, the same map is therefore an embedding in the sense of section˜3.1. Thus the order used by Kruskal is stronger than $\preceq$, which is all the wqo argument needs. Nash–Williams’s formulation makes explicit that the underlying unlabelled relation is homeomorphism onto a subtree [14, p. 833].

The three coordinates of $Q_{\Phi}$ impose the remaining clauses. Equality of the root marker sends the sole node carrying $\mathsf{root}$ in the source to the sole such node in the target. Inclusion of the second coordinate is the required inclusion of input formulae, and equality of the third preserves both the output node and its formula. Hence every infinite sequence of nested sequents has a $\preceq$-comparable pair. The relation is therefore a wqo, and its decidability was established above. ∎

The empty set has the empty basis. Suppose $U\neq\varnothing$ and fix $T_{0}\in U$. If no $\lhd$-minimal member of $U$ lay below $T_{0}$, choose $T_{n+1}\in U$ with $T_{n+1}\lhd T_{n}$ recursively. This choice can be continued: a minimal member below some $T_{n}$ would also lie below $T_{0}$. For $i<j$, transitivity gives $T_{j}\preceq T_{i}$, whereas $T_{i}\preceq T_{j}$ would imply $T_{i}\preceq T_{i+1}$, contrary to $T_{i+1}\lhd T_{i}$. The sequence would therefore be bad. Hence every member of $U$ lies above a minimal one. Distinct minimal $\equiv$-classes are incomparable, and infinitely many such classes would give an infinite bad sequence by choosing one representative from each. There are consequently only finitely many minimal classes. One representative from each forms a finite basis: its upward closure is contained in $U$, while every member of $U$ lies above one of the representatives.

For the second assertion, suppose that an increasing chain $(U_{n})_{n\in\mathbb{N}}$ does not stabilise. Choose recursively

$$n_{0}<n_{1}<n_{2}<\cdots\qquad\text{with}\qquad U_{n_{i}}\subsetneq U_{n_{i+1}},$$

and choose $T_{i}\in U_{n_{i+1}}\setminus U_{n_{i}}$. By section˜3.3, there are $i<j$ with $T_{i}\preceq T_{j}$. Since $n_{i+1}\leq n_{j}$, we have $T_{i}\in U_{n_{i+1}}\subseteq U_{n_{j}}$; upward closure of $U_{n_{j}}$ then gives $T_{j}\in U_{n_{j}}$, contrary to the choice of $T_{j}$. Thus the chain stabilises. ∎