Determine under which conditions the formula $\phi[t/x]\leftrightarrow \forall x ((x=t)\rightarrow \phi)$ is logically true

Question

I am stucked at this problem for a long time:

Determine under which conditions the following first-order formula is logically true

$$\phi[t/x]\leftrightarrow \forall x ((x=t)\rightarrow \phi)$$

where $t$ is a term, $x$ is a variable, $\phi$ is a formula and $\phi[t/x]$ denotes that we are substituting the term $t$ in place of the free occurrences of the variable $x$ in the string $\phi$ and that none of the variables in $t$ becomes bound to one of the quantifieres in $\phi$ (If any).

---

For the $\rightarrow$ side we can deduce as follows: let $K=\{\phi[t/x]\}$, now (1) $K\vdash \phi[t/x]$ (2) $K\vdash \phi[t/x]\rightarrow ((t=t)\rightarrow \phi[t/x])$ (3) $K\vdash ((t=t)\rightarrow \phi[t/x])$ , Now I do not know how to conclude $K\vdash \forall x((x=t)\rightarrow \phi)$ ? Which axioms should I use?

Thanks for any hint/help.

Answer 1

Ref to :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), Ex.13, page 130.

For $\leftarrow$ :

1) $∀x((x=t) \to \varphi)$ --- assumed

2) $(t=t) \to \varphi[t/x]$ --- from 1) and Enderton's Ax.2 : $∀xα \to α_t^x$, where $t$ is substitutable for $x$ in $\alpha$, and modus ponens

3) $\vdash t=t$ --- from equality axiom Ax.5

4) $\varphi[t/x]$ --- from 2) and 3) by mp

$\vdash ∀x((x=t) \to \varphi) \to \varphi[t/x]$ --- from 1) and 4) by Deduction Th.

---

For $\rightarrow$ :

We need the following :

Equality Theorem [see Shoenfield, page 35]. Let the term $b'$ be obtained from the term $b$ by replacing some occurrences of $a_1, \ldots ,a_n$ by $a_1', \ldots, a_n'$ respectively, and let the formula $A'$ be obtained from the formula $A$ by the same type of replacements.

If $\vdash a_1 = a_1', \ldots, \vdash a_n = a_n'$, then $\vdash b = b'$ and $\vdash A \leftrightarrow A'$.

It is provable by induction on the lenght of $b$. We have also [page 36] the

Corollary 2. $\vdash a_1 = a_1' \to \ldots \to a_n = a_n' \to (A[a_1,\ldots, a_n] \leftrightarrow A[a_1',\ldots, a_n'])$.

[It is the "generalization" of Enderton's equality axiom Ax.6 : $x = y \to (α → α')$, where $α$ is atomic and $α'$ is obtained from $α$ by replacing $x$ in zero or more (but not necessarily all) places by $y$.]

1) $\varphi[t/x]$ --- assumed : $x$ does not occur in $t$ and $t$ has replaced all the free occurrences of the variable $x$ in $\varphi$

2) $\vdash x=t \to (\varphi \leftrightarrow \varphi[t/x])$ --- from Coroll.2 above : $\varphi$ is $\varphi[x/x]$

3) $\vdash \varphi[t/x] \to (x=t \to \varphi)$ --- from 2) by tautological implication [Enderton's Lemma 24C (Rule T), page 118]

4) $(x=t \to \varphi)$ --- from 1) and 3) by mp

5) $\forall x (x=t \to \varphi)$ --- from 5) by Generalization Th : $x$ not free in 1), that means : $t$ must replace all free occurrences of $x$ in $\varphi$, and that $t$ has no occurrences of $x$

$\vdash \varphi[t/x] \to \forall x (x=t \to \varphi)$ --- from 1) and 5) by Deduction Th.