I was trying the following exercise of identity of VanDalen's Predicate Logic. It is as follows.

$$\vDash \phi(t) \leftrightarrow \forall x(x=t \rightarrow \phi(x)), \ \ \ x \not \in FV(t)$$

It has a similar part of the Instant Axiom: $$ \vDash \forall x_1,\cdots,x_n, y_1,\cdots,y_n\ \wedge_{i\leq n} (x_i = y_i)\rightarrow (\phi(x_1,\cdots, x_n)\rightarrow \phi(y_1, \cdots, y_n)) $$

I was trying proving this exercise, going from $\forall x(x=t \rightarrow \phi(x))$ to $\phi(t)$. Using the axiom, we have

\begin{align*} &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t))\\ \text{and by introduction of }\wedge, \\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t))) \wedge \forall x(x=t \rightarrow \phi(x))\\ \text{because }x\not \in FV(t), \\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t)) \wedge (x=t \rightarrow \phi(x))\\ &\vDash \forall x,t (x=t \rightarrow (\phi(x)\rightarrow\phi(t)) \wedge \phi(x))\\ &\vDash \forall x,t (x=t \rightarrow \phi(t))\\ \end{align*}

I'm having problems finishing the entire proof, above is my unfinished version of rl-direction ($\Leftarrow$).

How do you prove it with a short or more clear way. Thanks.

  • Are you sure about this statement? Take $$\begin{cases} \phi(0) = \top \\ \phi(1) = \bot \\ t = 1 \end{cases}$$ This is why universal instantiation is usually written as $$\text{from } P \vdash Qt \text{ infer } P \implies \forall Q$$ rather than $$\text{from } P \implies Qt \text{ infer } P \implies \forall Q$$ – DanielV Jul 16 '16 at 11:02
up vote 2 down vote accepted

Just apply the universally quantified statement to $t$, and you'll get "$t=t \to φ(t)$" after which you can get rid of the condition since it is true by an axiom. In general, don't pattern-match to guess which axioms to use (it won't work), but rather figure out what the statements themselves mean and how to construct or deconstruct them as appropriate. In this case where you want to prove the backward implication, you want to construct "$φ(t)$", and the only way you can do that using the given universal statement is to deconstruct it, and clearly applying it to $t$ is necessary to get what you want at all.

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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