[proofplan] Fix an effective, sound, and complete proof system for first-order logic. The algorithm enumerates all finite strings and checks which of them encode formal derivations of the input sentence. Effective syntax makes this verification decidable, completeness ensures that every valid sentence eventually appears as the conclusion of some finite derivation, and soundness ensures that no invalid sentence is ever accepted. [/proofplan] [step:Fix an effective sound and complete proof system] Let $\mathsf{P}$ be a standard formal proof system for first-order logic over the language $\mathcal{L}$, such as a Hilbert system, natural deduction system, or sequent calculus, whose formulas and finite derivations are effectively encoded by finite strings over a finite alphabet. We require the following two properties of $\mathsf{P}$: 1. Soundness: if $\mathsf{P} \vdash \varphi$, then $\mathfrak{M} \models \varphi$ for every $\mathcal{L}$-structure $\mathfrak{M}$. 2. Completeness: if $\mathfrak{M} \models \varphi$ for every $\mathcal{L}$-structure $\mathfrak{M}$, then $\mathsf{P} \vdash \varphi$. These are the soundness theorem and [Gödel completeness theorem](/theorems/4652) for first-order logic (citing a result not yet in the wiki: Soundness and Completeness Theorem for First-Order Logic). Since $\mathcal{L}$ is computable, there is an algorithm deciding whether a finite string is a well-formed $\mathcal{L}$-formula, whether it is an $\mathcal{L}$-sentence, and whether a finite sequence of formulas satisfies each inference rule of $\mathsf{P}$. [/step] [step:Define the semi-decision procedure by enumerating finite derivations] Define a Turing machine $T$ as follows. On input $n \in \mathbb{N}$, first check whether $n = \ulcorner \varphi \urcorner$ for some $\mathcal{L}$-sentence $\varphi$. If not, run forever. If $n = \ulcorner \varphi \urcorner$, enumerate all finite strings $s_1, s_2, s_3, \dots$ over the proof alphabet of $\mathsf{P}$. For each string $s_k$, run the decidable derivation-checking procedure for $\mathsf{P}$ to determine whether $s_k$ encodes a correct finite $\mathsf{P}$-derivation whose final line is exactly $\varphi$. If it does, halt and accept. If it does not, continue to $s_{k+1}$. This procedure is effective because finite strings over a finite alphabet are computably enumerable, and correctness of a finite formal derivation is decidable by checking each displayed formula and each inference-rule application in finitely many steps. [/step] [step:Show that every valid sentence is accepted] Assume $\ulcorner \varphi \urcorner \in \operatorname{Val}_{\mathcal{L}}$. By definition of $\operatorname{Val}_{\mathcal{L}}$, the sentence $\varphi$ is true in every $\mathcal{L}$-structure. By completeness of $\mathsf{P}$, there exists a finite $\mathsf{P}$-derivation $d$ whose final line is $\varphi$. The enumeration of all finite strings eventually lists the finite string encoding $d$. When the machine reaches that string, the derivation-checking procedure verifies that it is a correct $\mathsf{P}$-derivation with conclusion $\varphi$. Therefore $T$ halts on input $\ulcorner \varphi \urcorner$. [/step] [step:Show that no invalid sentence is accepted] Assume $\ulcorner \varphi \urcorner \notin \operatorname{Val}_{\mathcal{L}}$. Then there exists an $\mathcal{L}$-structure $\mathfrak{M}$ such that $\mathfrak{M} \not\models \varphi$. By soundness of $\mathsf{P}$, no correct $\mathsf{P}$-derivation can have final line $\varphi$; otherwise $\varphi$ would be true in every $\mathcal{L}$-structure. Hence, during the enumeration, the derivation-checking procedure never finds a correct derivation of $\varphi$. The machine $T$ therefore never halts on input $\ulcorner \varphi \urcorner$. [/step] [step:Conclude semi-decidability of first-order validity] The machine $T$ halts exactly on those inputs $\ulcorner \varphi \urcorner$ for which $\varphi$ is a valid first-order $\mathcal{L}$-sentence. Therefore $\operatorname{Val}_{\mathcal{L}}$ is semi-decidable. [/step]