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.