I have to give a formal proof in the Hilbert calculus for

$(\forall x\,\,\phi)\rightarrow (\forall y\,\, \phi\frac{y}{x})$, if $x$ is free for $y$ in $\phi$ and $y$ is not free in $\phi$.

Unfortunately I have no idea how this proof could be done.

I would be very grateful, if someone could give a hint, or maybe show an example proof, using the Hilbert-calculus.

  • 1
    $\begingroup$ What are your axioms? Have you tried to apply directly the axiom schemes Q5 and Q6 here? $\endgroup$ – Bruno Bentzen May 5 '15 at 12:42
  • $\begingroup$ Excuse me, I do not know where to start. Yes, I have to use the axiom schemes, but I cant really imagine how I have to combine them to get this result. $\endgroup$ – user105916 May 5 '15 at 12:56

See :

1) $\forall x \phi$ --- assumption

2) $\forall x \phi \to \phi^y_x$ --- Ax.2 : $x$ is free for $y$ in $\phi$

3) $\phi^y_x$ --- from 1) and 2) by modus ponens

4) $\forall y \phi ^y_x$ --- from 3) by Generalization Th [page 117 : $y$ not free in $\forall x \phi$]

5) $\forall x \phi \to \forall y \phi ^y_x$ --- from 1) and 4) by Deduction Th [page 118].


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.