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

[Mr.Cauliflower]

Hello,

I don't know how to prove this:

<br /> \vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)<br />

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

<br /> \vdash A_{x}[t] \rightarrow (\exists x) A<br />

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 -&gt; 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 \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 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 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&#039;re given, since if A_x[t] is defined such that EVERY free occurence of x is replaced by t, then if A -&gt; B has free occurences of x in it, it doesn&#039;t fit the right format to be used in the &quot;axioms of specificatino&quot; 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&#039;ve given.

 

[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 occurence of x.

And if this condition is satisfied, then

<br /> A_{x}[t]<br />

means formula A with ALL occurrences of x substituted 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 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 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.

I don't get this...if I have let's say formula A

<br /> (x.x = z.x) \rightarrow (z &gt; 0)<br />

then if I write A_{x}[t], where t = \sin z, it is

<br /> (\sin z. \sin z = z.\sin z) \rightarrow (z &gt; 0)<br />

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 occurence of x.

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 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 occurence 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 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?

 

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

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)

 

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