Question about $\Gamma_\infty^M$ deriving a very specific wff

Question

In p.69 of Tourlakis's mathematical logic book.

He pulls a very specific theorem seemingly out of thin air.

$\Gamma_\infty^M \vdash \exists_x(f \bar n ... = x)$

I'm not sure how this is derived as there are no theorems about the restricted theory and function symbols.

The closest thing I found was it derives some general $\exists_x(A)$ but can $A = f \bar n ... = x$ in every case? Is this the correct train of thought?

Answer 1

The context is the "Henkin construction" of the model needed for the proof of the Completeness Theorem.

At page 65 you can see the definition of the set $\Gamma_{\infty}$ of formulas.

At page 67 there is the definition of its "restriction" $\Gamma_{\infty}^M$.

$M$ is defined as a subset of $\mathbb N$ :

$M = \{ f (n) : n \in \mathbb N \}$

where $f(n) = \text { the smallest } m \text { such that } m ∼ n$ [using Definition I.5.25 of page 66 for the equivalence relation $∼$].

Consider now page 69 :

Let next $f_k$ be a function letter of arity $k$,

this is not the fucntion $f$ above. The new one is a symbol of the language.

and let $n_1,\ldots, n_k$ be an input for $f_k^I$. What is the appropriate output? [I.e. what is $f_k^I (n_1,\ldots, n_k)$ ? ]

Well, first observe that $\Gamma_{\infty}^M \vdash (∃x) f_k(\overline {n_1},\ldots, \overline {n_k}) = x$

Why? By axioms for equality : $x=x$ [Ax3., page 34], followed by Corollary I.4.12 (Substitution of Terms) : $\vdash f_k(\overline {n_1},\ldots, \overline {n_k})=f_k(\overline {n_1},\ldots, \overline {n_k})$.

Finally apply Ax2. : $\mathcal A[x ← t] \to (∃x) \mathcal A \text { for any term } t$, to get :

$\vdash (∃x)f_k(\overline {n_1},\ldots, \overline {n_k})=x$.

Answer 2

For any language, any theory $\Gamma$, and any terms $t_1,...,t_k$ not containing the variable $x$, any function symbol $f$ of arity $k$, you have $\Gamma \vdash (\exists x) ft_1...t_k = x$.

That's for the simple reason that you have $\Gamma \vdash ft_1...t_k = t$ with $t=ft_1...t_k$ and so you can use Existential introduction on $t$.

Note that Existential Introduction is the rule that (under the right conditions) states that if $\Gamma \vdash P(t)$ for some term $t$, then $\Gamma\vdash (\exists x) P(x)$. This rule makes sense : if you know that $P(t)$ is true for a specific $t$, then you know that it's true for some $x$.