5

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.

Rudy the Reindeer
  • 46,359
  • What does $\top \to x$ even mean, if $x$ is a variable (as opposed to a proposition or a predicate)? – Zhen Lin Oct 23 '11 at 12:09
  • It could be an axiom but I wrote it as an example of the kind of example I'm looking for. – Rudy the Reindeer Oct 23 '11 at 12:15
  • 1
    @Matt: It can't be an axiom, since it's not even a well-formed formula. – Chris Eagle Oct 23 '11 at 12:25
  • @ChrisEagle: True! I'll delete it seeing as it's not relevant for my question. – Rudy the Reindeer Oct 23 '11 at 12:33
  • 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$. – boumol Oct 23 '11 at 15:20
  • @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... – Rudy the Reindeer Oct 23 '11 at 20:51
  • @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. – boumol Oct 23 '11 at 23:14
  • 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. – Doug Spoonwood Oct 23 '11 at 23:37
  • Take $\psi$ as $Px$, and $\varphi$ as $\forall x Px$. – boumol Oct 23 '11 at 23:41

1 Answers1

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.

Rudy the Reindeer
  • 46,359
  • i think it is necessary to mention the Domain of your interpretation which can be natural numbers. – KFkf Jan 09 '15 at 13:29
  • also it would be better to explain why $\vdash (x = 1) \to \forall x (x = 1)$ is not satisfied by your interpretation – KFkf Jan 09 '15 at 13:30