0
$\begingroup$

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?

enter image description here

$\endgroup$
1
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ This answer and Max's answer is pretty much the same, but I would pick this as the answer because it is more formally put. $\endgroup$ – japseow Jan 13 at 11:53
4
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ Ah yes this is exactly what I was missing. Thanks! $\endgroup$ – japseow Jan 13 at 11:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.