One can provide a constructive proof of the propositional Adequacy Theorem, though it is (necessarily) much more involved. The classical one, due to Kalmar and contained in Mendelson's Introduction to Mathematical Logic, is based on the following.
Notation: Let $v$ be any truth assignment to the sentence variables. Given any sentence $A$, by $A^\prime$ we denote $ \begin{cases} A, &\text{if }v(A) = T; \\ \neg A, &\text{if }v(A) = F. \end{cases} $
Main Lemma: Suppose that $A$ is a sentence, and $b_1 , \ldots , b_n$ are all of the sentence variables that occur in $A$. If $v$ is any truth assignment to the sentence variables, then $b_1^\prime , \ldots , b_n^\prime \vdash A^\prime.$
Proof sketch of Main Lemma: We proceed by induction on the complexity of $A$, the number of logical connectives in $A$.
- The base case consists of $A$ being a sentence variable itself, and the result follows trivially.
- In the inductive case where $A \equiv \neg A_0$, note that we have that $b_1^\prime , \ldots , b_n^\prime \vdash A_0^\prime$. We handle the cases $v(A_0) = T$ and $v(A_0) = F$ separately, noting how $A^\prime$ is related to $A_0^\prime$.
- In the inductive case where $A \equiv A_0 \rightarrow A_1$, note that by the induction hypothesis we already have that \begin{gather} b_0^\prime , \ldots , b_n^\prime \vdash A_0^\prime; \\ b_0^\prime , \ldots , b_n^\prime \vdash A_1^\prime. \end{gather} We look at the four possible combinations of $v(A_0)$ and $v(A_1)$ separately, noting how $A^\prime$ is related to $A_0^\prime$ and $A_1^\prime$ in each case. $\vdash$
Once the Main Lemma has been established, one can proceed rather quickly to the proof of Adequency as follows.
Proof of Adequacy: Let $A$ be any tautology, and let $b_1 , \ldots , b_n$ be the sentence variables which occur in $A$. As any truth assignment makes $A$ true, by the Main Lemma we have that $*b_1 , \ldots , *b_{n-1}, *b_n \vdash A,$ where $*b_i$ denotes an arbitrary choice between $b_i$ and $\neg b_i$. That is, the Main Lemma gives us $2^n$ different formal proofs.
Fixing some choice for $*b_1 , \ldots , *b_{n-1}$, note that as \begin{gather} *b_1 , \ldots , *b_{n-1}, b_n \vdash A; \\ *b_1 , \ldots , *b_{n-1}, \neg b_n \vdash A, \end{gather} by the Deduction Theorem it follows that \begin{gather} *b_1 , \ldots , *b_{n-1} \vdash b_n \rightarrow A; \\ *b_1 , \ldots , *b_{n-1} \vdash \neg b_n \rightarrow A. \end{gather} We may then conclude that $*b_1 , \ldots , *b_{n-1} \vdash A.$ Note that this gives us an additional $2^{n-1}$ formal proofs.
Again fixing choices for $*b_1, \ldots , *b_{n-2}$ we have that \begin{gather} *b_1 , \ldots , *b_{n-2}, b_{n-1} \vdash A; \\ *b_1 , \ldots , *b_{n-2}, \neg b_{n-1} \vdash A, \end{gather} and we may continue the procedure as above.
Eventually we will arrive at $\vdash A,$ as desired. $\Box$
The proof outlined above does rely on knowing some additional formal theorems, such as $( C \rightarrow D ) \rightarrow ( ( \neg C \rightarrow D ) \rightarrow D )$ for sentences $C,D$, but there are only finitely many such theorem schemata, and each can be given a formal proof. Additionally, we need a constructive proof of the Deduction Theorem, which, again, is not too difficult to provide.