Problem in Logic - Hilbert Systems

[andrewkirk]

Homework Statement

In a Hilbert System, prove:
$$\phi[x|m] \rightarrow\forall y((y=m)\rightarrow\phi[x|y])$$
where $\phi$ is a formula, $y, x$ are variables and $m$ is a constant.
$\phi[a|b]$ denotes the formula obtained by substituting $b$ for $a$ in $\phi$
This problem crops up in my attempting to prove Godel's diagonal lemma (aka 'Fixed Point Theorem').

Homework Equations

The axioms of a Hilbert system are standard, as set out in http://en.wikipedia.org/wiki/Hilbert_system

The Attempt at a Solution

\begin{align}
\phi[x|m]\ \ \ \ \ \ \text{1. Hypothesis}\\
y=m\ \ \ \ \ \ \text{2. Hypothesis}\\
(y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y))\ \ \ \ \ \ \text{3. Axiom Schema 6 (substitution of equal variables)}\\
\phi[x|m]\rightarrow\phi[x|y]))\ \ \ \ \ \ \text{4. Modus Ponens applied to 2 and 3}\\
\phi[x|y]\ \ \ \ \ \ \text{5. Modus Ponens applied to 1 and 4}\\
(y=m)\rightarrow\phi[x|y]\ \ \ \ \ \ \text{6. Deduction Theorem applied to 2 and 5)}\\
\phi[x|m]\rightarrow((y=m)\rightarrow\phi[x|y])\ \ \ \ \ \ \text{7. Deduction Theorem applied to 1 and 6)}\\
\end{align}
This is almost what's required, except it's missing the universal quantifier $\forall y$ and I can't use Axiom Schema 4 of Generalisation to add it because y is free in this formula.
I tried a different approach that gave me the quantifier where I needed it, but it didn't have the right form.

Any suggestions gratefully received.

PS the equations are horribly aligned. Any suggestions about how to better align them in TeX would be appreciated too.

 

[mighty2000]

Thank you for bringing this interesting problem to our attention. I am happy to help you with your proof.

Firstly, I would like to address your approach using Modus Ponens and the Deduction Theorem. While this is a valid approach, as you have correctly identified, it does not result in the desired form of the formula with the universal quantifier. This is because, as you mentioned, y is a free variable in the formula and thus cannot be generalized using Axiom Schema 4.

Instead, I would like to suggest a different approach using Axiom Schema 6 and Universal Instantiation. Here is the proof:

\begin{align} \phi[x|m]\ \ \ \ \ \ \text{1. Hypothesis}\\\phi[x|m]\rightarrow(\phi[x|m]\rightarrow\phi[x|y])\ \ \ \ \ \ \text{2. Axiom Schema 6 (substitution of equal variables)}\\ \phi[x|m]\rightarrow\phi[x|y]\ \ \ \ \ \ \text{3. Modus Ponens applied to 1 and 2}\\\forall y((y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y]))\ \ \ \ \ \ \text{4. Universal Instantiation applied to 3}\\ \phi[x|m]\rightarrow\forall y((y=m)\rightarrow\phi[x|y])\ \ \ \ \ \ \text{5. Deduction Theorem applied to 1 and 4}\end{align}

As for your question about aligning the equations in TeX, I would suggest using the align* environment instead of align, as it automatically aligns the equations at the desired position. Additionally, you can use the & symbol to specify where you want the equations to be aligned. For example:

\begin{align*} \phi[x|m] & \text{1. Hypothesis}\\ y=m & \text{2. Hypothesis}\\ (y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y]) & \text{3. Axiom Schema 6 (substitution of equal variables)}\\ \phi[x|m]\rightarrow\phi[x|y] & \text{4. Modus Ponens applied to 2 and 3}\\ \forall y((y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y]))