5
$\begingroup$

The deduction theorem states that if $T \cup \{ \psi \} \vdash \varphi $ and the generalisation rule is not used to prove $\varphi$ then $T \vdash \psi \rightarrow \varphi $.

If I apply the generalisation rule, where exactly does it go wrong if I apply the deduction theorem thereafter? Can someone provide an example?

Many thanks for your help.

  • 0
    What does $\top \to x$ even mean, if $x$ is a variable (as opposed to a proposition or a predicate)?2011-10-23
  • 0
    It could be an axiom but I wrote it as an example of the kind of example I'm looking for.2011-10-23
  • 1
    @Matt: It can't be an axiom, since it's not even a well-formed formula.2011-10-23
  • 0
    @ChrisEagle: True! I'll delete it seeing as it's not relevant for my question.2011-10-23
  • 1
    Hint: Forget about $T$ (i.e., take $T = \emptyset$), and take $\psi$ as a formula with free variables (i.e., it is not a setence) such that $\varphi$ is the universal closure of $\psi$.2011-10-23
  • 0
    @boumol: This? $\{ \exists y (x = y) \} \vdash \forall x \exists y ( x = y)$ and then $\vdash \exists y (x = y) \rightarrow \forall x \exists y (x = y)$? I think that's not a counter example...2011-10-23
  • 0
    @Matt: This is not a counterexample because $\exists y (x = y)$ is always true (it does not matter which is the element $x$). Take a formula with a free variable, but which is not always true.2011-10-23
  • 0
    I don't see how anything could go wrong in classical logic. If you've proven phi assuming psi, no matter how you've proven it, then via soundness phi qualifies as true given psi. So, semantically we have that (psi->phi) comes as equivalent to (psi->T) which implies (psi->phi) as true.2011-10-23
  • 0
    Take $\psi$ as $Px$, and $\varphi$ as $\forall x Px$.2011-10-23

1 Answers 1

3

The important thing to realise is that whatever is on the RHS of $\vdash$ has got to be an axiom (meaning: a universally true formula). On the other hand, on the LHS we can assume whatever we like. So for example if $T = \emptyset$ we can show that $\{ \varphi (x) \} \vdash \forall x \varphi(x)$. What we can't do is to show that $\emptyset \vdash \varphi(x) \to \forall x \varphi (x)$.

To see why we can't let's consider the example $\varphi (x) = (x = 1)$:

If we assume ($x = 1$) then we get the following formal proof of $\{ x = 1 \} \vdash \forall x (x = 1)$:

$(1) x = 1 ( \in T)$

$(2) \forall x (x = 1)$ (generalisation rule applied to ($1$))

On the other hand, if we use the deduction rule on this to get $\vdash (x = 1) \to \forall x (x = 1)$ then we have $\top \to \bot$ if we replace $x$ with $1$ where it's free. But this is false, hence the formula on the RHS is not universally true.

  • 0
    i think it is necessary to mention the Domain of your interpretation which can be natural numbers.2015-01-09
  • 0
    also it would be better to explain why $\vdash (x = 1) \to \forall x (x = 1)$ is not satisfied by your interpretation2015-01-09