[proofplan] We use cut elimination to reduce derivability to cut-free derivability. In a cut-free propositional derivation, after removing inessential weakenings, every formula that appears is a subformula of the end-sequent. Since the end-sequent has only finitely many subformulas, and contraction and exchange allow us to treat contexts as finite sets rather than ordered lists with repetitions, only finitely many relevant sequents can occur. We then decide derivability by a finite saturation procedure over this finite set of sequents. [/proofplan] [step:Pass from arbitrary derivations to cut-free derivations with subformulas of the end-sequent] Fix a finite propositional sequent $S_0 := \Gamma_0 \Rightarrow \Delta_0$. In the case of $\mathrm{LJ}$, assume $|\Delta_0| \leq 1$. Let $\operatorname{Sub}(S_0)$ denote the finite set of all subformulas of formulas appearing in $\Gamma_0 \cup \Delta_0$. By the standard cut elimination theorem for propositional $\mathrm{LK}$ and $\mathrm{LJ}$ (citing a result not yet in the wiki: Gentzen cut elimination theorem), $S_0$ is derivable if and only if it has a cut-free derivation. We use the corresponding subformula property for cut-free propositional derivations, with inessential weakenings deleted: every formula appearing in such a derivation is a member of $\operatorname{Sub}(S_0)$. Thus, to decide whether $S_0$ is derivable, it is enough to decide whether there exists a cut-free derivation of $S_0$ all of whose formulas lie in the finite set $\operatorname{Sub}(S_0)$. [guided] Fix a finite propositional sequent $S_0 := \Gamma_0 \Rightarrow \Delta_0$. In the intuitionistic case $\mathrm{LJ}$, assume $|\Delta_0| \leq 1$, because intuitionistic sequents have at most one formula in the succedent. Define $\operatorname{Sub}(S_0)$ to be the set of all subformulas of formulas appearing in $\Gamma_0 \cup \Delta_0$. The reason for introducing $\operatorname{Sub}(S_0)$ is that cut elimination bounds the formulas needed in proof search. By the standard Gentzen cut elimination theorem for propositional $\mathrm{LK}$ and $\mathrm{LJ}$, applied to the finite propositional sequent $S_0$, the sequent $S_0$ is derivable if and only if $S_0$ has a cut-free derivation. The hypotheses are exactly the present ones: we are working in the propositional sequent calculi $\mathrm{LK}$ and $\mathrm{LJ}$, and $S_0$ is a finite sequent of the appropriate shape. The associated subformula property for cut-free propositional derivations says that logical rules in a cut-free proof only decompose formulas already present in their conclusions. After deleting weakenings that introduce formulas never used later, every formula appearing in the derivation is therefore a subformula of a formula in the end-sequent. Hence every formula in the relevant cut-free derivation belongs to $\operatorname{Sub}(S_0)$. Since $S_0$ is finite and each propositional formula has finitely many subformulas, $\operatorname{Sub}(S_0)$ is finite. Thus, to decide whether $S_0$ is derivable, it is enough to decide whether there exists a cut-free derivation of $S_0$ whose formulas all lie in the finite set $\operatorname{Sub}(S_0)$. [/guided] [/step] [step:Replace contexts by finite sets of subformulas] Because exchange is admissible in both $\mathrm{LK}$ and $\mathrm{LJ}$, the order of formulas in a context does not affect derivability. Because contraction is admissible, repeated copies of the same formula do not affect derivability. Therefore, for the purpose of deciding derivability, we may represent each context by a subset of $\operatorname{Sub}(S_0)$. Let \begin{align*} \mathcal{Q}_{\mathrm{LK}}(S_0) := \{\, \Gamma \Rightarrow \Delta \mid \Gamma \subseteq \operatorname{Sub}(S_0),\ \Delta \subseteq \operatorname{Sub}(S_0) \,\} \end{align*} be the finite set of classical sequents built from subformulas of $S_0$. If $m := |\operatorname{Sub}(S_0)|$, then \begin{align*} |\mathcal{Q}_{\mathrm{LK}}(S_0)| = 2^m \cdot 2^m = 4^m. \end{align*} For intuitionistic sequents define \begin{align*} \mathcal{Q}_{\mathrm{LJ}}(S_0) := \{\, \Gamma \Rightarrow \Delta \mid \Gamma \subseteq \operatorname{Sub}(S_0),\ \Delta \subseteq \operatorname{Sub}(S_0),\ |\Delta| \leq 1 \,\}. \end{align*} Then \begin{align*} |\mathcal{Q}_{\mathrm{LJ}}(S_0)| = 2^m(m+1), \end{align*} because the succedent is either empty or consists of one formula from $\operatorname{Sub}(S_0)$. [guided] The structural rules are what make the search space finite at the level of sequents, not merely at the level of formulas. Without contraction, one would have to consider sequents containing arbitrarily many repeated copies of the same formula. Without exchange, one would have to consider arbitrary orderings. But exchange removes dependence on order, and contraction removes dependence on multiplicity. Thus a context can be treated as a finite set of formulas. In the classical calculus, both the antecedent and succedent may be arbitrary subsets of $\operatorname{Sub}(S_0)$, giving $2^m$ choices for each side and hence $4^m$ possible sequents. In the intuitionistic calculus, the succedent is restricted to have at most one formula, so there are $m+1$ choices for the succedent: the empty succedent, or one of the $m$ formulas. The antecedent still has $2^m$ choices. This gives a finite search space in both cases. [/guided] [/step] [step:Define a finite saturation procedure for proof search] We describe the procedure for either calculus $\mathsf{G} \in \{\mathrm{LK}, \mathrm{LJ}\}$. Let $\mathcal{Q}_{\mathsf{G}}(S_0)$ denote the corresponding finite set of sequents defined above. Define a sequence of subsets \begin{align*} D_0 \subseteq D_1 \subseteq D_2 \subseteq \cdots \subseteq \mathcal{Q}_{\mathsf{G}}(S_0) \end{align*} as follows. Let $D_0$ be the set of all initial sequents in $\mathcal{Q}_{\mathsf{G}}(S_0)$. Having defined $D_k$, define $D_{k+1}$ to be $D_k$ together with every sequent $T \in \mathcal{Q}_{\mathsf{G}}(S_0)$ for which there is a cut-free inference rule of $\mathsf{G}$ whose conclusion is $T$ and whose premises all lie in $D_k$. Since $\mathcal{Q}_{\mathsf{G}}(S_0)$ is finite, this increasing sequence stabilizes after at most $|\mathcal{Q}_{\mathsf{G}}(S_0)|$ strict enlargements. Let \begin{align*} D_\infty := \bigcup_{k=0}^{\infty} D_k. \end{align*} The algorithm computes $D_0,D_1,D_2,\dots$ until $D_{k+1}=D_k$, and then accepts $S_0$ exactly when $S_0 \in D_k$. [guided] Fix one calculus $\mathsf{G} \in \{\mathrm{LK}, \mathrm{LJ}\}$. Let $\mathcal{Q}_{\mathsf{G}}(S_0)$ be the corresponding finite set of sequents built from $\operatorname{Sub}(S_0)$: for $\mathrm{LK}$ this is $\mathcal{Q}_{\mathrm{LK}}(S_0)$, and for $\mathrm{LJ}$ this is $\mathcal{Q}_{\mathrm{LJ}}(S_0)$. We now define a finite fixed-point computation. Define subsets \begin{align*} D_0 \subseteq D_1 \subseteq D_2 \subseteq \cdots \subseteq \mathcal{Q}_{\mathsf{G}}(S_0) \end{align*} recursively as follows. Let $D_0$ be the set of all initial sequents in $\mathcal{Q}_{\mathsf{G}}(S_0)$. Here an initial sequent means a contextual identity axiom: a sequent $\Gamma \Rightarrow \Delta$ such that some formula $A \in \operatorname{Sub}(S_0)$ lies on both sides, so $A \in \Gamma \cap \Delta$; in $\mathrm{LJ}$ this is interpreted with $|\Delta| \leq 1$. These contextual identity sequents absorb the weakenings that were already folded into the finite set representation of contexts. Having defined $D_k$, define $D_{k+1}$ to be $D_k$ together with every sequent $T \in \mathcal{Q}_{\mathsf{G}}(S_0)$ for which there is a cut-free inference rule of $\mathsf{G}$ whose conclusion is $T$ and whose premises all lie in $D_k$. The construction is effective because $\mathcal{Q}_{\mathsf{G}}(S_0)$ is finite and the propositional cut-free inference rules can be checked by a finite inspection of possible premises and conclusions inside $\mathcal{Q}_{\mathsf{G}}(S_0)$. At every stage $D_k$ is a subset of the finite set $\mathcal{Q}_{\mathsf{G}}(S_0)$. If $D_{k+1} \neq D_k$, then at least one new sequent has been added. Therefore strict enlargement can occur at most $|\mathcal{Q}_{\mathsf{G}}(S_0)|$ times. Define \begin{align*} D_\infty := \bigcup_{k=0}^{\infty} D_k. \end{align*} The algorithm computes $D_0,D_1,D_2,\dots$ until it reaches a stage with $D_{k+1}=D_k$. Once this equality holds, applying the same rule-closure operation again cannot add a new sequent, so the fixed point has been reached. The procedure then accepts $S_0$ exactly when $S_0 \in D_k$ at that stable stage. [/guided] [/step] [step:Prove that saturation accepts exactly the cut-free derivable sequents] Let $\mathbb{N}$ denote the set of positive integers. We prove by [induction on derivation height](/theorems/4623) that every sequent in $\mathcal{Q}_{\mathsf{G}}(S_0)$ having a cut-free derivation belongs to $D_\infty$. If the derivation has height $0$, then its end-sequent is initial, hence belongs to $D_0 \subseteq D_\infty$. Suppose the derivation has positive height. Let $T$ be its end-sequent, and let $T_1,\dots,T_r$ be the premises of the last inference rule, where $r \in \mathbb{N}$ depends on the rule. Each $T_i$ has a cut-free derivation of smaller height. By the induction hypothesis, $T_i \in D_\infty$ for each $i$. Hence there exists $k \in \mathbb{N}$ such that $T_i \in D_k$ for all $i$. By the definition of the saturation procedure, $T \in D_{k+1} \subseteq D_\infty$. Conversely, every sequent in $D_\infty$ has a cut-free derivation. This is proved by induction on the least $k$ such that the sequent belongs to $D_k$. If $k=0$, the sequent is initial. If $k>0$, then the sequent was added as the conclusion of a cut-free inference rule whose premises lie in $D_{k-1}$; by induction those premises have cut-free derivations, and appending the inference rule gives a cut-free derivation of the conclusion. Therefore $D_\infty$ is exactly the set of sequents in $\mathcal{Q}_{\mathsf{G}}(S_0)$ that have cut-free derivations using formulas from $\operatorname{Sub}(S_0)$. [/step] [step:Conclude decidability for propositional $\mathrm{LK}$ and $\mathrm{LJ}$] For $\mathsf{G}=\mathrm{LK}$, the finite saturation procedure terminates and accepts $S_0$ if and only if $S_0$ has a cut-free $\mathrm{LK}$ derivation using only formulas from $\operatorname{Sub}(S_0)$. By cut elimination and the subformula property, this holds if and only if $\mathrm{LK} \vdash S_0$. For $\mathsf{G}=\mathrm{LJ}$, the same argument applies with the finite intuitionistic search space $\mathcal{Q}_{\mathrm{LJ}}(S_0)$, where succedents have cardinality at most $1$. Thus the procedure terminates and accepts $S_0$ if and only if $\mathrm{LJ} \vdash S_0$. Hence derivability in propositional $\mathrm{LK}$ and derivability in propositional $\mathrm{LJ}$ are decidable. [/step]