# Predicate logic proof

1. Jun 20, 2006

### Mr.Cauliflower

Hello,

I don't know how to prove this:

$$\vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)$$

First I thought it is just an instantiation of the dual form of the axiom of specification, which says

$$\vdash A_{x}[t] \rightarrow (\exists x) A$$

but it probably shouldn't be so easy...

Would someone give me any hints?

Thank you.

2. Jun 20, 2006

### AKG

Your notation and terminology is different from mine, but yes, it is that easy.

3. Jun 21, 2006

### Mr.Cauliflower

Thank you. Could you tell me the name you use for the axiom I used here? I often don't know how to translate these things from Czech to English when I want to find something on Google.

4. Jun 21, 2006

### AKG

Different books call it different things. The book I used called it "existential introduction", and in fact it was given in my book as a rule of inference (from $A_x[t]$ you may infer $(\exists x)(A)$).

5. Jun 21, 2006

### Mr.Cauliflower

So I suppose there's no problem having unbound x in $A -> B$?

It would be strange if it was problem, but to be sure...

6. Jun 21, 2006

Well, what exactly does your book say? You have the scheme $\vdash A_x[t] \rightarrow (\exists x)A[/tex], but like I said, your notation is different from mine. How exactly is Ax[t] defined? I assume it means that every free occurence of x in A is replaced with t? Does it require that there actually is a free occurence of x in A? For example, if A is y=y, then can Ax[t] be defined, and is it just y=y? If there are free x in $A \rightarrow B$, then you cannot use the axioms you're given, since if Ax[t] is defined such that EVERY free occurence of x is replaced by t, then if A -> B has free occurences of x in it, it doesn't fit the right format to be used in the "axioms of specificatino" scheme. So if there are free x in $A \rightarrow B$, then I would use the following facts: $\phi \vdash (\forall x)(\phi )$ for any formula $\phi$ $(\forall x)(\phi ) \vdash \phi _x[t]$ for any term t, and any formula $\phi$. $\vdash (\phi _x[t] \rightarrow (\exists x)(\phi ))$, the axioms you've given. 7. Jun 21, 2006 ### Mr.Cauliflower We say that term $t$ is substituable for variable $x$ in formula $A$ if for each variable $y$ from $t$ no subformula of $A$ of form $(\forall x) B$, $(\exists x) B$ contains free occurence of $x$. And if this condition is satisfied, then $$A_{x}[t]$$ means formula $A$ with ALL occurrences of $x$ substituted with $t$. Given the definition above, I would say, NO, it doesn't require any occurrence of the variable being substitued and YES, the result of what you wrote is just $y = y$. I don't get this...if I have let's say formula A $$(x.x = z.x) \rightarrow (z > 0)$$ then if I write $A_{x}[t]$, where $t = \sin z$, it is $$(\sin z. \sin z = z.\sin z) \rightarrow (z > 0)$$ and I think it's perfectly ok even though $x$ is of free occurrence in $A$. Last edited: Jun 21, 2006 8. Jun 21, 2006 ### AKG Something is wrong here. You mean that subformulas of the form $(\forall y)B$ and $(\exists y)B$ contain no free occurence of x. I was thinking, for some reason, that t had to be a constant symbol. Since t can be any term, Ax[x] is the same as A, and so the "axiom of specification" does apply. 9. Jun 21, 2006 ### Mr.Cauliflower I think we're both saying the same, I wrote ...no subformula of form.... So the result is that I should know something more about the variables in $$A \rightarrow B$ to know if I can directly use the axiom of specification ( = if term $t$ can be substituted for $x$)? Or that I can prove it that way? 10. Jun 22, 2006 ### AKG ... of the form $(\forall \mathbf{x})$..." but it should be $(\forall \mathbf{y})$. No, I mean you can use the axiom of specification. I assume that the scheme: [tex]\vdash A_x[t] \rightarrow (\exists x) A$$

holds for any formula A, and any term t. Then, in particular its true that:

$$\vdash (A \rightarrow B)_x[x] \rightarrow (\exists x)(A \rightarrow B)$$

But $(A \rightarrow B)_x[x]$ is just $(A \rightarrow B)$ so indeed

$$\vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)$$

11. Jun 23, 2006

### Mr.Cauliflower

You're right, it's my typo.

Thank you for help.