Proof of Predicate Logic Statement: (A → B) → (∃x)(A → B)

[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.

 

[AKG]

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

 

[Mr.Cauliflower]

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

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.

 

[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)$).

 

[Mr.Cauliflower]

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)$).

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...

 

[AKG]

Well, what exactly does your book say? You have the scheme [itex]\vdash A_x[t] \rightarrow (\exists x)A[/tex], but like I said, your notation is different from mine. How <i>exactly</i> is A_x[t] defined? I assume it means that every free occurrence of x in A is replaced with t? Does it require that there actually is a free occurrence of x in A? For example, if A is y=y, then can A_x[t] be defined, and is it just y=y?<br /> <br /> If there are free x in $A \rightarrow B$, then you cannot use the axioms you're given, since if A_x[t] is defined such that EVERY free occurrence 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:<br /> <br /> $\phi \vdash (\forall x)(\phi )$ for any formula $\phi$<br /> <br /> $(\forall x)(\phi ) \vdash \phi _x[t]$ for any term t, and any formula $\phi$.<br /> <br /> $\vdash (\phi _x[t] \rightarrow (\exists x)(\phi ))$, the axioms you've given.[/itex]

 

[Mr.Cauliflower]

Well, what exactly does your book say?

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 occurrence of $x$.

And if this condition is satisfied, then

$$A_{x}[t]$$

means formula $A$ with ALL occurrences of $x$ substituted with $t$.

Does it require that there actually is a free occurrence of x in A? For example, if A is y=y, then can A_x[t] be defined, and is it just y=y?

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$.

If there are free x in $A \rightarrow B$, then you cannot use the axioms you're given, since if A_x[t] is defined such that EVERY free occurrence 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.

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$.

 

[AKG]

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 occurrence of $x$.

Something is wrong here. You mean that subformulas of the form $(\forall y)B$ and $(\exists y)B$ contain no free occurrence of x.

I don't get this...

I was thinking, for some reason, that t had to be a constant symbol. Since t can be any term, A_x[x] is the same as A, and so the "axiom of specification" does apply.

 

[Mr.Cauliflower]

Something is wrong here. You mean that subformulas of the form $(\forall y)B$ and $(\exists y)B$ contain no free occurrence of x.

I think we're both saying the same, I wrote ...no subformula of form....

I was thinking, for some reason, that t had to be a constant symbol. Since t can be any term, A_x[x] is the same as A, and so the "axiom of specification" does apply.

So the result is that I should know something more about the variables in [tex]A \rightarrow B[/itex] to know if I can directly use the axiom of specification ( = if term $t$ can be substituted for $x$)?<br /> <br /> Or that I can prove it that way?[/tex]

 

[AKG]

I think we're both saying the same, I wrote ...no subformula of form....

... of the form $(\forall \mathbf{x})$..." but it should be $(\forall \mathbf{y})$.

So the result is that I should know something more about the variables in [tex]A \rightarrow B[/itex] to know if I can directly use the axiom of specification ( = if term $t$ can be substituted for $x$)?<br /> <br /> Or that I can prove it that way?[/tex]

[tex]No, I mean you can use the axiom of specification. I assume that the scheme:<br /> <br /> $$\vdash A_x[t] \rightarrow (\exists x) A$$<br /> <br /> holds for any formula A, and any term t. Then, in particular its true that:<br /> <br /> $$\vdash (A \rightarrow B)_x[x] \rightarrow (\exists x)(A \rightarrow B)$$<br /> <br /> But $(A \rightarrow B)_x[x]$ is just $(A \rightarrow B)$ so indeed<br /> <br /> $$\vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)$$[/tex]

 

[Mr.Cauliflower]

... of the form $(\forall \mathbf{x})$..." but it should be $(\forall \mathbf{y})$

You're right, it's my typo.

Thank you for help.