[proofplan] We reduce the syntactic decision problem $S \vdash t$ to a finite semantic check. By the [Completeness Theorem](/theorems/1457), $S \vdash t$ is equivalent to $S \models t$. Because $S$ is finite, only finitely many primitive propositions occur in $S \cup \{t\}$; enumerate them as $p_1, \dots, p_n$. Every valuation of the full language is determined on the propositions relevant to $S \cup \{t\}$ by its restriction to $\{p_1, \dots, p_n\}$, of which there are exactly $2^n$. The algorithm enumerates these $2^n$ restrictions, evaluates each formula of $S$ and the formula $t$ under each, and returns "yes" iff every restriction that validates all of $S$ also validates $t$. The total running time is bounded by $2^n \cdot (|S|+1) \cdot c$ where $c$ is the cost of evaluating a single formula, so the procedure halts in finite and bounded time. [/proofplan] [step:Reduce syntactic derivability to semantic entailment via Completeness] The relation $S \vdash t$ asks for the existence of a finite formal proof of $t$ from hypotheses $S$. A naive search for such a proof is not bounded in advance — formal proofs have unbounded length. We therefore replace $\vdash$ by $\models$ using the [Completeness Theorem](/theorems/1457) for propositional calculus: \begin{align*} S \vdash t \iff S \models t. \end{align*} Both directions apply. So for the remainder of the proof it suffices to give an algorithm that decides whether $S \models t$ in finite and bounded time. [guided] Why do we immediately translate the problem? A formal proof is a finite sequence of formulas, but there is no a priori bound on its length. An algorithm that searches for proofs of increasing length will always eventually find one if it exists, but it will not halt if no proof exists — so it is not a **decision** procedure, it is only a **semi-decision** procedure. Bounded decidability requires a different approach. The trick is to use the [Completeness Theorem](/theorems/1457): \begin{align*} S \vdash t \iff S \models t. \end{align*} The left-hand side is syntactic and unbounded; the right-hand side is semantic and, crucially, involves only the finitely many primitive propositions mentioned in $S$ and $t$. We have reduced a search problem in an unbounded space to an evaluation problem in a bounded space — this is the whole idea of the proof. [/guided] [/step] [step:List the finitely many primitive propositions appearing in $S \cup \{t\}$] Since $S \subseteq L$ is finite, we may enumerate its elements as $S = \{s_1, \dots, s_m\}$. Each formula $s_i$ and the formula $t$ are finite strings built from primitive propositions using logical connectives, hence each mentions only finitely many primitive propositions. Let \begin{align*} P &:= \{p \in L : p \text{ is a primitive proposition appearing in } s_1, \dots, s_m, \text{ or } t\}. \end{align*} Then $P$ is finite; set $n := |P|$ and enumerate $P = \{p_1, \dots, p_n\}$. [guided] The hypothesis that $S$ is finite is used here for the first and only time to ensure that only finitely many primitive propositions are relevant. If $S$ were infinite, even if each formula in $S$ used finitely many atoms, the collection over all of $S$ could be infinite — and our method would fail. Let $S = \{s_1, \dots, s_m\}$ with $m = |S|$, and let \begin{align*} P &:= \{p \in L : p \text{ is a primitive proposition appearing in } s_1, \dots, s_m, \text{ or } t\}. \end{align*} A formula is a finite tree of connectives with primitive propositions at the leaves, so each of the finitely many formulas $s_1, \dots, s_m, t$ contributes finitely many primitives. $P$ is a finite union of finite sets and is therefore finite. Fix an enumeration $P = \{p_1, \dots, p_n\}$ with $n := |P|$. Why is $P$ the right set to track? Because the truth value of any Boolean combination of formulas mentioning only atoms from $P$ depends **only** on the truth values assigned to $P$. So the behaviour of $s_1, \dots, s_m, t$ under an arbitrary valuation $v: L \to \{0,1\}$ is completely determined by the restriction $v|_P: P \to \{0,1\}$. This is the lemma that collapses the infinite space of valuations down to the finite space of $\{0,1\}^P$. [/guided] [/step] [step:Enumerate the $2^n$ restricted valuations] The set of functions $P \to \{0, 1\}$ has cardinality $2^n$. Enumerate these functions as \begin{align*} v_1, v_2, \dots, v_{2^n} &: P \to \{0, 1\}. \end{align*} Each $v_j$ extends to a valuation $\tilde{v}_j: L \to \{0, 1\}$ of the entire language $L$ by assigning $\tilde{v}_j(p) = v_j(p)$ for $p \in P$ and, say, $\tilde{v}_j(p) = 0$ for every primitive proposition $p \in L \setminus P$, then extending recursively through the connectives. The choice of extension on $L \setminus P$ is immaterial for our purposes: the truth values $\tilde{v}_j(s_i)$ and $\tilde{v}_j(t)$ depend only on $v_j|_P = v_j$, since $s_1, \dots, s_m, t$ only mention atoms of $P$. [guided] We now manufacture concrete valuations to feed to the evaluation step. The finite cube $\{0,1\}^P$ has cardinality $2^n$; list its elements as $v_1, \dots, v_{2^n}$. Each $v_j$ is a function on the finite set $P$, easily represented as a length-$n$ binary string in a computer. We must, however, remember that a valuation as defined by the propositional calculus is a function on the **entire** language $L$, not merely on $P$. Extend each $v_j$ to a valuation $\tilde{v}_j: L \to \{0,1\}$ by any choice (say, assigning $0$ to every primitive outside $P$ and then computing connectives recursively). Why does the choice not matter? Because $s_1, \dots, s_m$ and $t$ are by construction built only from atoms in $P$, so their truth values under $\tilde{v}_j$ are functions of $v_j|_P$ alone. Changing $\tilde{v}_j$ on $L \setminus P$ does not alter $\tilde{v}_j(s_i)$ or $\tilde{v}_j(t)$. The upshot: semantically, only $2^n$ valuations are distinguishable by $S \cup \{t\}$, and we can enumerate them in $2^n$ steps. [/guided] [/step] [step:For each restricted valuation, evaluate $S$ and $t$ and decide membership] The algorithm proceeds as follows. For each $j \in \{1, 2, \dots, 2^n\}$: 1. Evaluate $\tilde{v}_j(s_i) \in \{0, 1\}$ for each $i = 1, \dots, m$. This is done by a standard post-order traversal of the formula's parse tree: at each leaf, read the assigned value from $v_j$; at each internal node labelled by a connective, combine the children's values using the truth table of the connective. 2. If $\tilde{v}_j(s_i) = 1$ for **all** $i$ (so the valuation satisfies $S$), evaluate $\tilde{v}_j(t)$ by the same procedure. If $\tilde{v}_j(t) = 0$, output "**No** ($S \not\vdash t$)" and halt. 3. If $\tilde{v}_j(s_i) = 0$ for some $i$ (the valuation fails $S$), no semantic constraint arises from this $v_j$; proceed to $j+1$. If the loop completes without halting at Step 2, output "**Yes** ($S \vdash t$)". [guided] We now define the algorithm explicitly. The iteration is over $j = 1, \dots, 2^n$, and for each $j$ we do three things. **Step (a) — evaluate the hypotheses.** For each formula $s_i \in S$, compute $\tilde{v}_j(s_i) \in \{0,1\}$. The evaluation is mechanical: $s_i$ is a finite parse tree, with primitive propositions at leaves and connectives at internal nodes. At each leaf, look up the value assigned by $v_j$. At each internal node, combine the child values using the truth table of the connective ($\land, \lor, \neg, \to$, etc.). A post-order traversal computes the value in time linear in the size of $s_i$. **Step (b) — check whether $v_j$ satisfies $S$.** If all $\tilde{v}_j(s_i) = 1$, then $\tilde{v}_j$ satisfies $S$ and we must check whether it satisfies $t$. Evaluate $\tilde{v}_j(t)$ the same way. If $\tilde{v}_j(t) = 0$, we have found a model of $S$ that is not a model of $t$, so $S \not\models t$, hence by Completeness $S \not\vdash t$; we output "No" and halt. **Step (c) — skip if $v_j$ does not satisfy $S$.** If $\tilde{v}_j(s_i) = 0$ for some $i$, the implication "valuation satisfies $S$ $\implies$ valuation satisfies $t$" is vacuously true under this $v_j$, and contributes nothing to deciding $S \models t$. Move on. If the loop completes without ever finding a counterexample valuation, we have verified that **every** $v_j \in \{0,1\}^P$ that satisfies $S$ also satisfies $t$. Since any valuation on $L$ is equivalent on $S \cup \{t\}$ to some $\tilde{v}_j$, this means $S \models t$, hence by Completeness $S \vdash t$; output "Yes". [/guided] [/step] [step:Bound the running time and verify correctness] **Termination in bounded time.** The outer loop runs exactly $2^n$ times. Each iteration performs at most $|S| + 1 = m + 1$ formula evaluations, and each evaluation traverses a parse tree of size bounded by the total symbol count of $s_1, \dots, s_m, t$. Writing $c$ for the cost of evaluating one formula under one valuation, the total running time is at most \begin{align*} 2^n \cdot (m + 1) \cdot c, \end{align*} which is finite and bounded by a quantity depending only on $S$ and $t$. **Correctness.** The algorithm outputs "No" precisely when some $\tilde{v}_j$ satisfies all of $S$ yet fails $t$, i.e.\ when $S \not\models t$. Every valuation of $L$ agrees with some $\tilde{v}_j$ on $P$, so $S \not\models t$ if and only if some $\tilde{v}_j$ witnesses it. Hence the algorithm outputs "No" iff $S \not\models t$, and "Yes" iff $S \models t$. By the [Completeness Theorem](/theorems/1457) (Step 1), this is equivalent to deciding $S \vdash t$. This completes the proof that the propositional calculus is decidable for finite hypothesis sets. [guided] Two things to verify: that the algorithm always halts in a bounded number of steps, and that its output is correct. **Bounded time.** The outer loop has exactly $2^n$ iterations. In each iteration we evaluate at most $|S| + 1 = m + 1$ formulas (the $s_i$'s and possibly $t$). Evaluating a single formula under a given valuation requires walking its parse tree once; let $c$ be the maximum such cost over $s_1, \dots, s_m, t$ (a constant depending only on the input). The total cost is bounded by \begin{align*} 2^n \cdot (m + 1) \cdot c. \end{align*} This is finite and depends only on the input $S, t$, not on any external parameter. In particular, the algorithm always halts. **Correctness.** Suppose the algorithm outputs "No" at iteration $j$. Then $\tilde{v}_j(s_i) = 1$ for all $i$ but $\tilde{v}_j(t) = 0$; so $\tilde{v}_j$ is a valuation satisfying $S$ but not $t$, witnessing $S \not\models t$. Conversely, suppose $S \not\models t$. Then some valuation $w: L \to \{0,1\}$ satisfies $S$ but not $t$. Consider its restriction $w|_P$; this equals $v_{j_0}$ for some $j_0 \in \{1, \dots, 2^n\}$. As noted in Step 3, the truth values of $s_1, \dots, s_m, t$ depend only on the restriction to $P$, so $\tilde{v}_{j_0}(s_i) = w(s_i) = 1$ for all $i$ and $\tilde{v}_{j_0}(t) = w(t) = 0$. Hence iteration $j_0$ outputs "No". In summary: "No" output $\iff$ $S \not\models t$ $\iff$ $S \not\vdash t$ (by Completeness). Equivalently, "Yes" output $\iff$ $S \vdash t$. The algorithm is a correct decision procedure running in time $O(2^n)$, which is bounded by a function of the input. [/guided] [/step]