0
$\begingroup$

I am asked to prove that

$$K \vdash (a \rightarrow \exists x \beta ) \implies K\vdash \alpha \rightarrow \beta[t/x]$$ is true using deduction.

I've failed to prove this and suspect there is an error here and this is false.

$\endgroup$
  • $\begingroup$ I think it is wrong. In the left term, $x$ is a bound variable (i.e. it is binded, you can't give it any value you want), while in the right term, $x$ is a free variable, so the truth value of the expression depends on the value of $x$. $\endgroup$ – Zachi Evenor Jun 9 '12 at 12:12
2
$\begingroup$

It is not true. Let $K$ be the empty theory in a language with one predicate letter $p$, no constant letters and no function letters; then let $\alpha$ be $\exists x.p(x)$ and $\beta$ be $p(x)$. Then the precedent $$\varnothing \vdash (\exists x.p(x)) \to (\exists x.p(x))$$ is easily provable, but the only possible $t$s in the languages are variables, and if we choose such a $t$, then the conclusion $$\varnothing \vdash (\exists x.p(x)) \to p(y)$$ is clearly not valid -- it is easy to find an interpretation where it isn't true.

On the other hand, you should be able to prove $$ K\vdash \alpha \to \forall x.\beta ~\Longrightarrow~ K \vdash \alpha \to \beta[t/x]$$

$\endgroup$
  • $\begingroup$ I hate this course :( $\endgroup$ – Nahum Jun 9 '12 at 16:09

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.