[proofplan] Given a propositional formula $A$, we use only the finitely many propositional variables that actually occur in $A$. There are finitely many Boolean assignments to those variables, and for each such assignment the truth value of $A$ is computed by a finite structural evaluation of its syntax tree. The decision algorithm checks all these finitely many assignments and accepts exactly when every one makes $A$ true. [/proofplan] [step:Extract the finite set of variables occurring in the input formula] Let $A \in \operatorname{Form}(\mathcal{L})$ be the input formula. Define $\operatorname{At}(A)$ to be the set of propositional variables that occur in $A$. Since $A$ is a finite string built from finitely many symbols, scanning the string from left to right produces a finite list of all variable occurrences in $A$. Removing repetitions gives a finite set \begin{align*} \operatorname{At}(A) = \{p_1,\dots,p_m\}, \end{align*} where $m \in \mathbb{N} \cup \{0\}$ and $p_1,\dots,p_m$ are distinct propositional variables. [guided] The first reduction is from all possible valuations of the whole language to valuations of only the variables that appear in the formula. Let $A \in \operatorname{Form}(\mathcal{L})$ be the input formula. We define $\operatorname{At}(A)$ to be the set of propositional variables that occur as atomic subformulas of $A$. The formula $A$ is a finite syntactic object. Therefore its displayed string, or equivalently its syntax tree, has only finitely many atomic leaves. By scanning the formula and recording each propositional variable that occurs, then deleting repeated entries, we obtain a finite set \begin{align*} \operatorname{At}(A) = \{p_1,\dots,p_m\}, \end{align*} where $m \in \mathbb{N} \cup \{0\}$ and $p_1,\dots,p_m$ are pairwise distinct. The case $m=0$ means that $A$ contains no propositional variables; then there is exactly one assignment to the empty set of variables. [/guided] [/step] [step:Enumerate all Boolean assignments to those variables] Define the finite set of restricted Boolean valuations \begin{align*} \mathcal{V}_A := \{0,1\}^{\operatorname{At}(A)}. \end{align*} After choosing the ordering $\operatorname{At}(A)=\{p_1,\dots,p_m\}$, each element $\sigma \in \mathcal{V}_A$ is represented by an $m$-tuple \begin{align*} (\sigma(p_1),\dots,\sigma(p_m)) \in \{0,1\}^m. \end{align*} Thus $\mathcal{V}_A$ has exactly $2^m$ elements. The algorithm can enumerate them lexicographically as binary strings of length $m$. [guided] We now need to check finitely many possibilities. Define \begin{align*} \mathcal{V}_A := \{0,1\}^{\operatorname{At}(A)} \end{align*} to be the set of all functions $\sigma: \operatorname{At}(A) \to \{0,1\}$. These are not yet valuations of every propositional variable in the language; they are the restrictions that matter for the formula $A$. Using the ordering \begin{align*} \operatorname{At}(A)=\{p_1,\dots,p_m\}, \end{align*} each $\sigma \in \mathcal{V}_A$ is completely determined by the binary tuple \begin{align*} (\sigma(p_1),\dots,\sigma(p_m)) \in \{0,1\}^m. \end{align*} There are exactly $2^m$ such tuples, so $\mathcal{V}_A$ is finite. An algorithm can enumerate them by listing the binary strings of length $m$ in lexicographic order. If $m=0$, the set $\{0,1\}^0$ contains exactly the empty function, so the enumeration still consists of finitely many cases. [/guided] [/step] [step:Compute the truth value of the formula under each assignment] For each $\sigma \in \mathcal{V}_A$, define the evaluation map \begin{align*} E_\sigma: \{\text{subformulas of } A\} &\to \{0,1\} \end{align*} by structural recursion on subformulas. If $B$ is an atomic subformula $p_i$, set \begin{align*} E_\sigma(B) := \sigma(p_i). \end{align*} For compound formulas, define $E_\sigma$ according to the truth table of the outermost Boolean connective; for example, \begin{align*} E_\sigma(\neg B) &:= 1 - E_\sigma(B), \\ E_\sigma(B \wedge C) &:= \min\{E_\sigma(B),E_\sigma(C)\}, \\ E_\sigma(B \vee C) &:= \max\{E_\sigma(B),E_\sigma(C)\}, \\ E_\sigma(B \to C) &:= \max\{1-E_\sigma(B),E_\sigma(C)\}. \end{align*} Since $A$ has finitely many subformulas and each recursive call is made on a proper subformula, the computation of $E_\sigma(A)$ terminates. [guided] Fix an assignment $\sigma \in \mathcal{V}_A$. We define a function \begin{align*} E_\sigma: \{\text{subformulas of } A\} &\to \{0,1\} \end{align*} which assigns a truth value to every subformula of $A$. The definition follows the syntax tree from the leaves upward. If $B$ is an atomic subformula, then $B=p_i$ for some $i \in \{1,\dots,m\}$, and we set \begin{align*} E_\sigma(B) := \sigma(p_i). \end{align*} If $B$ is compound, its immediate subformulas are smaller formulas, so their values have already been determined when the syntax tree is evaluated bottom-up. We then use the truth table of the outermost connective. For the usual connectives this gives \begin{align*} E_\sigma(\neg B) &:= 1 - E_\sigma(B), \\ E_\sigma(B \wedge C) &:= \min\{E_\sigma(B),E_\sigma(C)\}, \\ E_\sigma(B \vee C) &:= \max\{E_\sigma(B),E_\sigma(C)\}, \\ E_\sigma(B \to C) &:= \max\{1-E_\sigma(B),E_\sigma(C)\}. \end{align*} For any additional Boolean connective in the finite language, the same procedure uses its finite truth table. This computation terminates because the syntax tree of $A$ is finite. Every recursive call moves from a formula to one of its proper subformulas, so there cannot be an infinite descending chain of recursive calls. Hence, for each $\sigma \in \mathcal{V}_A$, the value $E_\sigma(A) \in \{0,1\}$ is effectively computed in finitely many steps. [/guided] [/step] [step:Accept exactly when every assignment makes the formula true] Define the decision procedure $D$ on input $A \in \operatorname{Form}(\mathcal{L})$ as follows. First compute $\operatorname{At}(A)=\{p_1,\dots,p_m\}$. Then enumerate every $\sigma \in \mathcal{V}_A$. For each such $\sigma$, compute $E_\sigma(A)$. If some $\sigma$ satisfies $E_\sigma(A)=0$, return no. If all enumerated assignments satisfy $E_\sigma(A)=1$, return yes. The procedure halts because $\mathcal{V}_A$ is finite and each evaluation $E_\sigma(A)$ terminates. It remains to verify correctness. If $D$ returns yes, then $E_\sigma(A)=1$ for every assignment $\sigma:\operatorname{At}(A)\to\{0,1\}$. Any Boolean valuation $v$ of the full propositional language restricts to an element $v|_{\operatorname{At}(A)} \in \mathcal{V}_A$, and the value of $A$ under $v$ depends only on this restriction. Hence $v(A)=1$ for every Boolean valuation $v$, so $A$ is valid. Conversely, if $A$ is valid, then every full Boolean valuation extending any $\sigma \in \mathcal{V}_A$ makes $A$ true, and therefore $E_\sigma(A)=1$ for every $\sigma \in \mathcal{V}_A$. The algorithm consequently returns yes. Thus the algorithm returns yes exactly for valid formulas and no exactly for invalid formulas. [guided] We now assemble the decision algorithm. On input $A \in \operatorname{Form}(\mathcal{L})$, the algorithm first computes \begin{align*} \operatorname{At}(A)=\{p_1,\dots,p_m\}. \end{align*} It then enumerates the finite set \begin{align*} \mathcal{V}_A=\{0,1\}^{\operatorname{At}(A)}. \end{align*} For each assignment $\sigma \in \mathcal{V}_A$, it computes $E_\sigma(A)$. If any one of these computations gives \begin{align*} E_\sigma(A)=0, \end{align*} then the algorithm returns no. If all of them give \begin{align*} E_\sigma(A)=1, \end{align*} then the algorithm returns yes. The algorithm halts because two finite processes are being nested: there are only $2^m$ assignments $\sigma \in \mathcal{V}_A$, and for each one the evaluation of $A$ is a finite computation along the finite syntax tree of $A$. It remains to prove that this halting algorithm decides validity. Suppose first that the algorithm returns yes. Then \begin{align*} E_\sigma(A)=1 \end{align*} for every $\sigma:\operatorname{At}(A)\to\{0,1\}$. Let $v$ be any Boolean valuation of the full propositional language. Its restriction \begin{align*} v|_{\operatorname{At}(A)}:\operatorname{At}(A)\to\{0,1\} \end{align*} is an element of $\mathcal{V}_A$. Since every atom occurring in $A$ lies in $\operatorname{At}(A)$, the truth value of $A$ under $v$ is determined entirely by $v|_{\operatorname{At}(A)}$. Therefore \begin{align*} v(A)=E_{v|_{\operatorname{At}(A)}}(A)=1. \end{align*} Because $v$ was arbitrary, every Boolean valuation makes $A$ true, so $A$ is valid. Conversely, suppose $A$ is valid. Let $\sigma \in \mathcal{V}_A$ be arbitrary. Extend $\sigma$ to a Boolean valuation $v$ of the full propositional language by assigning arbitrary truth values to variables not in $\operatorname{At}(A)$. Since $A$ is valid, $v(A)=1$. The formula $A$ contains no variables outside $\operatorname{At}(A)$, so evaluation under $v$ agrees with evaluation under $\sigma$ on $A$: \begin{align*} E_\sigma(A)=v(A)=1. \end{align*} Thus every assignment in $\mathcal{V}_A$ makes $A$ true, and the algorithm returns yes. Therefore the algorithm halts on every input and returns yes exactly on the valid propositional formulas. Hence $\operatorname{Val}(\mathcal{L})$ is decidable. [/guided] [/step]