Adequacy theorem for propositional calculus

Question

I have been thinking about the following classical theorem of propositional calculus:

Adequacy Theorem:

if $A$ is a tautology then $A$ is provable by the logical axioms

Now "$A$ is a tautology" is a sentence of the form $\forall v T_A$($v$) (where $v$ is a valuation function and $T_A(v)$ says that $A$ is true for $v$) while on the other hand "A is provable" is $\exists p$ i.e. an existential statement.

Looking at classical proofs of this theorem it seems to me that we started with a hypothesis which is not existential and we came up claiming that there exists something (a proof) without actually providing any way to find it(!)

The proof of Adequacy Theorem is carried out in slightly different ways among the logic textbooks but I suppose the core argument is essentially the same. In my book (Hamilton) the key step of the proof are:

lemma 1

if the system $L^*$ is consistent then there exists a consistent complete extension

lemma 2

if $L^*$ is consistent and complete then $L^*$ has a model

my understanding is that the relevant "existence bit" of the proof is in lemma 1 and apparently it seems nonconstructive to me and even if it would be constructive we are using it in a proof by contradiction.

So my questions are:

• which logical principles are involved here? Are they really non-constructive? Is there a hidden axiom of choice? Is there a way to prove the theorem in a constructive way?

Thank you for your insights.

Answer 1

In the very general case the a weaker form of the axiom of choice is needed, namely the Prime Ideal Theorem. This is because, in the general case, an ultrafilter in the Lindenbaum's algebra is a complete and consistent theory.

On the other hand if the language is countable you can enumerate its sentences hence using the axiom of choice is not necessary. Of course, the construction of the complete consistent set of sentences is fairly non-constructive. The argument is as follows:

Let $T_0$ be a consistent set of sentences. Define:

$$T_{n+1} =\begin{cases} T_n\cup\{\phi_n\} & \textrm{ if } T_n\cup\{\phi_n\}\textrm{ is consistent} \\ T_n\cup\{\lnot\phi_n\} & \textrm{ otherwise} \end{cases}$$

In the second case it is obvious that $T_n\models\lnot\phi_n$, hence $T_n\cup\{\lnot\phi_n\}$ is consistent, if $T_n$ is. It is fairly easy to see that $T^\star=\bigcup_{n\in\mathbb{N}}T_n$ is complete and consistent. The completeness follows directly from the fact that for every sentence $\phi$ $T^\star$ contains either $\phi$ or $\lnot\phi$. The consistency is seen as follows: If $T^\star$ proved an inconsistency, then finite number of sentences would be part of the proof, hence some $T_n$ would be inconsistent.

As you can see this is highly non-constructive. It is unclear how you can decide which of the sets is consistent (in fact in many cases you cannot). Of course there is no use of the axiom of choice here.

Answer 2

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.

Answer 3

Moving from a (countable) consistent complete theory to a syntactic model can be done computably. However obtaining a consistent complete extension cannot be done computably (see Godel's first incompleteness theorem).

If you are interested in the topic, I would suggest checking "Pure Recursive Model Theory" by T.S. Miller in E.R. Griffor, Handbook of Computability Theory, 1999. It is a very good starting point.

Another reference on the topic is "Handbook of Recursive Mathematics: Recursive Model Theory" by Y.L. Ershov.

(I am interpreting "constructive" as "algorithmic/computably", if that is not what you mean please clarify the question.)